Connecting a Logical Framework to a First-Order Logic Prover

Andreas Abel, Thierry Coquand and Ulf Norell. Connecting a Logical Framework to a First-Order Logic Prover (Extended Version). Technical report, Departement of Computing Science, Chalmers University of Technology, Gothenburg Sweden, 2005.
[ps, pdf, bib ]

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.


Valid HTML 4.01! Disclaimer
Last modified: Thu 13 Apr 2006 03:06:33 PM CEST