# Proof discovery in LK system by analogy

## Abstract

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.

## Keywords

Logic Program Inference Rule Schema Base Complete Proof Analogical Reasoning## Preview

Unable to display preview. Download preview PDF.

## References

- 1.H. Barendregt:
*Introduction to Generalized Type Systems*, Proc. of 3rd International Conference on Theoretical Computer Science, 1–37 (1989).Google Scholar - 2.B. Brock, S. Cooper and W. Pierce:
*Analogical Reasoning and Proof Discovery*, LNCS**310**454–468 (1988).Google Scholar - 3.M. R. Donat and L. A. Wallen:
*Learning and Applying Generalized Solutions using Higher Order Resolution*, LNCS**310**, 41–60 (1988).Google Scholar - 4.G. Evans:
*A Program for the Solution of Geometric Analogy Intelligence Test Questions*, in Minsky (ed.):*Semantic Information Processing*, MIT Press, 271–353 (1968).Google Scholar - 5.C. Feng and S. Muggleton:
*A Note on Least General Generalization in Higher Order Logic*, Proc. of lst Workshop on Inductive Logic Programming (1992).Google Scholar - 6.P. Flener:
*Logic Program Synthesis from Incomplete Information*, Kluwer Academic Press (1995).Google Scholar - 7.J. H. Gallier:
*Logic for Computer Science*, John Wiley & Sons (1987).Google Scholar - 8.N. J. Genesereth and N. J. Nilson:
*Logical Foundation of Artificial Intelligence*, Morgan Kaufman Pub. (1987).Google Scholar - 9.R. Greiner:
*Learning by Understanding Analogy*, Proc. of lst Intern. Workshop on Analogical Reasoning (1987).Google Scholar - 10.M. Haraguchi and S. Arikawa:
*A Formulation of Analogical Reasoning and Its Realization*, J. of JSAI**1**, 132–139 (1986) (in Japanese).Google Scholar - 11.M. Harao:
*LK Theorem Proving by Analogy*, Proc. of PRICAI'92, 714–720 (1992).Google Scholar - 12.R. Harper, F. Honsell and G.Plotokin:
*A Framework for Defining Logics*, Proc. of Symposium on Logic in Computer Science, 194–204 (1987).Google Scholar - 13.R. W. Hasker:
*The Replay of Program Derivations*, PhD Thesis of the University of Illinois (1995).Google Scholar - 14.S. Hayasi:
*Mathematical logic*, Corona Publisher (1989) (in Japanese).Google Scholar - 15.D. H. Helman (ed.):
*Analogical Reasoning*, Kluwer Academic Publishers (1988).Google Scholar - 16.J. H. Holland, K. J. Holyoak, R. E. Nisbett and P. R. Thagard:
*Process of Inference, Learning, and Discovery*, The MIT Press (1986).Google Scholar - 17.G. P. Huet:
*A Unification Algorithm for Typed λ-Calculus*, Theoretical Computer Science**1**, 27–57 (1975).CrossRefGoogle Scholar - 18.G. Huet and B. Lang:
*Proving and Applying Program Transformations Expressed with Second Order Patterns*, Acta Informatica**11**, 31–55 (1975).Google Scholar - 19.
- 20.S. Kedar-Cabelli:
*Analogy from a Unified Perspective*, in [15].Google Scholar - 21.J. W. Lloyd:
*Foundations of Logic Programming*, Springer Verlag (1984).Google Scholar - 22.D. Miller and A. Felty:
*An Integration of Resolution and Natural Deduction Theorem Proving*, Proc. of the AAAI'86, 198–202 (1986).Google Scholar - 23.
- 24.F. Pfenning:
*Types in Logic Programming*, The MIT Press (1992).Google Scholar - 25.G. Polya:
*Induction and Analogy in Mathematics*, Princeton University Press (1953).Google Scholar - 26.K. R. Popper:
*The logic of Scientific Discovery*, Basic Book Inc. (1959).Google Scholar - 27.W. Snyder and J. Gallier:
*Higher Order Unification Revised*, J. of Symbolic Computation**8**, 101–140 (1989).Google Scholar - 28.T. B. de la Tour and R. Caferra:
*Proof Analogy in Interactive Theorem Proving*, Proc. IJCAI'97 95–99 (1989).Google Scholar