Pith. sign in

REVIEW 2 major objections 4 minor 41 references

Partial Redundancy in Saturation

T0 review · 2 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Partial redundancy attaches to each clause a formula marking its redundant ground instances, yielding a refutationally complete calculus PaRC that deletes and skips more; in Vampire it solves 24 previously unsolved problems.

desk verdict Genuinely new redundancy criterion with a credible Vampire implementation, but the completeness proof is a sketch with a real gap in the minimal-counterexample induction. read the letter →

arxiv 2505.22213 v1 pith:UXTBKOPZ submitted 2025-05-28 cs.LO

Márton Hajdu , Laura Kovács , Andrei Voronkov This is my paper
classification cs.LO MSC 03B3568T15
keywords partialredundancyformulasclausessuperpositioncalculusrefutationalcompletenesssaturationtheoremprovingVampiredemodulation
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

This paper tries to make saturation-based theorem provers prune more aggressively while preserving the guarantee that the empty clause will still be found. The key move is to attach a redundancy formula to each clause, forming a partial clause, so that every ground instance of the clause satisfying the formula is known to be redundant and need not be kept. The resulting calculus PaRC keeps superposition, equality resolution, and equality factoring, but adds side conditions that skip an inference when the unifying substitution makes the attached formula true, and it permits redundancy formulas to be weakened step by step until a clause becomes wholly redundant. The paper proves soundness and refutational completeness for PaRC and shows that the method generalizes demodulation and related restrictions. An implementation in the Vampire theorem prover solves 24 benchmark problems that no solver, including earlier versions of Vampire, had solved before.

What carries the argument

The load-bearing object is the partial clause $C\setminus R$: an ordinary clause $C$ paired with a redundancy formula $R$, a first-order formula over the ground term algebra extended with relations such as the simplification order $\succ$. Semantically, $R$ records exactly which ground instances of $C$ are known to be redundant, so only instances with $\theta\not\models R$ are active. The mechanism has two moving parts: redundancy steps may replace $R$ by a weaker $R\lor R'$ when $R'$ is admissible, and the PaRC inference rules carry side conditions of the form $\sigma\not\models R$ that suppress steps whose unifier satisfies the formula. This single representation unifies clause-level and inference-level redundancy.

What would settle it

A bounded exhaustive search over finite signatures could look for a fair PaRC saturation whose constructed ground rewrite system $I_\omega$ violates property 5 for some ground terms $s\succ t$; finding such a saturation, or a fair saturation of a small unsatisfiable clause set that never derives $\Box$, would refute Theorem 1 as stated.

Watch

Extended reading notes

Core claim

The central claim is that redundancy can be made ground-instance-wise without sacrificing completeness. In PaRC, a partial clause is $C\setminus R$, where $R$ is a redundancy formula interpreted over the ground term algebra; the calculus only needs to retain those ground instances $C\theta$ for which $\theta\not\models R$. A saturation may weaken $R$ to $R\lor R'$ when every ground instance satisfying $R'$ is redundant, and each inference rule has a side condition $\sigma\not\models R$ that blocks the inference when the unifying substitution makes the attached formula true. Completeness is stated for fair saturations: if the initial clause set is unsatisfiable, the empty partial clause $\Box\setminus\bot$ appears at some stage. The proof works by constructing a convergent ground rewrite system $I_\omega$ and proving by minimal counterexample that every persistent ground clause is true in it. The paper also formulates a generalized demodulation lemma and reports that a Vampire implementation of PaRC solved 24 benchmark problems that no previous prover had solved.

Load-bearing premise

The load-bearing premise is that the five model-construction properties stated in Section 5 are true; the paper asserts them without proof, and property 5, that if $s\succ t$ and $s$ is irreducible w.r.t. $I_\omega$, then $I_\omega\models s\not\approx t$, is used directly in Subcase 3.1 of Lemma 6, so a failure of any of these properties would collapse the completeness proof.

Editorial extensions

If this is right

  • Fewer clauses and inferences need to be kept, so saturation can finish on problems that previously exhausted time or memory.
  • Any fair PaRC saturation of an unsatisfiable clause set still derives the empty clause, so the pruning does not jeopardize refutational completeness.
  • Redundancy formulas can be weakened incrementally, letting a clause accumulate partial redundancy evidence until the evidence is a tautology and the clause is deleted.
  • The generalized demodulation lemma gives a checkable condition under which a demodulation-style replacement can be performed as a redundancy step rather than an inference.
  • The reported 24 newly solved benchmark problems, plus the large number of discarded PaRC inferences in successful runs, shows the technique transfers from theory to proof search.

Reading between the lines

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

  • The same partial-clause mechanism could be applied to theory-specific redundancy relations, such as arithmetic or datatype constraints, because redundancy formulas are arbitrary first-order formulas over the term algebra, not just ordering constraints.
  • If the five model-construction properties are formally verified, the PaRC proof structure should give a uniform way to derive existing redundancy restrictions such as connectedness, blocking, and compositeness as instances of the same framework.
  • A more controlled experiment would isolate the calculus from the schedule search by comparing proof runs with and without PaRC options under identical strategies and measuring how many suppressed inferences are later needed for proof reconstruction.
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

2 major / 4 minor

Summary. The paper introduces partial redundancy for saturation-based theorem proving. A redundancy formula is attached to a clause, marking ground instances that are already redundant; this generalizes standard redundancy and blurs the distinction between clause and inference redundancy. The authors define the PaRC calculus on partial clauses, claim refutational soundness and completeness, give a proof sketch based on a standard model construction, and describe an implementation in Vampire. Experiments on TPTP benchmarks show that the modified Vampire solves 24 problems previously unsolved by any prover, including previous Vampire versions. The claimed theoretical contribution is a more powerful redundancy criterion together with a completeness proof; the practical contribution is the Vampire implementation and the experimental results.

Significance. If the completeness proof is completed, the paper makes a solid contribution to redundancy elimination in superposition calculi: it introduces a genuinely new notion of partial redundancy, shows that it subsumes standard redundancy, and provides a general framework that can express demodulation-like simplifications. The experimental evaluation is a concrete strength: 24 new TPTP solutions, including rating-1.0 problems, and the implementation is publicly available. The paper also connects its framework to constraint-based theorem proving. The main weakness is that the central completeness proof is still a sketch with several unproved model-construction properties and at least one unjustified strict-decrease step in the key induction lemma. The significance would be high once these gaps are filled, but as submitted the main theorem is not fully established.

major comments (2)
  1. [Section 5, model construction, properties 1-5 (pages 8-9)] The properties 1-5 of I_omega are asserted to be 'straightforward' and are not proved. These properties are load-bearing for Lemma 6: property 5 is used in Subcase 3.1 to conclude I_omega models s'!/=t' from irreducibility of s', and properties 2-4 are used in Subcases 3.2 and 4.2 to transfer truth from I_≺l to I_omega. A completeness proof cannot rest on unproved properties of the model construction. Please provide full proofs, or a precise reference to a published source where these exact properties are proved for this construction with redundancy formulas.
  2. [Section 5, Lemma 6, Case 1 (page 9)] The proof asserts 'Note that B is different from D since B is redundant, hence we have B≻D' after applying Lemma 5 to B. This is not a valid inference: a ground clause can be redundant w.r.t. S*_i and still be persistent in the saturation, in which case {B} is a legitimate trace and Lemma 5 may return D = B. To obtain the strict decrease B≻D, the proof should apply Lemma 5 to the clauses C1,...,Cn that witness the redundancy of B, because each such clause is strictly smaller than B and at least one of them must be false in I_omega. As written, the minimal-counterexample induction in Lemma 6 does not go through.
minor comments (4)
  1. [Section 5, opening sentence (page 9)] The first sentence reads 'We starts this section by proving soundness of PaRC.' It should be 'We start'.
  2. [Definition 1, page 5] The phrase 'a first-order formula of TR(Σ)' is awkward; it should be 'a first-order formula in the language of TR(Σ)' or 'over TR(Σ)'.
  3. [Section 5, property 4 (page 9)] Property 4 uses the notation I_s and I_t for arbitrary terms s,t, but I_l has only been defined for the specific term l being processed in the construction. Please clarify whether these are I_≺s and I_≺t, or define the notation.
  4. [Section 7, footnote 5 and Table 3 (pages 16-17)] The footnote 'To be published' is not a usable reference; please provide a citation or remove it. In Table 3, the meaning of the column 'total' should be stated explicitly (for example, number of successful runs).

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: PaRC's completeness argument and experiments are self-contained; the main issue is an incomplete proof, not a circular reduction.

full rationale

PaRC is a self-contained calculus: the redundancy-formula mechanism (Definition 1) and the saturation and fairness definitions (Definitions 3-5) are stated as proof-theoretic conditions, and the completeness theorem is approached by the standard minimal-counterexample/model-construction method rather than by assuming the theorem. Lemma 7's demodulation admissibility proof is a direct derivation: it exhibits the existing rewrite rule and rewritten clause as smaller ground instances that entail the target instance, so it does not smuggle the conclusion into the premise. The experiments are external: schedules are tuned on a training split and evaluated on a disjoint test split of TPTP, and no theoretical result is inferred from the benchmark data. The only self-citations (Vampire system [24], code trees [35]) are implementation credits and are not premises of Theorem 1. The genuine weakness is a proof gap, not circularity: Section 4 states 'We will not give a full proof of Theorem 1', Section 5 lists model-construction properties 1-5 as 'straightforward' without proof, and Lemma 6 Case 1 compresses the strict-decrease argument ('Note that B is different from D since B is redundant, hence we have B≻ D'). These omissions could affect correctness but do not make the derivation reduce to its own inputs.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

The central claim rests on standard superposition theory assumptions plus the new partial-clause formalism. The main free parameters are absent; the practical implementation has Boolean option switches but no fitted numeric constants. The most significant unstated premise is the correctness of the unproved model-construction properties.

assumptions (4)
  • domain assumption The signature has at least one constant, and the term algebra TR(Σ) with fixed redundancy relations, including a simplification order, is available.
    Assumed in Section 3 before Definition 1 to ensure Herbrand-style interpretations and ground instances exist.
  • standard math The simplification order is a well-founded reduction ordering that is total on ground terms, and bag extensions preserve well-foundedness and totality.
    Used throughout Section 5 for the model construction and in the redundancy ordering; standard in the superposition literature.
  • domain assumption The unproved model-construction properties 1-5 of Iω are correct, especially property 5 about irreducible terms and disequalities.
    Asserted as 'straightforward' in Section 5 and used in Lemma 6, Subcase 3.1, for the completeness proof. This is load-bearing and not proved.
  • standard math Ground clauses that are redundant w.r.t. S*_i remain redundant w.r.t. all later S*_j and S⊛_j, as stated in Lemma 2.
    Used to justify the trace lemma and the persistence arguments; relies on well-foundedness of the ordering.
invented entities (2)
  • Partial clause C\R independent evidence
    purpose: A clause C with an attached redundancy formula R, meaning all ground instances of C satisfying R are known to be redundant in the search space.
    Formally defined in Definition 1, used throughout the calculus, and implemented in Vampire with observable effects on solving performance.
  • Redundancy formula R independent evidence
    purpose: A first-order formula over TR(Σ) that characterizes a subset of ground instances of a clause as redundant.
    Defined in Definition 1 and used in the side conditions of Sup, EqRes, and EqFac, as well as in redundancy steps. The implementation checks such formulas.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Partial Redundancy in Saturation." pith.science (2026). https://pith.science/paper/UXTBKOPZ

@misc{pith2026250522213,
  author       = {Pith},
  title        = {Pith review of: Partial Redundancy in Saturation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UXTBKOPZ}},
  note         = {Machine review of arXiv:2505.22213}
}
read the original abstract

Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We improve redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas, which is more powerful than the standard notion: there are both clauses and inferences that are redundant when we use our notions and not redundant when we use standard notions. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses. Our calculus is refutationally complete and is strong enough to capture some standard restrictions of the superposition calculus. We discuss the implementation of the calculus in the theorem prover Vampire. Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire.

Figures

Figures reproduced from arXiv: 2505.22213 by the authors.

Figure 1
Figure 1. The PaRC calculus. variables occur in C. If σ is a substitution and R a redundancy formula, we write σ  R if every ground instance of Rσ is true in TR(Σ). We write σ 2 R if σ  R does not hold. ❏ An example of a redundancy formula is f(x) ≻ y ∨ y = x. Note that we can use equality = in redundancy formulas as in this example. In the sequel, we denote redundancy formulas by R, and partial clauses by C and D, possibly… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

41 extracted references · 23 canonical work pages

  1. [1]

    Journal of Symbolic Co mputation (2003)

    Avenhaus, J., Hillenbrand, T., L¨ ochner, B.: On Using Gro und Joinable Equa- tions in Equational Theorem Proving. Journal of Symbolic Co mputation (2003). https://doi.org/10.1016/S0747-7171(03)00024-5

    work page doi:10.1016/s0747-7171(03)00024-5 2003

  2. [2]

    In: Term Rew rit- ing and All That, chap

    Baader, F., Nipkow, T.: Equational problems. In: Term Rew rit- ing and All That, chap. 4. Cambridge University Press (1998) . https://doi.org/10.1017/CBO9781139172752

    doi:10.1017/cbo9781139172752 1998

  3. [3]

    Progress in t heoretical computer sci- ence, Birkh¨ auser (1991)

    Bachmair, L.: Canonical Equational Proofs. Progress in t heoretical computer sci- ence, Birkh¨ auser (1991). https://doi.org/10.1007/978-1-4684-7118-2

    work page doi:10.1007/978-1-4684-7118-2 1991

  4. [4]

    Journal of Symbolic Computation (1988)

    Bachmair, L., Dershowitz, N.: Critical Pair Criteria for Completion. Journal of Symbolic Computation (1988). https://doi.org/10.1016/S 0747-7171(88)80018-X

    doi:10.1016/s 1988

  5. [5]

    In: CADE (1990)

    Bachmair, L., Ganzinger, H.: On restrictions of ordered p aramodulation with sim- plification. In: CADE (1990). https://doi.org/10.1007/3- 540-52885-7 105

    doi:10.1007/3- 1990

  6. [6]

    In: Automated Deduction: A Basis for Applications , vol

    Bachmair, L., Ganzinger, H.: Equational Reasoning in Sat uration-Based Theorem Proving. In: Automated Deduction: A Basis for Applications , vol. I, chap. 11. Springer (1998). https://doi.org/10.1007/978-94-017-0 437-3

    work page doi:10.1007/978-94-017-0 1998

  7. [7]

    In: Handbook of Automated Reasoning, pp

    Bachmair, L., Ganzinger, H.: Resolution Theorem Proving . In: Handbook of Automated Reasoning, pp. 19–99. Elsevier and MIT Press (2 001). https://doi.org/10.1016/B978-044450813-3/50004-7

    doi:10.1016/b978-044450813-3/50004-7

  8. [8]

    Infor- mation and Computation (1995)

    Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation. Infor- mation and Computation (1995). https://doi.org/10.1006/ inco.1995.1131

    work page arXiv 1995

Show all 41 references
  1. [10]

    In: CADE (2021)

    Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi´ c , P.: Su- perposition for Full Higher-order Logic. In: CADE (2021). https://doi.org/10.1007/978-3-030-79876-5 23

    2021 doi

  2. [11]

    In: CADE (2023)

    Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition with Delayed Unification. In: CADE (2023). https://doi.org/10.1007/978-3-031-384 99-8 2

    2023 doi

  3. [12]

    Inte rnational Journal of Foun- dations of Computer Science (1990)

    Comon, H.: Solving Symbolic Ordering Constraints. Inte rnational Journal of Foun- dations of Computer Science (1990). https://doi.org/10.1 142/S0129054190000278 20 M´ arton Hajdu, Laura Kov´ acs and Andrei Voronkov

    1990

  4. [13]

    ACM TOCL (200 3)

    Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch , M.: Deciding the confluence of ordered term rewrite systems. ACM TOCL (200 3). https://doi.org/10.1145/601775.601777

  5. [14]

    In: Annual IEEE Sy mposium on Logic in Computer Science (1995)

    Comon, H., Nieuwenhuis, R., Rubio, A.: Orderings, AC-Th eories and Symbolic Constraint Solving (Extended Abstract). In: Annual IEEE Sy mposium on Logic in Computer Science (1995). https://doi.org/10.1109/LIC S.1995.523272

    1995

  6. [15]

    Com- munications of the ACM (1979)

    Dershowitz, N., Manna, Z.: Proving Termination with Mul tiset Orderings. Com- munications of the ACM (1979). https://doi.org/10.1145/3 59138.359142

    1979

  7. [16]

    I n: ITP (2024)

    Desharnais, M., Toth, B., Waldmann, U., Blanchette, J., Tourret, S.: A Modular Formalization of Superposition in Isabelle/HOL. I n: ITP (2024). https://doi.org/10.4230/LIPIcs.ITP.2024.12

    2024 doi

  8. [17]

    In: IJCAR (2022)

    Duarte, A., Korovin, K.: Ground Joinability and Connect edness in the Superposi- tion Calculus. In: IJCAR (2022). https://doi.org/10.1007 /978-3-031-10769-6 11

    2022

  9. [18]

    Ganzinger, H., Nieuwenhuis, R.: Constraints and Theore m Proving, p. 159–201. Springer Berlin Heidelberg (2001). https://doi.org/10.1 007/3-540-45406-3 4

    2001

  10. [19]

    Journal of Symbolic Compu- tation (1988)

    Kapur, D., Musser, D.R., Narendran, P.: Only Prime Super positions Need be Con- sidered in the Knuth-Bendix Completion Procedure. Journal of Symbolic Compu- tation (1988). https://doi.org/10.1016/S0747-7171(88) 80019-1

    1988 doi

  11. [20]

    Research report, INRIA (1990), https://www.researchgate.net/publication/245850515

    Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with Symbolic Constraints. Research report, INRIA (1990), https://www.researchgate.net/publication/245850515

    1990

  12. [21]

    In: Au- tomation of Reasoning: 2: Classical Papers on Computationa l Logic 1967–1970

    Knuth, D.E., Bendix, P.B.: Simple Word Problems in Unive rsal Algebras. In: Au- tomation of Reasoning: 2: Classical Papers on Computationa l Logic 1967–1970. Springer (1983). https://doi.org/10.1007/978-3-642-81 955-1 23

    1983 doi

  13. [22]

    In: IJCAR (200 8)

    Korovin, K.: iProver — An Instantiation-Based Theorem P rover for First-Order Logic (System Description). In: IJCAR (200 8). https://doi.org/10.1007/978-3-540-71070-7 24

    doi

  14. [23]

    In: ICALP (2001)

    Korovin, K., Voronkov, A.: Knuth-Bendix Constraint Sol ving Is NP-Complete. In: ICALP (2001). https://doi.org/10.1007/3-540-48224-5 79

    2001 doi

  15. [24]

    In: CA V (2013)

    Kov´ acs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CA V (2013). https://doi.org/10.1007/978-3-642-39799-8 1

    2013 doi

  16. [25]

    In: IJCAR (2004)

    L¨ ochner, B.: A Redundancy Criterion Based on Ground Red ucibility by Ordered Rewriting. In: IJCAR (2004). https://doi.org/10.1007/97 8-3-540-25984-8 2

    2004 doi

  17. [26]

    In: RTA (1993)

    Lynch, C., Snyder, W.: Redundancy Criteria for Constrai ned Completion. In: RTA (1993). https://doi.org/10.1007/978-3-662-21551-7 2

    1993 doi

  18. [27]

    Jour nal of Automated Reasoning (2006)

    L¨ ochner, B.: Things to Know when Implementing KBO. Jour nal of Automated Reasoning (2006). https://doi.org/10.1007/s10817-006- 9031-4

    2006 doi

  19. [28]

    In: Hand- book of Automated Reasoning, chap

    Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theo rem Proving. In: Hand- book of Automated Reasoning, chap. 7. Elsevier and MIT Press (2001). https://doi.org/10.1016/B978-044450813-3/50009-6

    2001 doi

  20. [29]

    Information Processing Letters (1993)

    Nieuwenhuis, R.: Simple LPO constraint solving methods . Information Processing Letters (1993). https://doi.org/10.1016/0020-0190(93) 90226-Y

    1993 doi

  21. [30]

    In: ESOP (1992)

    Nieuwenhuis, R., Rubio, A.: Basic Superposition is Comp lete. In: ESOP (1992). https://doi.org/10.1007/3-540-55253-7 22

    1992 doi

  22. [31]

    Journal of Symbolic Computation ( 1995)

    Nieuwenhuis, R., Rubio, A.: Theorem Proving with Orderi ng and Equal- ity Constrained Clauses. Journal of Symbolic Computation ( 1995). https://doi.org/10.1006/jsco.1995.1020

    1995

  23. [32]

    Journal of Symbolic Computati on (1991)

    Pais, J., Peterson, G.E.: Using forcing to prove complet eness of res- olution and paramodulation. Journal of Symbolic Computati on (1991). https://doi.org/10.1016/S0747-7171(08)80130-7 Partial Redundancy in Saturation 21

    1991 doi

  24. [33]

    Ar chive of Formal Proofs (September 2016), https://isa-afp.org/entries/SuperCalc.html

    Peltier, N.: A variant of the superposition calculus. Ar chive of Formal Proofs (September 2016), https://isa-afp.org/entries/SuperCalc.html

    2016

  25. [34]

    In: T ACAS (2018)

    Reger, G., Suda, M., Voronkov, A.: Unification with Abstr action and Theory Instantiation in Saturation-Based Reasoning. In: T ACAS (2018). https://doi.org/10.1007/978-3-319-89960-2 1

    2018 doi

  26. [35]

    In: Logics in Artificial Intelligence (2000)

    Riazanov, A., Voronkov, A.: Partially adaptive code tre es. In: Logics in Artificial Intelligence (2000). https://doi.org/10.1007/3-540-40 006-0 15

    2000 doi

  27. [36]

    In: CADE (2004)

    Riazanov, A., Voronkov, A.: Efficient Checking of Term Ord ering Constraints. In: CADE (2004). https://doi.org/10.1007/978-3-540-25984- 8 3

    2004 doi

  28. [37]

    Robinson, G., Wos, L.: Paramodulation and Theorem-Prov ing in First-Order The- ories with Equality, p. 298–313. Springer Berlin Heidelber g, Berlin, Heidelberg (1983). https://doi.org/10.1007/978-3-642-81955-1 19

    1983 doi

  29. [38]

    In: CADE (2019)

    Schulz, S., Cruanes, S., Vukmirovi´ c, P.: Faster, Highe r, Stronger: E 2.3. In: CADE (2019). https://doi.org/10.1007/978-3-030-29436-6 29

    2019 doi

  30. [39]

    In: IJCA R (2024)

    Sutcliffe, G.: Stepping Stones in the TPTP World. In: IJCA R (2024). https://doi.org/10.1007/978-3-031-63498-7 3

    2024 doi

  31. [40]

    Journal of Automated R easoning (2022)

    Waldmann, U., Tourret, S., Robillard, S., Blanchette, J .: A Comprehensive Frame- work for Saturation Theorem Proving. Journal of Automated R easoning (2022). https://doi.org/10.1007/S10817-022-09621-7

    2022 doi

  32. [41]

    In: RTA (1989)

    Zhang, H., Kapur, D.: Consider only General Superpositi ons in Completion Pro- cedures. In: RTA (1989). https://doi.org/10.1007/3-540- 51081-8 129

    1989 doi

  33. [42]

    In: Mathematical Systems Theory (1 990)

    Zhang, H., Kapur, D.: Unnecessary Inferences in Associa tive-Commutative Completion Procedures. In: Mathematical Systems Theory (1 990). https://doi.org/10.1007/BF02090774

    doi

Pith tools

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