Proof Discovery in LK System by Analogy
Masateru Haxao · 2005
Abs t r ac t . In this paper, a schema guided model of proof discovery by analogy in theorem proving under the concept such that similar problems have similar proofs is proposed. A proof discovery system for LK inference system is formulated by considering it as a general reasoning system which is close to our thinking process. At first, a schema and a proof schema which describe the types of formulas and proofs are formulated as higher order terms. Next, the similarities of formulas and proofs are defined by means of the realizability by schemata and proof schema. Finally, a unification based procedure of discovering an LK proof for any given sequent is presented, and the implemented system is overviewed.