Proof discovery in LK system by analogy

  • Masateru Harao
Session 5
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


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.


Logic Program Inference Rule Schema Base Complete Proof Analogical Reasoning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    H. Barendregt: Introduction to Generalized Type Systems, Proc. of 3rd International Conference on Theoretical Computer Science, 1–37 (1989).Google Scholar
  2. 2.
    B. Brock, S. Cooper and W. Pierce: Analogical Reasoning and Proof Discovery, LNCS 310 454–468 (1988).Google Scholar
  3. 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. 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. 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. 6.
    P. Flener: Logic Program Synthesis from Incomplete Information, Kluwer Academic Press (1995).Google Scholar
  7. 7.
    J. H. Gallier: Logic for Computer Science, John Wiley & Sons (1987).Google Scholar
  8. 8.
    N. J. Genesereth and N. J. Nilson: Logical Foundation of Artificial Intelligence, Morgan Kaufman Pub. (1987).Google Scholar
  9. 9.
    R. Greiner: Learning by Understanding Analogy, Proc. of lst Intern. Workshop on Analogical Reasoning (1987).Google Scholar
  10. 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. 11.
    M. Harao: LK Theorem Proving by Analogy, Proc. of PRICAI'92, 714–720 (1992).Google Scholar
  12. 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. 13.
    R. W. Hasker: The Replay of Program Derivations, PhD Thesis of the University of Illinois (1995).Google Scholar
  14. 14.
    S. Hayasi: Mathematical logic, Corona Publisher (1989) (in Japanese).Google Scholar
  15. 15.
    D. H. Helman (ed.): Analogical Reasoning, Kluwer Academic Publishers (1988).Google Scholar
  16. 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. 17.
    G. P. Huet: A Unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1, 27–57 (1975).CrossRefGoogle Scholar
  18. 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. 19.
    K. Inoue: Principles of Abduction, J. of JSAI 7, 48–59 (1991) (in Japanese).Google Scholar
  20. 20.
    S. Kedar-Cabelli: Analogy from a Unified Perspective, in [15].Google Scholar
  21. 21.
    J. W. Lloyd: Foundations of Logic Programming, Springer Verlag (1984).Google Scholar
  22. 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. 23.
    L. C. Paulson: Isabelle, LNCS 828 (1988).Google Scholar
  24. 24.
    F. Pfenning: Types in Logic Programming, The MIT Press (1992).Google Scholar
  25. 25.
    G. Polya: Induction and Analogy in Mathematics, Princeton University Press (1953).Google Scholar
  26. 26.
    K. R. Popper: The logic of Scientific Discovery, Basic Book Inc. (1959).Google Scholar
  27. 27.
    W. Snyder and J. Gallier: Higher Order Unification Revised, J. of Symbolic Computation 8, 101–140 (1989).Google Scholar
  28. 28.
    T. B. de la Tour and R. Caferra: Proof Analogy in Interactive Theorem Proving, Proc. IJCAI'97 95–99 (1989).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Masateru Harao
    • 1
  1. 1.Department of Artificial IntelligenceKyushu Institute of TechnologyIizukJapan

Personalised recommendations