Problem Solving in Interactive Proof: A Knowledge-Modelling Approach
J. Stuart Aitken · 1996
This paper presents a model of proof discovery derived from the proof attempts of subjects who carried out interactive proofs using the HOL or Isabelle provers. Techniques of knowledge modelling, from knowledge-basedsystem development, are used to derive a semi-formal model of the knowledge utilised by the subjects. The proposedmodel makes claims about the relation between the problem class, the proof plan and its implementation.