TL;DR
This paper presents a two-phase approach to integrate an intuitionistic first-order prover into Coq, enabling efficient proof replay by generating and translating certificates based on matrix characterization.
Contribution
It introduces a novel method combining matrix-based certificate generation with sequent proof translation for intuitionistic logic in Coq.
Findings
Successfully integrates intuitionistic prover into Coq
Enables efficient proof replay of external proofs
Uses matrix characterization for certificate generation
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
