TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq

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, 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.