Advertisement

Automated theorem proving in a simple meta-logic for LF

  • Carsten Schürmann
  • Frank Pfenning
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with induction principles needed to reason about them. In this paper we develop a meta-logic M2 which allows inductive reasoning over LF encodings, and describe its implementation in Twelf, a special-purpose automated theorem prover for properties of logics and programming languages. We have used Twelf to automatically prove a number of non-trivial theorems, including type preservation for Mini-ML and the deduction theorem for intuitionistic propositional logic.

Keywords

Deductive System Recursive Call Logical Framework Sequent Calculus Automate Theorem Prove 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Coq91]
    Thierry Coquand. An algorithm for testing conversion in type theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255–279. Cambridge University Press, 1991.Google Scholar
  2. [CP96]
    Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264–275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.Google Scholar
  3. [DPS97]
    JoËlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA '97), pages 147–163, Nancy, France, April 1997. Springer-Verlag LNCS.Google Scholar
  4. [Eri94]
    Lars-Henrik Eriksson. Pi: An interactive derivation editor for the calculus of partial inductive definitions. In Alan Bundy, editor, Proceedings of the Twelfth International Conference on Automated Deduction, pages 821–825. Springer-Verlag LNAI 814, June 1994.Google Scholar
  5. [HHP93]
    Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.MathSciNetGoogle Scholar
  6. [Mag95]
    Lena Magnusson. The Implementation of ALF—A Proof Editor Based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology and Göteborg University, January 1995.Google Scholar
  7. [McD97]
    Raymond McDowell. Reasoning in a logic with definitions and induction. PhD thesis, University of Pennsylvania, 1997.Google Scholar
  8. [MM97]
    Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, Warsaw, Poland, June 1997. To appear.Google Scholar
  9. [MP91]
    Spiro Michaylov and Frank Pfenning. Natural semantics and some of its meta-theory in Elf. In L.-H. Eriksson, L. HallnÄs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299–344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596.Google Scholar
  10. [Pfe91]
    Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, The Netherlands, July 1991.Google Scholar
  11. [Pfe92]
    Frank Pfenning. Computation and deduction. Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May 1992.Google Scholar
  12. [Pfe94]
    Frank Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811–815, Nancy, France, June 1994. Springer-Verlag LNAI 814. System abstract.Google Scholar
  13. [Pfe96]
    Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119–134, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk.Google Scholar
  14. [PR92]
    Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 537–551, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607.Google Scholar
  15. [Roh94]
    Ekkehard Rohwedder. Verifying the meta-theory of deductive systems. Thesis Proposal, February 1994.Google Scholar
  16. [RP96]
    Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296–310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058.Google Scholar
  17. [SH93]
    Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222–232, Montreal, Canada, June 1993.Google Scholar
  18. [SP98]
    Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. Technical Report CMU-CS-98-123, Carnegie Mellon University, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Carsten Schürmann
    • 1
  • Frank Pfenning
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityUSA

Personalised recommendations