Electronic Proceedings in Theoretical Computer Science (Jun 2016)

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

  • Fabian Kunze

DOI
https://doi.org/10.4204/EPTCS.210.6
Journal volume & issue
Vol. 210, no. Proc. HaTT 2016
pp. 30 – 35

Abstract

Read online

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.