TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
Johann Rosain, Julie Cailler

TL;DR
This paper introduces TableauxRocq, a formalized, sound embedding of free-variable tableaux in Rocq, enabling certified proof checking and improved performance with Skolemization in automated theorem proving.
Contribution
It formalizes free-variable tableaux in Rocq within a proof assistant, providing a modular Skolemization system and a certified proof checker for automated theorem provers.
Findings
TableauxRocq is sound and modular.
It enables certified proof checking with comparable performance.
Skolemization optimizations improve proof checking efficiency.
Abstract
The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because it is the only available method-e.g., in certain modal logics-or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimizations. Moreover, we show how TableauxRocq can be used as a certifier for automated theorem provers by adapting the Goeland prover- that can already output Rocq terms-to output proofs in the TableauxRocq format. By using the power of reflection,…
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
