Pith. sign in

REVIEW 3 major objections 4 minor 53 references

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

T0 review · 3 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper specifies SC-TPTP, an extension of the TPTP derivation format that makes sequent-calculus proofs from automated provers mechanically checkable and exportable to Coq.

desk verdict SC-TPTP is a sensible, well-scoped proposal for a sequent-proof interchange format; the format deserves referee time, but the Coq export is not yet shown sound. read the letter →

arxiv 2507.11349 v1 pith:FFS7AIZV submitted 2025-07-15 cs.LO

Julie Cailler , Simon Guilloud This is my paper · ORCID
classification cs.LO MSC 03B3568V15
keywords TPTPsequentcalculusproofformatinteroperabilityautomatedtheoremprovinginteractivecongruenceclosureCoqexport
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper claims that a common derivation format for sequent-based proofs can be built by over-specifying the existing TPTP derivation format, fixing what TPTP leaves open: how each proof step was derived. SC-TPTP defines two levels of steps, thirty low-level sequent-calculus rules that are complete for first-order logic with equality and easy to verify, plus higher-level steps such as congruence closure that come with procedures to unfold them into low-level steps. The authors implement a library that parses, prints, checks, and transforms SC-TPTP proofs, exports them to Coq, and wire the format into the Lisa proof assistant and the Goéland automated prover. If the format is sound and adopted, proof exchange between sequent-based systems becomes a matter of one import and one export per tool, and ATP answers become unambiguously verifiable.

What carries the argument

The machinery is the two-level derivation-step system. Level 1 is a fixed set of thirty rules whose parameters are indices into the sequent, so checking a step reduces to comparing sets of formulas, and level 2 is an extensible set of advanced steps for which an elimination algorithm produces a level 1 derivation. The proof-producing e-graph, an equivalence-class data structure for terms under equalities and congruence, is the object that turns a congruence-closure justification into explicit equality edges and, recursively, into substitution proofs.

What would settle it

A concrete test is to run the library's Coq export on level 1 SC-TPTP proofs of classically valid but intuitionistically invalid sequents such as Peirce's formula and check whether the generated theorem, after stripping the double-negation encoding, is provably equivalent to the original sequent for every rule; the paper's own displayed Drinker theorem is double-negated, so the soundness of that encoding for general proofs is the crux.

Watch

Extended reading notes

Core claim

The central claim is that a proof format can be faithful to mathematical tradition and still mechanically checkable if it pins down the meaning of every derivation step. SC-TPTP derivations are lists of TPTP-annotated statements whose formulas may be sequents, and each inference names a rule from a fixed table together with parameters, mostly indices, that make verification a set-comparison check rather than a search. Level 1 rules cover structural rules, left and right introduction of connectives and quantifiers, negated forms, and equality; level 2 rules, here negation normal form, simultaneous substitution, and congruence, are justified by elimination algorithms that unfold them into level 1 derivations. The implemented pipeline lets Lisa pose a conjecture, have Goéland return an SC-TPTP proof, check it, unfold congruence steps using an e-graph with an explain method, and export the result to Coq.

Load-bearing premise

The load-bearing assumption is that the Coq translation is sound: every SC-TPTP rule, including the double-negated and inverted versions used because Coq is intuitionistic, is faithfully represented by the supplied Coq lemmas, so a Coq-accepted proof really proves the original sequent.

Editorial extensions

If this is right

  • If SC-TPTP is adopted, every sequent-based tool needs only one SC-TPTP import and one export, replacing pairwise translation between every pair of systems.
  • Automated theorem prover answers for first-order problems can be verified unambiguously, since each step carries enough parameters to be checked without inference.
  • Users of Lisa can call Goéland as a proof-producing tactic and obtain proofs that are reconstructed inside Lisa's kernel.
  • Sequent-style proofs can be exported to Coq, and level 2 steps such as congruence can be eliminated into level 1 steps, making advanced ATP reasoning digestible for proof assistants.
  • The format is extensible by design: level 2 rules such as NNF are anticipated, so tools can keep their native high-level steps and eliminate only what their target cannot consume.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the same two-level design would likely extend to typed first-order logic: adding types to the rule parameters would make some checks more involved but would not change the set-comparison principle.
  • Beyond the paper, the Coq export could be turned into a fully verified translation by mechanically proving that the double-negation and inversion lemmas used for right and left rules are logically equivalent to the original sequent rules.
  • Beyond the paper, adding deskolemization as a level 2 step, as the conclusion suggests, would allow tableaux proofs with on-the-fly Skolem terms to be unfolded into level 1 derivations and would remove a major obstacle to importing such proofs.
  • Beyond the paper, the DRAT experience in SAT suggests that the main barrier for SC-TPTP is adoption rather than expressiveness, so an independent lightweight checker built by a third party would be a natural next step to build trust in the format.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes SC-TPTP, an extension of the TPTP derivation format intended for sequent-based first-order logic proofs. It defines two levels of derivation steps: 30 level-1 rules (structural, left/right introduction, left-negation, and equality rules) and three level-2 steps (NNF, congruence, and simultaneous substitution), with sequents interpreted as sets of formulas. The paper also describes a Scala library that parses, prints, checks, unfolds congruence steps, and exports proofs to Coq, together with an integration in which the Lisa proof assistant queries the Goéland ATP and imports SC-TPTP proofs. The central claims are that the format is precise, mechanically checkable, and interoperable, and that the provided tools realize these properties.

Significance. The proposal addresses a real interoperability need and has the virtue of building on the widely used TPTP syntax. The set-based semantics and explicit per-rule parameters simplify checking, and the public implementation, the proof-producing e-graph, and the working Lisa--Goéland integration are concrete artifacts that give the paper practical weight. If the soundness gaps identified below are resolved, SC-TPTP could become a useful common format for exchanging first-order sequent proofs. The level-1 rule set is standard, but the paper currently lacks the formal translation and soundness theorems needed to substantiate the Coq-export contribution and to guarantee that the format itself is sound as specified.

major comments (3)
  1. [Section 4.1, Examples 4.1-4.5] The Coq export is not defined as a translation on arbitrary SC-TPTP sequents and proofs. The displayed `Theorem drinker` proves `~(~(exists X, d X -> forall Y, d Y))`, while the original SC-TPTP conjecture in Example 3.2 is the positive formula `(? [X] : d(X) => (! [Y] : d(Y)))`. The paper does not state that exported proofs concern double-negated statements, does not list the classical axioms (e.g., `NNPP`, `classic`) on which the generated Coq scripts depend, and does not explain how multi-formula succedents, `cut`, or the `_s` inversion lemmas are composed into a full proof translation. Without a soundness statement relating SC-TPTP provability to Coq provability under the described translation, the contribution "export them into Coq files" is unverified.
  2. [Section 3.2, Tables 2 and 4] The `leftEx` and `leftNotAll` rules omit the eigenvariable (freshness) side condition. In standard LK, the rule `Γ, A(y) ⊢ Δ ⇒ Γ, ∃x.A(x) ⊢ Δ` is sound only when `y` does not occur free in `Γ, Δ`; the same freshness condition is required for `leftNotAll`. The surrounding text in Section 3.2 mentions a freshness check only for `rightAll` (step s3), so a checker implementing the tables literally would accept unsound derivations. This is a soundness gap in the proposed format itself and must be fixed in the rule definitions and in the checker.
  3. [Section 4.2] The e-graph-based unfolding of `congruence` steps is described only informally. No theorem states that the `explain` method always terminates, that the returned equality path is acyclic, or that its recursive expansion produces a valid sequence of level-1 `leftSubst`/`rightSubst` steps preserving the original sequent. Since eliminating level-2 steps in favor of low-level steps is a stated contribution, the unfolding procedure needs a precise correctness invariant and a proof that the constructed level-1 proof is well-formed.
minor comments (4)
  1. [Table 4] The parameter descriptions for `leftNotEx` and `leftNotAll` say the index points to the formula "on the right" of the conclusion; both rules are left-introduction rules, so this should read "on the left".
  2. [Example 3.2 vs. Table 4] Example 3.2 uses the rule name `leftNotForall`, while Table 4 names the same rule `leftNotAll`. The names should be harmonized and the example should parse against the published rule set.
  3. [Section 3.2, leftSubst example] The `leftSubst` derivation example appears to refer to `s1` as its own premise and contains a malformed parameter list (an extra closing parenthesis after `$fot(Z))`). It should refer to the axiom `a1` and use correct SC-TPTP syntax.
  4. [Section 3.2, completeness claim] The statement that the 30 rules are "complete for first order logic with equality" is asserted without proof or citation; since the paper is primarily about a format rather than a new calculus, this claim should be backed by a reference or softened to "complete for the usual LK-style presentation".

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: SC-TPTP is a proposed format with independent rule tables and a checker; the Coq export gap is a correctness concern, not a circular derivation.

full rationale

The paper's central contribution is a specification of an extension to the TPTP derivation format, not an empirically calibrated prediction or a theorem derived from prior work by the same authors. The SC-TPTP level 1 and level 2 rules are explicitly enumerated in Tables 1 through 6 with stated semantics, and the library is described as containing a parser, printer, and proof checker for the format. The use of the authors' own Goéland and Lisa systems is integration context: the format is implemented as import/export in those tools, but the format's definition does not reduce to those implementations. The Coq export section claims a 'one-to-one mapping' between SC-TPTP rules and Coq lemmas and illustrates it with examples; the absence of a formal soundness statement for that translation is a verification gap or correctness risk, not a circular step, because the export procedure is not an input to the definition of the format or to the validity checker. No derivation is fitted to data, and no assertion is justified solely by a self-citation chain. The paper is honest about being a 'proof of concept and a proposal to the community', and no load-bearing argument is equivalent by construction to its own inputs.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper fits no empirical parameters. Its background assumptions are standard sequent calculus facts plus three paper-specific choices: set semantics, reuse of the FOFX grammar, and the soundness of the Coq and e-graph translation algorithms. There are no invented physical or mathematical entities; SC-TPTP and its rules are syntactic artifacts with a public implementation.

assumptions (5)
  • standard math The 30 level 1 inference rules are sound and complete for classical first-order logic with equality.
    Invoked in Section 3.2 where the paper states 'Those rules are complete for first order logic with equality.' This is a standard textbook result for sequent calculus, but no proof tailored to the chosen set semantics is included.
  • domain assumption Sequents are identified with sets of formulas, so order and multiplicity of formulas are irrelevant.
    Section 3 states 'This is the semantic we chose for SC-TPTP.' This is a design choice, not something forced by TPTP or by the original Gentzen presentation.
  • domain assumption The TPTP FOFX grammar supports sequents and free variables even though TPTP itself does not allow free variables.
    Figure 2 and Section 3.1 rely on FOFX, which the paper describes as defined but 'not yet in use'. The paper asserts that the grammar supports free variables without providing an external citation or a formal grammar fragment.
  • ad hoc to paper The Coq export translation, including its double-negation and inversion lemmas, preserves the provability of SC-TPTP sequents.
    Section 4.1 maps each SC-TPTP rule to a Coq lemma and illustrates the translation, but no soundness theorem is stated. Example 4.5 proves a double-negated version of the Drinker formula, so the translation target is not made explicit.
  • ad hoc to paper The e-graph based algorithm of Section 4.2 correctly unfolds every congruence step into low-level substitution steps.
    The algorithm is described using union-find with an explain method, but the paper gives no correctness proof that the generated equality paths correspond to valid applications of leftSubst and rightSubst.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus." pith.science (2026). https://pith.science/paper/FFS7AIZV

@misc{pith2026250711349,
  author       = {Pith},
  title        = {Pith review of: SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FFS7AIZV}},
  note         = {Machine review of arXiv:2507.11349}
}
read the original abstract

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-order logic: SC-TPTP. To avoid multiplication of standards, our proposed format over-specifies the TPTP derivation format by focusing on sequent formalisms. By doing so, it provides a high level of detail, is faithful to mathematical tradition, and cover multiple existing tools and in particular tableaux-based strategies. We make use of this format to allow the Lisa proof assistant to query the Go\'eland automated theorem prover, and implement a library of tools able to parse, print and check SC-TPTP proofs, export them into Coq files, and rebuild low-level proof steps from advanced ones.

Figures

Figures reproduced from arXiv: 2507.11349 by the authors.

Figure 1
Figure 1. Standards (xkcd — https://xkcd.com/927/). Licensed under CC BY-NC 2.5 License (https: //creativecommons.org/licenses/by-nc/2.5/) unifying the syntax and proofs of arbitrarily many systems with unrelated foundations is overly ambitious and may not be practically feasible. A successful approach needs to convey the right level of abstraction, neither too specific nor too general. This introduction may remind the reader… view at source ↗
Figure 2
Figure 2. Main elements of the SC-TPTP syntax. logic_formula is the FOF syntax for logical formulas. For SC-TPTP derivations, annotations are of the form inference(rule, [parameters], [premises]). In the original presentation of Gentzen, sequents’ sides are formally lists of formulas, where order and number of duplicates are significant. This semantics requires additional structural rules for contraction and permutation of fo… view at source ↗
Figure 3
Figure 3. Use cases of SC-TPTP An e-graph is built on top of a Union-Find data structure, which maintains an equivalence class of terms under a given set of equality (which in an e-graph are either the input equalities or equalities that follow from congruence). To produce SC-TPTP proofs, our Union-Find data structure is equipped with an explain method, as in [41], which when prompted to explain 𝑎 = 𝑐 outputs a path (𝑎, 𝑏1),(… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 39 canonical work pages

  1. [1]

    Sutcliffe, The logic languages of the TPTP world, Logic Journal of the IGPL 31 (2023) 1153–1169

    G. Sutcliffe, The logic languages of the TPTP world, Logic Journal of the IGPL 31 (2023) 1153–1169. doi:10.1093/jigpal/jzac068

    doi:10.1093/jigpal/jzac068 2023

  2. [2]

    Guilloud, S

    S. Guilloud, S. Gambhir, V. Kuncak, LISA – A Modern Proof System, in: 14th Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, Daghstuhl, Bialystok, 2023, pp. 17:1–17:19

    2023

  3. [3]

    Cailler, J

    J. Cailler, J. Rosain, D. Delahaye, S. Robillard, H. L. Bouziane, Goéland: A Concurrent Tableau-Based Theorem Prover (System Description), in: J. Blanchette, L. Kovács, D. Pat- tinson (Eds.), Automated Reasoning, Lecture Notes in Computer Science, Springer Interna- tional Publishing, Cham, 2022, pp. 359–368. doi:10.1007/978-3-031-10769-6_22

    doi:10.1007/978-3-031-10769-6_22 2022

  4. [4]

    Kohlhase, F

    M. Kohlhase, F. Rabe, Experiences from Exporting Major Proof Assistant Libraries, Journal of Automated Reasoning 65 (2021) 1265–1298. doi:10.1007/s10817-021-09604-0

    doi:10.1007/s10817-021-09604-0 2021

  5. [5]

    Barbosa, C

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar, Cvc5: A Versatile and Industrial-Strength SMT Solver, in: D. Fisman, G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, volume 13243, Springer...

    doi:10.1007/978-3-030-99524-9_24 2022

  6. [6]

    Assaf, G

    A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halma- grand, O. Hermant, R. Saillard, Dedukti: a logical framework based on the 𝜆𝜋-calculus modulo theory (2016)

    work page 2016

  7. [7]

    Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Auto- mated Reasoning 59 (2017) 483–502

    G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Auto- mated Reasoning 59 (2017) 483–502. doi:10.1007/s10817-017-9407-7

    doi:10.1007/s10817-017-9407-7 2017

  8. [8]

    Böhme, T

    S. Böhme, T. Weber, Designing proof formats: A user’s perspective—experience report, in: First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011

    work page 2011

Show all 53 references
  1. [9]

    Reger, M

    G. Reger, M. Suda, Checkable proofs for first-order theorem proving., in: ARCADE@ CADE, 2017, pp. 55–63

    2017

  2. [10]

    Wetzler, M

    N. Wetzler, M. J. Heule, W. A. Hunt Jr, Drat-trim: Efficient checking and trimming using expressive clausal proofs, in: International Conference on Theory and Applications of Satisfiability Testing, Springer, 2014, pp. 422–429

    2014

  3. [11]

    Cruz-Filipe, M

    L. Cruz-Filipe, M. J. Heule, W. A. Hunt, M. Kaufmann, P. Schneider-Kamp, Efficient certified rat verification, in: Automated Deduction–CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings, Springer, 2017, pp. 220–236

    2017

  4. [12]

    Stump, D

    A. Stump, D. Oe, Towards an smt proof format, in: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on bit-precise reasoning, 2008, pp. 27–32

    2008

  5. [13]

    Barbosa, C

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mo- hamed, A. Niemetz, A. Nötzli, et al., cvc5: A versatile and industrial-strength smt solver, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ...

    2022

  6. [14]

    De Moura, N

    L. De Moura, N. Bjørner, Z3: An efficient smt solver, in: International conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp. 337–340

    2008

  7. [15]

    L. M. de Moura, N. S. Bjørner, Proofs and refutations, and z3., in: LPAR Workshops, volume 418, Doha, Qatar, 2008, pp. 123–132

    2008

  8. [16]

    Besson, P

    F. Besson, P. Fontaine, L. Théry, A flexible proof format for smt: A proposal, in: First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011

    2011

  9. [17]

    Hoenicke, T

    J. Hoenicke, T. Schindler, A simple proof format for smt., in: SMT, 2022, pp. 54–70

    2022

  10. [18]

    Schurr, M

    H.-J. Schurr, M. Fleury, H. Barbosa, P. Fontaine, Alethe: Towards a generic smt proof format, arXiv preprint arXiv:2107.02354 (2021)

    2021 arXiv

  11. [19]

    Bouton, D

    T. Bouton, D. Caminha B. de Oliveira, D. Déharbe, P. Fontaine, verit: an open, trustable and efficient smt-solver, in: International Conference on Automated Deduction, Springer, 2009, pp. 151–156

    2009

  12. [20]

    Otten, S

    J. Otten, S. Holden, A syntax for connection proofs (2023)

    2023

  13. [21]

    Otten, W

    J. Otten, W. Bibel, leancop: lean connection-based theorem proving, Journal of Symbolic Computation 36 (2003) 139–161

    2003

  14. [22]

    S. B. Holden, Connect++: A New Automated Theorem Prover Based on the Connection Calculus, in: J. Otten, W. Bibel (Eds.), Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) Affiliated with the 32nd International Conference...

    2023

  15. [23]

    Baek, The tesc proof format for first-order atps, 2020

    S. Baek, The tesc proof format for first-order atps, 2020

    2020

  16. [24]

    Kovács, A

    L. Kovács, A. Voronkov, First-order theorem proving and vampire, in: International Conference on Computer Aided Verification, Springer, 2013, pp. 1–35

    2013

  17. [25]

    Schulz, S

    S. Schulz, S. Cruanes, P. Vukmirović, Faster, higher, stronger: E 2.3, in: Automated Deduction–CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings 27, Springer, 2019, pp. 495–507

    2019

  18. [26]

    Sutcliffe, Semantic derivation verification: Techniques and implementation, Interna- tional Journal on Artificial Intelligence Tools 15 (2006) 1053–1070

    G. Sutcliffe, Semantic derivation verification: Techniques and implementation, Interna- tional Journal on Artificial Intelligence Tools 15 (2006) 1053–1070

    2006

  19. [27]

    Willsey, C

    M. Willsey, C. Nandi, Y. R. Wang, O. Flatt, Z. Tatlock, P. Panchekha, Egg: Fast and extensible equality saturation, Proceedings of the ACM on Programming Languages 5 (2021) 23:1–23:29. doi:10.1145/3434304

    2021 doi

  20. [28]

    Gentzen, Untersuchungen über das logische Schließen I, Mathematische Zeitschrift 39 (1935) 176–210

    G. Gentzen, Untersuchungen über das logische Schließen I, Mathematische Zeitschrift 39 (1935) 176–210

    1935

  21. [29]

    Gentzen, Untersuchungen über das logische schließen

    G. Gentzen, Untersuchungen über das logische schließen. ii., Mathematische zeitschrift 39 (1935)

    1935

  22. [30]

    Rümmer, A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic, in: I

    P. Rümmer, A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic, in: I. Cervesato, H. Veith, A. Voronkov (Eds.), Logic for Programming, Arti- ficial Intelligence, and Reasoning, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2008...

    2008 doi

  23. [31]

    Bonichon, D

    R. Bonichon, D. Delahaye, D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, in: N. Dershowitz, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, volume 4790, Springer Berlin Heidelberg, Berlin, Heidelberg, 20...

    2007 doi

  24. [32]

    Delahaye, D

    D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, in: D. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg, F. Mattern, J. C. Mitchell, M. Naor, O. Nierstrasz, C. Pandu Rangan, B. Steffen, M...

    2013

  25. [33]

    Beckert, J

    B. Beckert, J. Posegga, LeanTAP: Lean tableau-based theorem proving, in: A. Bundy (Ed.), Automated Deduction — CADE-12, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1994, pp. 793–797. doi:10.1007/3-540-58156-1_62

    1994 doi

  26. [34]

    A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, 2 ed., Cambridge University Press, Cambridge, 2000. doi: 10.1017/ CBO9781139168717

  27. [35]

    Harrison, HOL Light: An Overview, in: S

    J. Harrison, HOL Light: An Overview, in: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (Eds.), Theorem Proving in Higher Order Logics, volume 5674, Springer Berlin Heidelberg, Berlin, Heidelberg, 2009, pp. 60–66. doi:10.1007/978-3-642-03359-9_4

    2009 doi

  28. [36]

    Sutcliffe, The szs ontologies for automated reasoning software., in: LPAR Workshops, volume 418, Citeseer, 2008

    G. Sutcliffe, The szs ontologies for automated reasoning software., in: LPAR Workshops, volume 418, Citeseer, 2008

    2008

  29. [37]

    R. M. Smullyan, What is the name of this book? The riddle of Dracula and other logical puzzles, Englewood Cliffs, N.J. : Prentice-Hall, 1978

    1978

  30. [38]

    Maziarz, T

    K. Maziarz, T. Ellis, A. Lawrence, A. Fitzgibbon, S. P. Jones, Hashing Modulo Alpha- Equivalence (2021) 17

    2021

  31. [39]

    J. H. Gallier, S. Raatz, W. Snyder, Theorem Proving Using Rigid E-Unification Equational Matings, in: Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987, IEEE Computer Society, 1987, pp. 338–346

    1987

  32. [40]

    Degtyarev, A

    A. Degtyarev, A. Voronkov, What you always wanted to know about rigid e-unification, Journal of Automated Reasoning 20 (1998) 47–80

    1998

  33. [41]

    Nieuwenhuis, A

    R. Nieuwenhuis, A. Oliveras, Proof-Producing Congruence Closure, in: J. Giesl (Ed.), Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, Springer, 2005, pp. 453...

    2005 doi

  34. [42]

    Cailler, Designing an Automated Concurrent Tableau-Based Theorem Prover for First- Order Logic, Ph.D

    J. Cailler, Designing an Automated Concurrent Tableau-Based Theorem Prover for First- Order Logic, Ph.D. thesis, Université de Montpellier, 2023

    2023

  35. [43]

    Dowek, T

    G. Dowek, T. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning 31 (2003) 33–72

    2003

  36. [44]

    Guilloud, M

    S. Guilloud, M. Bucev, D. Milovancevic, V. Kuncak, Formula Normalizations in Verification, in: 35th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer, Paris, 2023, pp. 398–422

    2023

  37. [45]

    Guilloud, V

    S. Guilloud, V. Kuncak, Orthologic with Axioms, 2023. doi:10.48550/arXiv.2307.07569. arXiv:2307.07569

    2023 doi arXiv

  38. [46]

    P. Rümmer, A constraint sequent calculus for first-order logic with linear integer arithmetic, in: Proceedings, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 5330 of LNCS, Springer, 2008, pp. 274–289

    2008

  39. [47]

    Otten, Connection Calculi for Automated Theorem Proving in Classical and Non-Classical Logics, Ph.D

    J. Otten, Connection Calculi for Automated Theorem Proving in Classical and Non-Classical Logics, Ph.D. thesis, University of Potsdam, 2013

    2013

  40. [48]

    Kaliszyk, Efficient Low-Level Connection Tableaux, in: H

    C. Kaliszyk, Efficient Low-Level Connection Tableaux, in: H. De Nivelle (Ed.), Auto- mated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Com- puter Science, Springer International Publishing, Cham, 2015, pp. 102–111. doi:10.1007/ 978-3-319-24312-2_8

    2015

  41. [49]

    J. C. Blanchette, A. Paskevich, Tff1: The tptp typed first-order form with rank-1 polymor- phism, in: Automated Deduction–CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings 24, Springer, 2013, pp. 414–420

    2013

  42. [50]

    Bonichon, O

    R. Bonichon, O. Hermant, A Syntactic Soundness Proof for Free-Variable Tableaux with on-the-fly Skolemization, 2013

    2013

  43. [51]

    Rosain, R

    J. Rosain, R. Bonichon, J. Cailler, O. Hermant, A generic deskolemization strategy, in: Logic for Programming, Artificial Intelligence, and Reasoning: 25th International Conference, LPAR-25, Balaclava, Mauritius, May 26-31, 2024. Proceedings 25, Springer, 2024

    2024

  44. [52]

    Nipkow, M

    T. Nipkow, M. Wenzel, L. C. Paulson, Isabelle/HOL: a proof assistant for higher-order logic, Springer, 2002

    2002

  45. [53]

    Avigad, L

    J. Avigad, L. De Moura, S. Kong, Theorem proving in lean, Release 3 (2015) 1–4

    2015

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.