Towards the Integration of an Intuitionistic First-Order Prover into Coq
Logic in Computer Science
2016-06-21 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1606.05948,
title = {Towards the Integration of an Intuitionistic First-Order Prover into Coq},
author = {Fabian Kunze},
journal= {arXiv preprint arXiv:1606.05948},
year = {2016}
}
Comments
In Proceedings HaTT 2016, arXiv:1606.05427