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.

翻译：自由变分表格式方法已被广泛用于多种逻辑中的自动化证明。许多自动定理证明器依赖于这一方法，或是因为它是唯一可用的方法（例如在某些模态逻辑中），或是因为它便于生成证明证书。然而，据作者所知，其结果从未在证明助手中被形式化。本文提出了TableauxRocq，一种在Rocq证明器中对自由变分一阶表格式的深层嵌入。该形式化演算被证明是可靠的，并提供了一个模块化的斯科伦化系统，从而能够实现基于斯科伦化的优化。此外，我们展示了如何通过调整Goeland证明器——该证明器已能输出Rocq项——以输出TableauxRocq格式的证明，从而将TableauxRocq用作自动定理证明器的验证器。通过利用反射的能力，我们免费提供了一个完全认证的证明检查器。我们证明，在没有证明优化的情况下，Goeland导出的Rocq项和TableauxRocq的证明证书可以在相似的时间范围内被检查，而在涉及斯科伦化相关优化时，后者具有显著更优的性能。