pith. sign in

arxiv: 2605.20054 · v1 · pith:6WXKAIIQnew · submitted 2026-05-19 · 💻 cs.LO

Automating proof search when equality is a logical connective

Kaustuv Chaudhuri , Arunava Gantait , Dale Miller This is my paper

Pith reviewed 2026-05-20 03:33 UTC · model grok-4.3

classification 💻 cs.LO
keywords equalitylogical connectivesequent calculusunificationproof searchquantifier alternationfirst-order logic
0
0 comments X

The pith

An extended unification procedure automates proof search when equality is treated as a logical connective in sequent calculi.

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

The paper develops a proof search procedure for sequent calculi that introduce syntactic equality directly through left and right introduction rules. This treatment supports deriving basic mathematical facts such as Peano axioms without induction. The procedure extends unification to cover quantifier alternations and equations in both positive and negative positions. A reader would care because the method fills a gap between interactive systems that use this equality and automated search tools that previously lacked direct support for it.

Core claim

The central claim is that extending unification to all cases of quantifier alternation and both positive and negative occurrences of equations yields a complete and consistent proof search procedure for first-order sequent calculi that treat equality as a logical connective.

What carries the argument

The unification-aware proof search procedure that extends standard unification across quantifier alternations and positive/negative equation occurrences.

If this is right

  • The method supports unification-aware search across a range of first-order sequent calculi.
  • It enables a lightweight logical framework that directly uses this form of equality.
  • Derivations of core principles such as Peano axioms become available inside automated search.
  • The approach addresses the lack of direct support for this equality in systems such as lambdaProlog and LF.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same extension might transfer to other introduction-rule-based connectives beyond equality.
  • An implementation could be checked for completeness on standard first-order equality examples.
  • The technique may reduce the need for separate equality axioms in certain logical frameworks.

Load-bearing premise

The procedure correctly extends unification to every combination of quantifier alternation and equation polarity without creating incompleteness or inconsistency.

What would settle it

A concrete sequent containing alternating quantifiers and mixed-polarity equations for which the procedure either misses an existing proof or accepts an invalid one.

Figures

Figures reproduced from arXiv: 2605.20054 by Arunava Gantait, Dale Miller, Kaustuv Chaudhuri.

Figure 1
Figure 1. Figure 1: The inference rules for the LJ = ω proof system • Sequents in LJ = ω will be of the form Σ:: Γ ⊢ C, where Γ (the assumptions) is a set of formulas, C is a formula, and Σ is explained below. The context Γ of assumptions is treated as a set instead of a multiset or a list. Thus, the structural rules of weakening, contraction, and exchange are admissible and therefore unnecessary. • The typed eigenvariables i… view at source ↗
Figure 2
Figure 2. Figure 2: A faithful specification of LJ = 1 as an object logic (compare with [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
read the original abstract

Treating syntactic equality as a logical connective -- governed by left- and right-introduction rules within the sequent calculus -- offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano's axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as $\lambda$Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality.

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 / 3 minor

Summary. The paper presents a proof search procedure for first-order sequent calculi in which equality is treated as a logical connective with explicit left- and right-introduction rules. The central contribution is an extension of unification that handles quantifier alternation and equations in both positive and negative positions while preserving sequent calculus invariants. The manuscript supplies the inference rules for the extended procedure together with a termination argument based on a lexicographic measure combining the multiset of goals and the depth of quantifier nesting.

Significance. If the procedure is terminating and complete for the stated fragment, the result would enable unification-aware automated proof search in lightweight logical frameworks that directly support equality as a connective, addressing a documented gap relative to systems such as λProlog and LF. The explicit construction of inference rules and the termination argument based on a lexicographic measure on goals and quantifier depth constitute concrete strengths that support the central claim.

major comments (1)
  1. [§4.2] §4.2 (Unification extension): the claim that the procedure correctly handles all quantifier alternations for negative equation occurrences rests on the preservation of sequent invariants, yet the manuscript does not exhibit a derivation showing how the new rules interact with ∀-L when the equation is introduced after quantifier movement; this case is load-bearing for the completeness argument.
minor comments (3)
  1. [§3] The notation distinguishing positive and negative equation occurrences is introduced in §3 without a small worked example that displays both polarities in the same sequent; adding one would improve readability.
  2. [Table 1] Table 1 (example derivations) reports success on a Peano axiom fragment but does not list the number of unification steps or the final measure value; including these would make the termination claim easier to inspect.
  3. [Introduction] The reference list omits the original Abella paper on equality as a connective; adding it would strengthen the positioning in the introduction.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and positive evaluation of the manuscript. The single major comment identifies a useful way to make the completeness argument more explicit, and we address it directly below.

read point-by-point responses

  1. Referee: §4.2 (Unification extension): the claim that the procedure correctly handles all quantifier alternations for negative equation occurrences rests on the preservation of sequent invariants, yet the manuscript does not exhibit a derivation showing how the new rules interact with ∀-L when the equation is introduced after quantifier movement; this case is load-bearing for the completeness argument.

    Authors: We agree that an explicit derivation would make the interaction between the extended unification rules and ∀-L clearer for negative equation occurrences after quantifier movement. The manuscript already states that the rules are designed to preserve sequent invariants, but we acknowledge that a concrete step-by-step derivation for this specific case would strengthen the completeness argument. In the revised version we will insert such a derivation in §4.2, showing how the new rules apply while maintaining the required invariants. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper constructs a unification-aware proof search procedure for sequent calculi treating equality as a logical connective by explicitly extending standard unification with new introduction rules for equations and quantifier movements. It supplies the inference rules directly and proves termination via a lexicographic measure on goals and quantifier depth, preserving sequent invariants. No load-bearing step reduces by definition or self-citation to its own inputs; the derivation is self-contained with independent content against the stated fragment.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The abstract relies on standard sequent-calculus rules for equality introduction and on the assumption that unification can be extended without breaking cut-elimination or other meta-properties; no free parameters or invented entities are mentioned.

axioms (1)
  • domain assumption Sequent calculus admits left and right introduction rules for syntactic equality as a logical connective.
    Stated in the opening sentence of the abstract as the foundation for deriving Peano axioms.

pith-pipeline@v0.9.0 · 5675 in / 1287 out tokens · 31162 ms · 2026-05-20T03:33:45.380151+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

  1. [1]

    Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: A sys- tem for reasoning about relational specifications. J. of Formalized Reasoning7(2), 1–89 (2014). DOI: 10.6092/issn.1972-5787/4650

    work page doi:10.6092/issn.1972-5787/4650 2014

  2. [2]

    In: Pfenning, F

    Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) 21th Conf. on Automated Deduction (CADE). pp. 391–397. No. 4603 in LNAI, Springer, New York (2007). DOI: 10.1007/978-3-540-73595-3_28, https://www.lix.polytechnique. fr/Labo/Dale.Miller/papers/cade2007.pdf 11

    work page doi:10.1007/978-3-540-73595-3_28 2007

  3. [3]

    In: de Moura, L

    Blanco, R., Chihani, Z., Miller, D.: Translating between implicit and explicit versions of proof. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothen- burg, Sweden, August 6-11, 2017, Proceedings. LNCS, vol. 10395, pp. 255–273. Springer (2017). DOI: 10.1007/978-3-319-63046-5_16

    work page doi:10.1007/978-3-319-63046-5_16 2017

  4. [4]

    In: Nivelle, H.D

    Chihani, Z., Libal, T., Reis, G.: The proof certifier Checkers. In: Nivelle, H.D. (ed.) Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). pp. 201–210. No. 9323 in LNCS, Springer (2015). DOI:10.1007/978-3-319-24312-2_14

    work page doi:10.1007/978-3-319-24312-2_14 2015

  5. [5]

    Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. of Automated Reasoning 59(3), 287–330 (2017). DOI:10.1007/s10817-016-9380-6

    work page doi:10.1007/s10817-016-9380-6 2017

  6. [6]

    Church, A.: A formulation of the Simple Theory of Types. J. of Symbolic Logic5, 56–68 (1940). DOI: 10.2307/2266170

    work page doi:10.2307/2266170 1940

  7. [7]

    Journal of Symbolic Computation7, 371–425 (1989)

    Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation7, 371–425 (1989). DOI:10.1016/S0747-7171(89)80017-3

    work page doi:10.1016/s0747-7171(89)80017-3 1989

  8. [8]

    Dowek, G.: Third order matching is decidable. Ann. Pure Appl. Log.69(2-3), 135–155 (1994). DOI: 10.1016/0168-0072(94)90083-3

    work page doi:10.1016/0168-0072(94)90083-3 1994

  9. [9]

    In: Lusk, E., Overbeck, R

    Felty, A., Miller, D.: Specifying theorem provers in a higher-order logic programming language. In: Lusk, E., Overbeck, R. (eds.) Ninth International Conference on Automated Deduction. pp. 61–80. No. 310 in LNCS, Springer, Argonne, IL (May 1988). DOI:10.1007/BFb0012823

    work page doi:10.1007/bfb0012823 1988

  10. [10]

    The Journal of Logic Programming37(1), 95–138 (1998)

    Fr¨ uhwirth, T.: Theory and practice of constraint handling rules. The Journal of Logic Programming37(1), 95–138 (1998). DOI:10.1016/S0743-1066(98)10005-5

    work page doi:10.1016/s0743-1066(98)10005-5 1998

  11. [11]

    Untersuchungen über das logische Schließen. I

    Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1935). DOI: 10.1007/BF01201353, translation of articles that appeared in 1934-35. Collected papers appeared in 1969

    work page doi:10.1007/bf01201353 1935

  12. [12]

    Girard, J.Y.: A fixpoint theorem in linear logic (Feb 1992), an email posting to linear@cs.stanford.edu archived athttps://www.seas.upenn.edu/ ~sweirich/types/archive/1992/msg00030.html

    work page 1992

  13. [13]

    Cambridge University Press (1989)

    Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press (1989)

    work page 1989

  14. [14]

    Journal of the ACM40(1), 143–184 (1993)

    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM40(1), 143–184 (1993). DOI:10.1145/138027.138060

    work page doi:10.1145/138027.138060 1993

  15. [15]

    In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence

    Huet, G.P.: A mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence. pp. 139–146. William Kaufmann (1973)

    work page 1973

  16. [16]

    Theoretical Computer Science1, 27–57 (1975)

    Huet, G.P.: A unification algorithm for typed λ-calculus. Theoretical Computer Science1, 27–57 (1975). DOI: 10.1016/0304-3975(75)90011-0

    work page doi:10.1016/0304-3975(75)90011-0 1975

  17. [17]

    In: Proceedings of the 14th ACM Symposium on the Principles of Programming Languages

    Jaffar, J., Lassez, J.L.: Constraint logic programming. In: Proceedings of the 14th ACM Symposium on the Principles of Programming Languages. ACM (1987)

    work page 1987

  18. [18]

    Annals of Mathematics and Artificial Intelligence90(5), 455–479 (2022)

    Libal, T., Miller, D.: Functions-as-constructors higher-order unification: extended pattern unification. Annals of Mathematics and Artificial Intelligence90(5), 455–479 (2022). DOI: 10.1007/s10472-021-09774-y, appears in theSpecial Issue on Theoretical and Practical Aspects of Unification

    work page doi:10.1007/s10472-021-09774-y 2022

  19. [19]

    Theoretical Computer Science232, 91–119 (2000)

    McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science232, 91–119 (2000). DOI:10.1016/S0304-3975(99)00171-1

    work page doi:10.1016/s0304-3975(99)00171-1 2000

  20. [20]

    Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation1(4), 497–536 (1991). DOI:10.1093/logcom/1.4.497

    work page doi:10.1093/logcom/1.4.497 1991

  21. [21]

    Journal of Symbolic Computation14(4), 321–358 (1992)

    Miller, D.: Unification under a mixed prefix. Journal of Symbolic Computation14(4), 321–358 (1992). DOI: 10.1016/0747-7171(92)90011-R

    work page doi:10.1016/0747-7171(92)90011-r 1992

  22. [22]

    Theory and Practice of Logic Programming24(6), 1123–1162 (Nov 2024)

    Miller, D., Momigliano, A.: Property-based testing by elaborating proof outlines. Theory and Practice of Logic Programming24(6), 1123–1162 (Nov 2024). DOI:10.1017/S1471068424000176 12

    work page doi:10.1017/s1471068424000176 2024

  23. [23]

    Cambridge University Press (Jun 2012)

    Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press (Jun 2012). DOI: 10.1017/CBO9781139021326

    work page doi:10.1017/cbo9781139021326 2012

  24. [24]

    Annals of Pure and Applied Logic51(1–2), 125–157 (1991)

    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic51(1–2), 125–157 (1991). DOI:10.1016/0168-0072(91)90068-W

    work page doi:10.1016/0168-0072(91)90068-w 1991

  25. [25]

    ACM Trans

    Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. on Computational Logic6(4), 749–783 (Oct 2005). DOI:10.1145/1094622.1094628

    work page doi:10.1145/1094622.1094628 2005

  26. [26]

    Annals of Mathematics and Artificial Intelligence90(5), 523–535 (2022)

    Miller, D., Viel, A.: Proof search when equality is a logical connective. Annals of Mathematics and Artificial Intelligence90(5), 523–535 (2022). DOI: 10.1007/s10472-021-09764-0,Special Issue on Theoretical and Practical Aspects of Unification

    work page doi:10.1007/s10472-021-09764-0 2022

  27. [27]

    Journal of Automated Reasoning 11(1), 115–145 (Aug 1993)

    Nadathur, G.: A proof procedure for the logic of hereditary Harrop formulas. Journal of Automated Reasoning 11(1), 115–145 (Aug 1993). DOI:10.1007/BF00881902

    work page doi:10.1007/bf00881902 1993

  28. [28]

    In: Huet, G., Plotkin, G

    Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks. pp. 149–181. Cambridge University Press (1991)

    work page 1991

  29. [29]

    In: Robinson, J.A., Voronkov, A

    Pfenning, F.: Logical frameworks. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1063–1147. Elsevier and MIT Press (2001)

    work page 2001

  30. [30]

    In: Ganzinger, H

    Pfenning, F., Sch¨ urmann, C.: System description: Twelf — A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) 16th Conf. on Automated Deduction (CADE). pp. 202–206. No. 1632 in LNAI, Springer, Trento (1999). DOI:10.1007/3-540-48660-7_14

    work page doi:10.1007/3-540-48660-7_14 1999

  31. [31]

    Journal of Functional Programming23(1), 1–37 (2013)

    Pientka, B.: An insider’s look at LF type reconstruction: everything you (n)ever wanted to know. Journal of Functional Programming23(1), 1–37 (2013). DOI:10.1017/S0956796812000408

    work page doi:10.1017/s0956796812000408 2013

  32. [32]

    In: Siekmann, J.H., Wrightson, G

    Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning, pp. 298–313. Symbolic Computation, Springer Berlin Heidelberg (1983). DOI:10.1007/978-3-642-81955-1_19

    work page doi:10.1007/978-3-642-81955-1_19 1983

  33. [33]

    In: Vardi, M

    Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) 8th Symp. on Logic in Computer Science. pp. 222–232. IEEE Computer Society Press, IEEE (Jun 1993). DOI:10.1109/LICS.1993.287585

    work page doi:10.1109/lics.1993.287585 1993

  34. [34]

    append

    Tassi, E.: Elpi: rule-based meta-languge for Rocq. In: Proceedings of CoqPL 2025. ACM (Jan 2025) A Provability from the empty logic program Consider the simple case of the empty logic program and the two classes of (first-order), atom-free formulas defined by the following recursive definition (taken from [26]): Φ ::= Φ1 ∧Φ 2 | ∃ σx.Φ| ∀ σx.Φ|Ψ Ψ ::=t 1 =...

    work page 2025