Abstract
We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track of the structure of the proof and to deal with the high level steps, for instance, induction. The steps that involve purely propositional or simple first-order reasoning are left to a first-order resolution prover (the system Gandalf in our prototype). The correctness of this interaction is based on a general meta-theoretic result. One feature is the simplicity of our translation between the logical framework and first-order logic, which uses implicit typing. Implementation and case studies are described.
Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abel, A., Coquand, T.: Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 23–38. Springer, Heidelberg (2005)
Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover (extended version). Technical report, Department of Computing Science, Chalmers University of Technology, Gothenburg, Sweden (2005), Available under http://www.cs.chalmers.se/~ulfn/papers/fol.html
Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (April 2005) (Manuscript, available online)
Beeson, M.: Otter-λ home page (2005), http://mh215a.cs.sjsu.edu/
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. In: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Bezem, M., Coquand, T.: Newman’s lemma – a case study in proof automation and geometric logic. Bulletin of the EATCS 79, 86–100 (2003); Logic in Computer Science Column
Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. JAR 29(3–4), 253–275 (2002); Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices 35(9), 268–279 (2000)
Coquand, C., Coquand, T.: Structured type theory. In: Workshop on Logical Frameworks and Meta-languages (LFM 1999), Paris, France (September 1999)
Coste, M., Lombardi, H., Roy, M.-F.: Dynamical methods in algebra: Effective Nullstellensätze. APAL 111(3), 203–256 (2001)
de Bruijn, N.G.: A survey of the project Automath. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays in combinatory logic, lambda calculus and formalism, pp. 579–606. Academic Press, London (1980)
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39(176–210), 405–431 (1935)
Huang, X., Kerber, M., Kohlhase, M., Melis, E., Nesmith, D., Richts, J., Siekmann, J.H.: Omega-MKRP: A proof development environment. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 788–792. Springer, Heidelberg (1994)
Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–321. Springer, Heidelberg (1999)
Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 134–138. Springer, Heidelberg (2002)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) STRATA 2003, number CP-2003-212448 in NASA Technical Reports, pp. 56–68 (September 2003)
Lamport., L.: How to write a proof. In: Global Analysis in Modern Mathematics, February 1993, pp. 311–321. Publish or Perish, Houston (1993); Also appeared as SRC Research Report 94
Meng, J., Paulson, L.C.: Experiments on supporting interactive proof using resolution. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 372–384. Springer, Heidelberg (2004)
Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358 (1992)
Nordström, B., Petersson, K., Smith, J.: Martin-Löf’s type theory. In: Handbook of Logic in Computer Science, vol. 5, OUP (October 2000)
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford (1990)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM 12(1), 23–41 (1965)
Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: JProver: Integrating connection-based theorem proving into interactive proof assistants. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 421–426. Springer, Heidelberg (2001)
Smith, J.M., Tammet, T.: Optimized encodings of fragments of type theory in first-order logic. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 265–287. Springer, Heidelberg (1996)
Tammet, T.: Gandalf. JAR 18(2), 199–204 (1997)
Wick, C.A., McCune, W.: Automated reasoning about elementary point-set topology. JAR 5(2), 239–255 (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abel, A., Coquand, T., Norell, U. (2005). Connecting a Logical Framework to a First-Order Logic Prover. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_17
Download citation
DOI: https://doi.org/10.1007/11559306_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)