Towards the Integration of an Intuitionistic First-Order Prover into Coq

Fabian Kunze
(Saarland University)

An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intuitionistic prover generates a certificate based on the matrix characterization of intuitionistic first-order logic; the certificate is then translated into a sequent-style proof.

In Jasmin Christian Blanchette and Cezary Kaliszyk: Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016), Coimbra, Portugal, July 1, 2016, Electronic Proceedings in Theoretical Computer Science 210, pp. 30–35.
Published: 17th June 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: