TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
This work provides the first formal verification of free-variable tableaux, enabling certified proof checking for automated theorem provers, which is a foundational step for proof assistants but incremental in methodology.
The authors present TableauxRocq, the first formalization of free-variable tableaux in a proof assistant (Rocq), proving it sound and modular. They demonstrate its use as a certifier for the Goeland prover, showing that proof checking times are comparable without optimizations and strictly better with Skolemization optimizations.
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, thereby providing a fully certified proof checker for free, we show that Goeland's exported Rocq terms and TableauxRocq's proof certificates can be checked in a similar time frame without proof optimizations, and that the latter has strictly better performances in presence of Skolemization-related optimizations.