pith. sign in

arxiv: 2605.16952 · v1 · pith:2E3EQ52Nnew · submitted 2026-05-16 · 💻 cs.LO

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

Johann Rosain , Julie Cailler This is my paper

Pith reviewed 2026-05-19 18:52 UTC · model grok-4.3

classification 💻 cs.LO
keywords free-variable tableauxRocqproof certificationSkolemizationautomated theorem provingdeep embeddingsoundnessGoeland
0
0 comments X

The pith

TableauxRocq embeds free-variable tableaux in Rocq and proves the embedding sound for use as a certified checker.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents TableauxRocq, a deep embedding of the free-variable first-order tableau calculus inside the Rocq proof assistant. It proves this embedding sound and equips it with a modular Skolemization system that supports common optimizations used by automated theorem provers. The work then adapts the Goeland prover to emit TableauxRocq certificates and shows that reflection-based checking of these certificates runs in similar time to direct Rocq term checking without optimizations and strictly faster when Skolemization optimizations are active. A sympathetic reader would care because the result supplies a practical bridge between efficient automated proof search and fully verified certificates inside an interactive prover.

Core claim

We present TableauxRocq, a deep embedding of free-variable first-order tableaux in Rocq. 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 is

What carries the argument

The deep embedding of the free-variable tableau calculus in Rocq, which encodes inference rules and supports reflective checking of proof certificates while allowing modular Skolemization.

Load-bearing premise

The adaptation of Goeland correctly translates its internal proof steps into the TableauxRocq format without introducing or omitting inferences that would invalidate soundness.

What would settle it

An experiment in which Goeland produces a TableauxRocq certificate that the embedding accepts yet the original formula is unsatisfiable, or a benchmark showing that Skolemization optimizations yield no checking-time improvement or a slowdown.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents TableauxRocq, a deep embedding of free-variable first-order tableaux in the Rocq prover. It claims a machine-checked soundness proof for the formalized calculus, introduces a modular Skolemization system to support optimizations, and demonstrates use as a certifier by adapting the Goeland prover to output proofs in the TableauxRocq format, with performance comparisons showing similar checking times without optimizations and strictly better performance for the latter with Skolemization-related optimizations.

Significance. If the soundness proof holds and the Goeland adaptation is faithful, the work supplies a verified foundation for a widely used proof method in automated theorem proving and enables practical certified checking that can incorporate Skolemization optimizations. The machine-checked soundness proof and the use of reflection for efficient checking are explicit strengths that increase confidence in the results.

major comments (1)
  1. [Section describing the Goeland adaptation and experimental evaluation] The central claim that TableauxRocq can serve as a certifier for Goeland rests on the correctness of the adaptation that maps Goeland's internal proof steps to the rules and Skolemization choices of the embedded calculus. No separate formalization or exhaustive testing of this translator is described, which is load-bearing because any mismatch (extra inferences, omitted variable conditions, or incorrect Skolem term generation) would allow invalid certificates to pass the checker.
minor comments (2)
  1. [Abstract] The abstract states that checking times are 'similar' without optimizations and 'strictly better' with them; adding a reference to the specific table or figure reporting the concrete timings would improve clarity.
  2. [Formalization sections] Notation for free variables, Skolem terms, and the modular Skolemization interface should be cross-checked for consistency between the informal description and the Rocq code excerpts.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their detailed and insightful comments on the manuscript. We address the major concern regarding the Goeland adaptation below and will update the paper to provide additional clarity and details on this aspect.

read point-by-point responses

  1. Referee: [Section describing the Goeland adaptation and experimental evaluation] The central claim that TableauxRocq can serve as a certifier for Goeland rests on the correctness of the adaptation that maps Goeland's internal proof steps to the rules and Skolemization choices of the embedded calculus. No separate formalization or exhaustive testing of this translator is described, which is load-bearing because any mismatch (extra inferences, omitted variable conditions, or incorrect Skolem term generation) would allow invalid certificates to pass the checker.

    Authors: We concur that ensuring the fidelity of the translation from Goeland's proof steps to the formalized TableauxRocq rules is essential for reliable certification. The machine-checked soundness proof guarantees that accepted certificates represent valid derivations in the free-variable tableau calculus. The manuscript describes the adaptation of Goeland to produce TableauxRocq certificates and presents experimental results demonstrating successful checking. To address the referee's point, we will revise the relevant section to include a more comprehensive description of the mapping between Goeland's internal representations and the TableauxRocq rules, including how variable conditions and Skolem terms are handled. Furthermore, we will elaborate on the testing methodology used to validate the translator, such as running it on a collection of first-order problems and confirming that the checker accepts precisely the proofs output by Goeland. revision: yes

Circularity Check

0 steps flagged

Machine-checked soundness with unverified Goeland translator

full rationale

The paper's core contribution is a deep embedding of free-variable tableaux in Rocq together with a machine-checked soundness proof and modular Skolemization. This rests on Rocq's kernel and does not reduce to self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations. The adaptation of Goeland to emit TableauxRocq certificates is presented as an application whose translator correctness is not separately formalized, but this does not create circularity in the derivation of the embedded calculus itself.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work adds a machine-checked soundness proof rather than new mathematical axioms or parameters; it relies on standard properties of Rocq's type theory and the informal correctness of the original free-variable tableau rules.

axioms (1)
  • standard math Rocq's kernel correctly implements its type theory
    Any deep embedding in Rocq inherits soundness from the proof assistant's trusted kernel.

pith-pipeline@v0.9.0 · 5745 in / 1264 out tokens · 53476 ms · 2026-05-19T18:52:26.994144+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

102 extracted references · 102 canonical work pages

  1. [1]

    Fitting , title =

    M. Fitting , title =. 1996 , edition =

    work page 1996

  2. [2]

    Schlussweisen Kalk

    Sch. Schlussweisen Kalk. Mathematische Annalen. 1950

    work page 1950

  3. [3]

    First-Order Logic

    Smullyan, Raymond M. First-Order Logic. 1968

    work page 1968

  4. [4]

    1979 , issue_date =

    Dershowitz, Nachum and Manna, Zohar , title =. 1979 , issue_date =. doi:10.1145/359138.359142 , journal =

    work page doi:10.1145/359138.359142 1979

  5. [5]

    Logic for Programming, Artificial Intelligence and Reasoning , pages =

    A constraint sequent calculus for first-order logic with linear integer arithmetic , author =. Logic for Programming, Artificial Intelligence and Reasoning , pages =

    work page

  6. [6]

    International Joint Conference on Automated Reasoning , pages =

    Incremental closure of free variable tableaux , author =. International Joint Conference on Automated Reasoning , pages =

    work page

  7. [7]

    Symbolic computation and automated reasoning , pages=

    Using meta-variables for natural deduction in Theorema , author=. Symbolic computation and automated reasoning , pages=. 2001 , publisher=

    work page 2001

  8. [8]

    Journal of Symbolic Computation , volume = 36, number =

    Depth-first proof search without backtracking for free-variable clausal tableaux , author =. Journal of Symbolic Computation , volume = 36, number =

    work page

  9. [9]

    Tableaux , volume=

    The disconnection method: a confluent integration of unification in the analytic framework , author=. Tableaux , volume=

    work page

  10. [10]

    Conference on Automated Deduction (CADE) , pages=

    A confluent connection calculus , author=. Conference on Automated Deduction (CADE) , pages=. 1999 , series=

    work page 1999

  11. [11]

    Hilbert's -Terms in Automated Theorem Proving

    Giese, Martin and Ahrendt, Wolfgang. Hilbert's -Terms in Automated Theorem Proving. Automated Reasoning with Analytic Tableaux and Related Methods. 1999

    work page 1999

  12. [12]

    Cailler, Julie and Rosain, Johann and Delahaye, David and Robillard, Simon and Bouziane, Hinde Lilia , booktitle=. Go

    work page

  13. [13]

    Artificial Intelligence , volume =

    Depth-First Iterative-Deepening: An Optimal Admissible Tree Search. Artificial Intelligence , volume =. 1985 , author =

    work page 1985

  14. [14]

    and Voronkov, Andrei , title =

    Robinson, J. and Voronkov, Andrei , title =. 2001 , isbn =

    work page 2001

  15. [15]

    Communicating Sequential Processes

    Hoare, Charles Antony Richard , journal=. Communicating Sequential Processes. 1978 , publisher=

    work page 1978

  16. [16]

    Formal Language Theory , pages=

    Equations and rewrite rules: A survey , author=. Formal Language Theory , pages=. 1980 , publisher=

    work page 1980

  17. [17]

    2013 , publisher=

    Handbook of tableau methods , author=. 2013 , publisher=

    work page 2013

  18. [18]

    Logic for Programming, Artificial Intelligence and Reasoning , pages =

    Zenon: An extensible automated theorem prover producing checkable proofs , author =. Logic for Programming, Artificial Intelligence and Reasoning , pages =

    work page

  19. [19]

    Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning , editor =

    Johann Rosain and Richard Bonichon and Julie Cailler and Olivier Hermant , title =. Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning , editor =

    work page

  20. [20]

    2000 , isbn =

    Anne Sjerp Troelstra and Helmut Schwichtenberg , title =. 2000 , isbn =

    work page 2000

  21. [21]

    Bonichon, Richard and Hermant, Olivier , title =

    work page

  22. [22]

    1982 , isbn =

    Wolfgang Bibel , title =. 1982 , isbn =

    work page 1982

  23. [23]

    Adding Virtualization Capabilities to the

    Balouek, Daniel and Carpen Amarie, Alexandra and Charrier, Ghislain and Desprez, Fr. Adding Virtualization Capabilities to the. Cloud Computing and Services Science , publisher =. doi:10.1007/978-3-319-04519-1\_1 , year =

    work page doi:10.1007/978-3-319-04519-1

  24. [24]

    The New Rewriting Engine of Dedukti (System Description) , journal =

    Hondet, Gabriel and Blanqui, Frédéric , keywords =. The New Rewriting Engine of Dedukti (System Description) , journal =. 2020 , copyright =. doi:10.4230/LIPICS.FSCD.2020.35 , url =

    work page doi:10.4230/lipics.fscd.2020.35 2020

  25. [25]

    Interoperability of Proof Systems with SC-TPTP , year =

    Guilloud, Simon and Cailler, Julie and Gambhir, Sankalp and Poiroux, Auguste and Herklotz, Yann and Bourgeat, Thomas and Kun. Interoperability of Proof Systems with SC-TPTP , year =. doi:10.1007/978-3-031-99984-0_18 , booktitle =

    work page doi:10.1007/978-3-031-99984-0_18

  26. [26]

    Journal of Automated Reasoning (JAR) , volume = 31, number = 1, pages =

    Dowek, Gilles and Hardin, Thérèse and Kirchner, Claude , title =. Journal of Automated Reasoning (JAR) , volume = 31, number = 1, pages =

    work page

  27. [27]

    , year =

    Sutcliffe, G. , year =. Journal of Automated Reasoning , volume =

    work page

  28. [28]

    Stepping Stones in the TPTP World

    Sutcliffe, G. Stepping Stones in the TPTP World. Proceedings of the 12th International Joint Conference on Automated Reasoning. 2024

    work page 2024

  29. [29]

    Dedukti: a logical framework based on the -calculus modulo theory , author =

    work page

  30. [30]

    16th Annual

    Jeremy Avigad , title =. 16th Annual

    work page

  31. [31]

    Matthias Baaz and Stefan Hetzl and Daniel Weller , title =. J. Symb. Log. , volume =

    work page

  32. [32]

    Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning , series =

    Michael F. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning , series =

    work page

  33. [33]

    Miller , title =

    Dale A. Miller , title =. Stud Logica , volume =

    work page

  34. [34]

    Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller , editor =

    work page

  35. [35]

    Beth, Evert Willem , title =

    work page

  36. [36]

    Societas Philosophica, Acta philosophica Fennica , volume = 8, pages =

    Hintikka, Jaakko , title =. Societas Philosophica, Acta philosophica Fennica , volume = 8, pages =

    work page

  37. [37]

    The even more liberalized -rule in free variable Semantic Tableaux , booktitle =

    Beckert, Bernhard and H. The even more liberalized -rule in free variable Semantic Tableaux , booktitle =. 1993 , publisher =

    work page 1993

  38. [38]

    Hilbert's -Terms in Automated Theorem Proving , booktitle =

    Giese, Martin and Ahrendt, Wolfgang , editor =. Hilbert's -Terms in Automated Theorem Proving , booktitle =. 1999 , publisher =

    work page 1999

  39. [39]

    Matthias Baaz and Christian G. Ferm

    work page

  40. [40]

    Reiner H. J. Autom. Reason. , volume =

    work page

  41. [41]

    Journal of the ACM (JACM) , volume =

    Theorem proving via general matings , author =. Journal of the ACM (JACM) , volume =. 1981 , publisher =

    work page 1981

  42. [42]

    Automated Deduction in Classical and Non-Classical Logics, Selected Papers , series =

    Domenico Cantone and Marianna Nicolosi Asmundo , editor =. Automated Deduction in Classical and Non-Classical Logics, Selected Papers , series =

    work page

  43. [43]

    , author =

    Global Skolemization with Grouped Quantifiers. , author =. APPIA-GULP-PRODE , pages =

    work page

  44. [44]

    Yves Bertot and Pierre Cast

    work page

  45. [45]

    Paulson , title =

    Lawrence C. Paulson , title =. J. Log. Program. , volume =

    work page

  46. [46]

    Journal of Automated Reasoning (JAR) , volume = 59, number = 4, pages =

    Sutcliffe, Geoff , title =. Journal of Automated Reasoning (JAR) , volume = 59, number = 4, pages =

    work page

  47. [47]

    , year =

    Sutcliffe, G. , year =. AI Magazine , volume =

    work page

  48. [48]

    1997 , school =

    The Coq proof assistant reference manual: Version 6.1 , author =. 1997 , school =

    work page 1997

  49. [49]

    2013 , publisher =

    Lambda calculus with types , author =. 2013 , publisher =

    work page 2013

  50. [50]

    Checking Zenon modulo proofs in Dedukti , author =

    work page

  51. [51]

    14th International Conference on Interactive Theorem Proving , year =

    LISA--A Modern Proof System , author =. 14th International Conference on Interactive Theorem Proving , year =

    work page

  52. [52]

    2002 , publisher=

    Isabelle/HOL: a proof assistant for higher-order logic , author=. 2002 , publisher=

    work page 2002

  53. [53]

    A verified prover based on ordered resolution , booktitle =

    Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel , editor =. A verified prover based on ordered resolution , booktitle =

    work page

  54. [54]

    A Brief Overview of Agda -- A Functional Language with Dependent Types

    Bove, Ana and Dybjer, Peter and Norell, Ulf. A Brief Overview of Agda -- A Functional Language with Dependent Types. Theorem Proving in Higher Order Logics. 2009

    work page 2009

  55. [55]

    International Conference on Intelligent Computer Mathematics , pages=

    Mizar: State-of-the-art and beyond , author=. International Conference on Intelligent Computer Mathematics , pages=. 2015 , organization=

    work page 2015

  56. [56]

    TPTP, TSTP, CASC, etc

    Sutcliffe, G. TPTP, TSTP, CASC, etc. Proceedings of the 2nd International Computer Science Symposium in Russia. 2007

    work page 2007

  57. [57]

    Journal of Automated Reasoning , volume=

    On the generation of quantified lemmas , author=. Journal of Automated Reasoning , volume=. 2019 , publisher=

    work page 2019

  58. [58]

    Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, LPAR-18, M

    Towards algorithmic cut-introduction , author=. Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, LPAR-18, M. 2012 , organization=

    work page 2012

  59. [59]

    A constructive proof of Skolem theorem for constructive logic , author=

    work page

  60. [60]

    Dirk van Dalen , title =

    work page

  61. [61]

    Journal of Automated Reasoning , volume =

    A Sound Framework for -Rule Variants in Free-Variable Semantic Tableaux , author =. Journal of Automated Reasoning , volume =. 2007 , publisher =

    work page 2007

  62. [62]

    International Conference on Theorem Proving in Higher Order Logics , year=

    A Structured Set of Higher-Order Problems , author=. International Conference on Theorem Proving in Higher Order Logics , year=

    work page

  63. [63]

    Über eine Schlussweise aus dem Endlichen ins Unendliche , author=

    work page

  64. [64]

    First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice , journal =

    Guillaume Burel and Guillaume Bury and Rapha. First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice , journal =

    work page

  65. [65]

    Free-Variable Tableaux for Propositional Modal Logics , journal =

    Bernhard Beckert and Rajeev Gor. Free-Variable Tableaux for Propositional Modal Logics , journal =. 2001 , url =. doi:10.1023/A:1013886427723 , timestamp =

    work page doi:10.1023/a:1013886427723 2001

  66. [66]

    Higher-Order Tableaux , booktitle =

    Michael Kohlhase , editor =. Higher-Order Tableaux , booktitle =. 1995 , url =. doi:10.1007/3-540-59338-1\_43 , timestamp =

    work page doi:10.1007/3-540-59338-1 1995

  67. [67]

    Leo Bachmair and Harald Ganzinger , title =. J. Log. Comput. , volume =. 1994 , url =. doi:10.1093/LOGCOM/4.3.217 , timestamp =

    work page doi:10.1093/logcom/4.3.217 1994

  68. [68]

    Lyaletski , editor =

    Boris Konev and Alexander V. Lyaletski , editor =. Tableau Method with Free Variables for Intuitionistic Logic , booktitle =. 2006 , url =. doi:10.1007/3-540-33521-8\_15 , timestamp =

    work page doi:10.1007/3-540-33521-8 2006

  69. [69]

    N. G. de Bruijn , title =. Indagationes Mathematicae , volume =. 1972 , publisher =

    work page 1972

  70. [70]

    The Locally Nameless Representation , url =

    Arthur Chargu. The Locally Nameless Representation , journal =. 2012 , url =. doi:10.1007/S10817-011-9225-2 , timestamp =

    work page doi:10.1007/s10817-011-9225-2 2012

  71. [71]

    Journal of the ACM (JACM) , volume =

    A machine-oriented logic based on the resolution principle , author =. Journal of the ACM (JACM) , volume =. 1965 , publisher =

    work page 1965

  72. [72]

    , author =

    Paramodulation-Based Theorem Proving. , author =. Handbook of automated reasoning , volume =

    work page

  73. [73]

    International Workshop on Theorem Proving with Analytic Tableaux and Related Methods , pages =

    Incremental theory reasoning methods for semantic tableaux , author =. International Workshop on Theorem Proving with Analytic Tableaux and Related Methods , pages =. 1996 , organization =

    work page 1996

  74. [74]

    International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , pages =

    Integrating simplex with tableaux , author =. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , pages =. 2015 , organization =

    work page 2015

  75. [75]

    International Conference on Logic for Programming Artificial Intelligence and Reasoning , pages =

    Zenon modulo: When achilles outruns the tortoise using deduction modulo , author =. International Conference on Logic for Programming Artificial Intelligence and Reasoning , pages =. 2013 , organization =

    work page 2013

  76. [76]

    Journal of Automated Reasoning , volume =

    First-order automated reasoning with theories: when deduction modulo theory meets practice , author =. Journal of Automated Reasoning , volume =. 2020 , publisher =

    work page 2020

  77. [77]

    arXiv preprint arXiv:2503.15541 , year =

    Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo , author =. arXiv preprint arXiv:2503.15541 , year =

    work page arXiv

  78. [78]

    16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =

    Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL , author =. 16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =. 2025 , organization =

    work page 2025

  79. [79]

    International Conference on Automated Deduction , pages =

    Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories , author =. International Conference on Automated Deduction , pages =

    work page

  80. [80]

    Journal of Automated Reasoning , volume =

    leanTAP: Lean tableau-based deduction , author =. Journal of Automated Reasoning , volume =

    work page

Showing first 80 references.