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: http://dx.doi.org/10.4204/EPTCS.210.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org