Pith. sign in

REVIEW 2 major objections 4 minor 48 references

Computing Witnesses Using the SCAN Algorithm (Extended Preprint)

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 SCAN can be extended to compute explicit first-order witnesses for eliminated second-order quantifiers.

desk verdict WSCAN is a genuinely new idea with a clear write-up, but the main theorem's proof has a load-bearing gap in Lemma 25, so the paper needs fixing before it can be trusted. read the letter →

arxiv 2506.00163 v1 pith:N3ZATNY5 submitted 2025-05-30 cs.LO

Fabian Achammer , Stefan Hetzl , Renate A. Schmidt This is my paper
classification cs.LO MSC 03B1503B3568T15
keywords second-orderquantifiereliminationSCANalgorithmformulaequationssaturationtheoremprovingwitnessconstructionfirst-orderone-sidedderivationspredicate
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

Second-order quantifier elimination asks for a first-order formula equivalent to a quantified formula such as $\exists X \varphi$. This paper tackles a stronger problem: finding an actual first-order predicate expression $\alpha$ that can be substituted for $X$ so that $\exists X \varphi \equiv \varphi[X \leftarrow \alpha]$. The authors show that every terminating run of the SCAN algorithm records enough information, if remembered as a derivation, to reconstruct such a witness by walking backwards through the derivation. This matters because witnessed second-order quantifier elimination sits between ordinary elimination and solving formula equations, and a witness can be used for forgetting, interpolation, and verification without rebuilding the formula from scratch.

What carries the argument

The load-bearing object is the predicate expression $p\mathrm{Res}^U_P$, defined for a pointed clause $P$ as follows: take the unit clause dual to $P$'s designated literal, close it under repeated constraint resolution with $P$, and convert the resulting (possibly infinite) clause set into a $\lambda$-predicate by conjoining or disjoining the clauses. The witness preservation lemma shows that replacing a witness for the clause set after a derivation step with $p\mathrm{Res}^U_P[X \leftarrow \alpha]$ yields a witness for the clause set before the step, which is what lets the algorithm walk backwards through the recorded SCAN run.

What would settle it

Find a clause set $N$, a pointed clause $P$, and a redundancy criterion satisfying the paper's two conditions (entailment-compatible and equivalence-preserving) such that every one-step resolvent of $P$ with $N$ is redundant in $N$ but some iterated resolvent in $\mathrm{Res}_P(N)$ is not entailed by $N$; such a counterexample would break the transformation lemma and with it the main theorem.

Watch

Extended reading notes

Core claim

The paper defines WSCAN, an extension of the SCAN algorithm on clause sets. Given an $X$-eliminating derivation $D$ from a clause set $N$, i.e., a recorded saturation run whose final clause set contains no predicate variables from $X$, the construction $\mathrm{wit}(D)$ yields a tuple of predicate expressions satisfying $\exists X N \equiv N[X \leftarrow \mathrm{wit}(D)]$. The construction is bottom-up: it starts from a trivial witness at the final clause set and, for each derivation step $S$ read backwards, applies a transformation $T_S$ to the current witness; for a purified clause deletion step, the component for the deleted predicate variable becomes $p\mathrm{Res}^U_P[X \leftarrow \alpha]$, built from the resolution closure of the deleted pointed clause $P$ against the unit clause dual to its designated literal. If every purified clause in $D$ is one-sided, meaning the eliminated predicate occurs with only one polarity, then $\mathrm{wit}(D)$ is a first-order predicate. The same machinery supplies a new correctness proof for SCAN itself.

Load-bearing premise

The proof assumes that once a clause's direct resolvents are redundant, all clauses obtainable by repeatedly resolving with it are also redundant, though the stated deletion rule only guarantees the direct ones are.

Editorial extensions

If this is right

  • If SCAN terminates on a clause set and the recorded derivation is one-sided, the algorithm outputs a first-order witness formula, not merely an equivalent clause set.
  • Feeding a computed witness to a first-order theorem prover decides the corresponding formula equation, because validity of $\varphi[X \leftarrow \alpha]$ is then a first-order question.
  • On clause sets, the method generalises Ackermann's Lemma: whenever the lemma applies, there is a one-sided derivation whose witness is equivalent to the lemma's witness, and the method also covers cases where the lemma does not apply.
  • For one-sided derivations, witness size is at most exponential in the number of purified clauses, and linear when each purified clause contains exactly one $X$-literal; matching lower bounds show the bounds are tight.
  • The transformation lemma underlying the witness construction doubles as a new proof of SCAN's correctness, independent of the original argument.

Reading between the lines

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

  • Editorial: The infinite witnesses that arise when a purified clause is not one-sided suggest a fixpoint extension: infinite $p\mathrm{Res}^U_P$ expressions often encode least or greatest fixpoints, and adding a fixpoint constructor to the witness language could make WSCAN succeed in cases where first-order witnesses provably do not exist.
  • Editorial: Since different choices of pointed clauses in the saturation loop give different, incomparable witnesses, the procedure could be used to generate candidate loop invariants in Horn-clause verification by running the saturation with varied strategies.
  • Editorial: The Skolem-constant example indicates a testable extension: integrating reverse Skolemization would let WSCAN detect when a witness exists only in an expanded signature and report the minimal signature extension required.
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 the problem of witnessed second-order quantifier elimination (WSOQE): given a formula ∃X φ with first-order φ, find a tuple α of predicate expressions such that ∃X φ ≡ φ[X←α]. The authors extend the SCAN algorithm to a new algorithm WSCAN, which uses a recorded SCAN derivation to construct such a witness in a bottom-up manner. The main result, Theorem 15, asserts that every X-eliminating C-derivation from N yields a witness wit(D) for ∃X N. The paper also gives sufficient conditions, one-sidedness, for the witness to be first-order (Corollary 20), discusses connections to formula equations and Ackermann's Lemma, and reports a prototype implementation in GAPT 2.18.1.

Significance. If Theorem 15 were correct, the paper would make a useful conceptual contribution: it connects second-order quantifier elimination with the older problem of solving formula equations, and the idea of extracting witnesses from a recorded saturation derivation is attractive. The appended proofs are detailed and the paper is generally well written. However, the central correctness claim is false as stated: I give a concrete, small counterexample in which the PurDel step is applicable, the derivation is X-eliminating, and the witness computed by Definition 14 is not a WSOQE-witness. Since the main theorem is unsound, the algorithm, its corollaries, and the implementation claims are not supported. The failure is load-bearing and cannot be repaired by local proof patching: the PurDel transformation itself is invalid.

major comments (2)
  1. [Appendix B, Lemma 25 and Lemma 6; Section 4, Theorem 15] Theorem 15 is false. Consider the clause set N0 = {X(a)∨A, ¬X(a)∨¬X(b)∨B, ¬X(b)∨B}, with P = X(a)∨A as the pointed clause. The PurDel_P step from N0 to N′ = {¬X(a)∨¬X(b)∨B, ¬X(b)∨B} is valid under Definition 2: the only resolvent of P with a clause of N′ is A∨¬X(b)∨B (after constraint elimination), which is subsumed by the clause ¬X(b)∨B and hence redundant in N′. All X-literals in N′ are negative, so ExtPurDel−_X is applicable, giving an X-eliminating C-derivation D from N0 to ∅. Following Definition 14, wit(D) is λu.¬A: the ExtPurDel−_X step sets the witness to λu.⊥, and the PurDel_P step transforms it to pResU_P[X←λu.⊥] = λu.¬A. However, ∃X N0 is logically equivalent to A∨B∨(a̸≃b): if a≠b, choose X(a)=true and X(b)=false; if A holds, choose X(a)=true; if B holds, choose X(a)=true for any X(b). Substituting λu.¬A for X turns N0 into (¬A∨A) ∧ (¬¬A∨¬¬A∨B) ∧ (¬¬A∨B), which simplifies to A∨B. This is not equivalent to A∨B∨(a̸≃b); in a model with a≠b, A=false, B=false, the former is false and the latter is true. Thus wit(D) is not a witness for ∃X N0, contradicting Theorem 15.
  2. [Appendix B, Lemma 25 proof; Definition 2 vs. Definition 7] The proof of Lemma 25 contains the unjustified assertion: 'Since P is purified in N′ we have that ResP(N′) is redundant in N′'. Definition 2 only requires every one-step resolvent of P with a clause from N′ to be redundant in N′. It does not require, and in general does not imply, that the full resolution closure ResP(N′) is redundant. In the counterexample above, the closure contains the clause a̸≃b∨B∨A, obtained by resolving P with the one-step resolvent A∨¬X(b)∨B. That clause is not entailed by N′: taking a≠b, A=false, B=false, X(b)=false satisfies both clauses of N′ but falsifies a̸≃b∨B∨A. Hence the closure redundancy used in the proof fails. Since Lemma 25 is the central device by which Lemma 6 and Theorem 15 are derived, the main proof is unsound.
minor comments (4)
  1. [Section 4, text after Lemma 6] In the paragraph explaining ExtPurDel^+_X and ExtPurDel^−_X, the sentence 'setting the X-component of TS(α) to X to λu.⊥' contains a typo; it should read 'to λu.⊥'.
  2. [Appendix B, Lemma 27 and surrounding text] The notation is inconsistent: ResU_P(C) and ResUP(C) are used interchangeably, and some occurrences of 'ResUP' should be 'Res_P'. This makes the otherwise detailed proofs harder to follow.
  3. [Section 7, 'Limitations for finding witnesses'] The example showing that no WSOQE-witness exists in the input language for Φ = ∃X∃u∃v(X(u)∧¬X(v)) is correct and instructive; however, its conclusion is presented as a limitation of the method rather than as a consequence of the semantics, which is worth clarifying.
  4. [Section 5, proof of Proposition 32] The recurrence for the lower bound uses the notation w_i for |wit_i(D_{p,n})|, but the indexing is off by one relative to the definition of w_i in the preceding paragraph; the intended asymptotic bounds are clear, but the indices should be fixed.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: witnesses are computed from recorded SCAN derivations and the pResUP construction is justified by proof, not by definitional equivalence.

full rationale

The central claim, Theorem 15, is not circular. wit(D) is defined from the recorded C-derivation by the explicit transformations in Definitions 13 and 14, and the WSOQE condition is proved, not assumed. The key object pResUP is an explicit predicate expression built from the resolution closure ResUP(c); Lemma 11, which shows that X←pResUP satisfies P and respects ResP(C), is proved from resolution-closure properties (Lemma 27) and duality (Lemma 28), not from the target equivalence. No parameter is fitted to data, and no output is a renamed input. Self-citations such as [17], [23], [26], and [27] are background, classical, or implementation references and are not load-bearing for the main result; Ackermann's Lemma is ultimately an external classical result [1]. The paper's honest limitations (Problem 21 on one-sided completeness, possible non-termination of first-order annotations, small benchmark set) are caveats, not circularity. The one substantive flaw is in Appendix B, proof of Lemma 25: 'Since P is purified in N' we have that ResP(N') is redundant in N'' is stronger than Definition 2's PurDel side condition, which only requires one-step resolvents of P with clauses of N' to be redundant. This is a genuine proof gap and correctness risk, but it is not circularity: the claimed witness property does not reduce to the assumptions by construction, and the gap could be repaired by adding a standard redundancy closure condition or by giving a different argument. Overall, no significant circularity is present.

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

The central theorem rests on standard logic plus the purification calculus; no free parameters are fitted to data. The only load-bearing unproved premise is closure redundancy of purified clauses, and the first-order witness guarantee requires one-sidedness, whose completeness is left open as Problem 21.

assumptions (4)
  • standard math Classical first-order and second-order logic with equality, Tarskian semantics, and standard clause logic.
    Section 2 presupposes these foundations; they are background assumptions, not derived.
  • domain assumption The input is given as a clause set, and the method does not handle Skolemization or reverse Skolemization.
    Section 7 states this restriction; the central theorem only applies to clause sets after clausification and with universal domain variables.
  • domain assumption Redundancy criteria satisfy compatibility with entailment and equivalence preservation.
    Section 3 states this as the only requirement on redundancy; the proof may need stronger closure properties under resolution.
  • ad hoc to paper For a purified clause P, the resolution closure ResP(N') is redundant in N'.
    Used in the proof of Lemma 25 without being derived from the PurDel side condition in Definition 2. It may hold for standard redundancy criteria, but it is not stated as an assumption or proved.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Computing Witnesses Using the SCAN Algorithm (Extended Preprint)." pith.science (2026). https://pith.science/paper/N3ZATNY5

@misc{pith2026250600163,
  author       = {Pith},
  title        = {Pith review of: Computing Witnesses Using the SCAN Algorithm (Extended Preprint)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N3ZATNY5}},
  note         = {Machine review of arXiv:2506.00163}
}
read the original abstract

Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

48 extracted references · 33 canonical work pages

  1. [1]

    Mathematische Annalen110(1), 390–413 (1935)

    Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen110(1), 390–413 (1935). https://doi.org/10.1007/BF01448035

    work page doi:10.1007/bf01448035 1935

  2. [2]

    In: Fernández-Duque, D., Palmigiano, A., Pinchinat, S

    Alassaf, R., Schmidt, R.A., Sattler, U.: Saturation-based uniform interpolation for multi-modal logics. In: Fernández-Duque, D., Palmigiano, A., Pinchinat, S. (eds.) Advances in Modal Logic, Volume 14. pp. 37–58. College Publications, London (2022), http://www.aiml.net/volumes/volume14

    work page 2022

  3. [3]

    Applicable Algebra in Engineering, Communication and Computing5, 193–212 (1994)

    Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing5, 193–212 (1994). https://doi.org/10.1007/BF01190829

    doi:10.1007/bf01190829 1994

  4. [4]

    In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A., Wolter, F

    Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. Lecture Notes in Computer Science, vol. 11560, pp. 15–56. Springer (2019). https://doi.org/10.1007/978-3-030-22102-7_2

    work page doi:10.1007/978-3-030-22102-7_2 2019

  5. [5]

    Archiv für mathematische Logik und Grundlagenforschung1(1), 17–29 (1950)

    Behmann, H.: Das Auflösungsproblem in der Klassenlogik. Archiv für mathematische Logik und Grundlagenforschung1(1), 17–29 (1950). https://doi.org/10.1007/BF01976313, first of two parts

    work page doi:10.1007/bf01976313 1950

  6. [6]

    Archiv für mathematische Logik und Grundlagenforschung1(2), 33–51 (1951)

    Behmann, H.: Das Auflösungsproblem in der Klassenlogik. Archiv für mathematische Logik und Grundlagenforschung1(2), 33–51 (1951). https://doi.org/10.1007/BF01982011, second of two parts

    work page doi:10.1007/bf01982011 1951

  7. [7]

    In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W

    Bjørner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol. 9300, pp. 24–51....

    doi:10.1007/978-3-319-23534-9_2 2015

  8. [8]

    Computers and Mathematics with Applications29(2), 73–90 (1995)

    Brink, C., Gabbay, D.M., Ohlbach, H.J.: Towards automating duality. Computers and Mathematics with Applications29(2), 73–90 (1995)

    work page 1995

Show all 48 references
  1. [9]

    In: Kejriwal, M., Szekely, P.A., Troncy, R

    Chen, J., Alghamdi, G., Schmidt, R.A., Walther, D., Gao, Y.: Ontology extraction for large ontologies via modularity and forgetting. In: Kejriwal, M., Szekely, P.A., Troncy, R. (eds.) Proceedings of the 10th International Conference on Knowledge Capture (K-CAP’19). pp. 45–52. ...

    2019

  2. [10]

    The core algorithm sqema

    Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and com- pleteness in modal logic: I. The core algorithm sqema. Logical Methods in Com- puter Science2(1:5), 1–26 (2006)

    2006

  3. [11]

    In: Baltag, A., Smets, S

    Conradie, W., Ghilardi, S., Palmigiano, A.: Unified correspondence. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, pp. 933–975. Springer (2014). https://doi.org/10.1007/978-3-319-06025-5_36

    2014 doi

  4. [12]

    Delgrande, J.P.: A knowledge level account of forgetting. J. Artif. Intell. Res.60, 1165–1213 (2017). https://doi.org/10.1613/JAIR.5530

    2017 doi

  5. [13]

    Journal of Automated Reasoning18(3), 297–336 (1997)

    Doherty, P., Lukaszewicz, W., Szalas, A.: Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning18(3), 297–336 (1997). https://doi.org/10.1023/A:1005722130532

    1997 doi

  6. [14]

    Fundamenta Informaticae36(1), 23–55 (1998)

    Doherty, P., Łukaszewicz, W., Szałas, A.: General domain circumscription and its effective reductions. Fundamenta Informaticae36(1), 23–55 (1998). https://doi.org/10.3233/FI-1998-3612 Computing Witnesses Using the SCAN Algorithm (Extended Preprint) 19

    1998 doi

  7. [15]

    In: Nebel, B

    Doherty,P.,Lukaszewicz,W.,Szalas,A.:Computingstrongestnecessaryandweak- est sufficient conditions of first-order formulas. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001). pp. 145–154. Morgan Kaufmann (2001)

    2001

  8. [16]

    In: Tsumoto, S., Slowinski, R., Komorowski, H.J., Grzymala-Busse, J.W

    Doherty, P., Szalas, A.: On the correspondence between approximations and similarity. In: Tsumoto, S., Slowinski, R., Komorowski, H.J., Grzymala-Busse, J.W. (eds.) Rough Sets and Current Trends in Computing (RSCTC 2004). Lecture Notes in Computer Science, vol. 3066, pp. 143–15...

    2004 doi

  9. [17]

    Journal of Logic and Computation27(1), 109–128 (2017)

    Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with pred- icates. Journal of Logic and Computation27(1), 109–128 (2017). https://doi.org/10.1093/logcom/exv059

    2017 doi

  10. [18]

    In: Olivetti, N., Tiwari, A

    Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System de- scription: Gapt 2.0. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning. pp. 293–301. Springer International Publishing, Cham (2016)

    2016

  11. [19]

    Künstliche Intell.33(1), 9–33 (2019)

    Eiter, T., Kern-Isberner, G.: A brief survey on forgetting from a knowledge representation and reasoning perspective. Künstliche Intell.33(1), 9–33 (2019). https://doi.org/10.1007/S13218-018-0564-6

    2019 doi

  12. [20]

    Diplomarbeit, Fachbereich Informatik, Univ

    Engel, T.: Quantifier Elimination in Second-Order Predicate Logic. Diplomarbeit, Fachbereich Informatik, Univ. des Saarlandes, Saarbrücken, Germany (October 1996)

    1996

  13. [21]

    In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A

    Férée, H., van der Giessen, I., van Gool, S., Shillito, I.: Mechanised uniform inter- polation for modal logics k, gl, and isl. In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning (IJCAR 2024). Lecture Notes in Computer Sci- ence, vol. 14740, pp. 43–60....

    2024 doi

  14. [22]

    South African Computer Journal7, 35–43 (1992)

    Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second order predicate logic. South African Computer Journal7, 35–43 (1992)

    1992

  15. [23]

    College Publications (2008)

    Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination. College Publications (2008)

    2008

  16. [24]

    Theory Pract

    Gonçalves, R., Knorr, M., Leite, J.: Forgetting in answer set program- ming: A survey. Theory Pract. Log. Program.23(1), 111–156 (2023). https://doi.org/10.1017/S1471068421000570

    2023 doi

  17. [25]

    In: Berghammer, R., Möller, B., Struth, G

    Goranko, V., Hustadt, U., Schmidt, R.A., Vakarelov, D.: SCAN is complete for all sahlqvist formulae. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science, vol. 3051, pp. 149...

    2003 doi

  18. [26]

    In: Hojjat, H., Kafle, B

    Hetzl, S., Kloibhofer, J.: A Fixed-point Theorem for Horn Formula Equa- tions. In: Hojjat, H., Kafle, B. (eds.) 8th Workshop on Horn Clauses for Ver- ification and Synthesis (HCVS). Electronic Proceedings in Theoretical Com- puter Science, vol. 344, pp. 65–78. Open Publishing ...

    2021 doi

  19. [27]

    In: Schmidt, R.A., Wernhard, C., Zhao, Y

    Hetzl, S., Kloibhofer, J.: An Abstract Fixed-Point Theorem for Horn Formula Equations (Abstract). In: Schmidt, R.A., Wernhard, C., Zhao, Y. (eds.) Proceed- ings of the Second Workshop on Second-Order Quantifier Elimination and Re- lated Topics (SOQE). CEUR Workshop Proceedings...

    2021

  20. [28]

    In: Giesl, J., Hähnle, R

    Hoder, K., Kovács, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: Giesl, J., Hähnle, R. (eds.) Automated Reasoning (IJCAR 2010). 20 F. Achammer, S. Hetzl, R. A. Schmidt Lecture Notes in Computer Science, vol. 6173, pp. 188–195. Springer (2010). https://...

    2010 doi

  21. [29]

    Cambridge University Press (1997)

    Hodges, W.: A Shorter Model Theory. Cambridge University Press (1997)

    1997

  22. [30]

    In: Creignou, N., Berre, D.L

    Khasidashvili,Z.,Korovin,K.:Predicateeliminationforpreprocessinginfirst-order theorem proving. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing (SAT 2016). Lecture Notes in Computer Science, vol. 9710, pp. 361–372. Springer (2016). https:/...

    2016 doi

  23. [31]

    In: Boutilier, C

    Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large- scale description logic terminologies. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009). pp. 830–835 (2009), http://ijcai.or...

    2009

  24. [32]

    In: McMillan, K., Middeldorp, A., Voronkov, A

    Koopmann, P., Schmidt, R.A.: Forgetting concept and role symbols inALCH- ontologies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013). Lec- ture Notes in Computer Science, vol. 8312, pp. 552–567. Sp...

    2013 doi

  25. [33]

    In: Fontaine, P., Ringeissen, C., Schmidt, R.A

    Koopmann, P., Schmidt, R.A.: Uniform interpolation ofALC-ontologies using fix- points. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013). Lecture Notes in Artificial Intelligenc...

    2013 doi

  26. [34]

    In: Bonet, B., Koenig, S

    Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting forALCon- tologies with aboxes. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty- Ninth AAAI Conference on Artificial Intelligence (AAAI-2015). pp. 175–181. AAAI Press (2015)

    2015

  27. [35]

    In: Calvanese, D., Erdem, E., Thielscher, M

    Koopmann, P., Del-Pinto, W., Tourret, S., Schmidt, R.A.: Signature-based abduc- tion for expressive description logics. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowl- edge Representation and Reasonin...

    2020 doi

  28. [36]

    Lin, F., Reiter, R.: Forget it! (1994), presented at the AAAI Fall Symposium on Relevance, New Orleans

    1994

  29. [37]

    In: Demartini, G., Zuccon, G., Culpepper, J.S., Huang, Z., Tong, H

    Liu, Z., Lu, C., Alghamdi, G., Schmidt, R.A., Zhao, Y.: Tracking semantic evo- lutionary changes in large-scale ontological knowledge bases. In: Demartini, G., Zuccon, G., Culpepper, J.S., Huang, Z., Tong, H. (eds.) CIKM’21: The 30th ACM International Conference on Information...

  30. [38]

    In: Baral, C., De Giacomo, G., Eiter, T

    Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for ALC tboxes with applications to logical difference. In: Baral, C., De Giacomo, G., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning (KR 2014). AAAI Press (2014)

    2014

  31. [39]

    Journal of Symbolic Computation7(3-4), 275–293 (1989)

    Martin, U., Nipkow, T.: Boolean Unification – The Story So Far. Journal of Symbolic Computation7(3-4), 275–293 (1989). https://doi.org/10.1016/S0747- 7171(89)80013-6

    1989 doi

  32. [40]

    In: Orłowska, E

    Nonnengart,A.,Szałas,A.:AFixpointApproachtoSecond-OrderQuantifierElim- ination with Applications to Correspondence Theory. In: Orłowska, E. (ed.) Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, Studies in Fuzziness and Soft Computing, vol. 24, pp. 307–328. Spr...

    1998

  33. [41]

    Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mi- haylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala program- ming language (2004), https://infoscience.epfl.ch/handle/20.500.14299/214698 Computing Witnesses Using the SCAN Alg...

    2004

  34. [42]

    In: McRobbie, M.A., Slaney, J.K

    Ohlbach, H.J.: SCAN: Elimination of predicate quantifiers. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction: CADE-13. Lecture Notes in Artificial Intelligence, vol. 1104, pp. 161–165. Springer (1996)

    1996

  35. [43]

    In: Konev, B., Reger, G

    Peuter,D.,Sofronie-Stokkermans,V.:Symboleliminationandapplicationstopara- metric entailment problems. In: Konev, B., Reger, G. (eds.) Frontiers of Combining Systems (FroCoS 2021). Lecture Notes in Computer Science, vol. 12941, pp. 43–62. Springer (2021). https://doi.org/10.100...

    2021 doi

  36. [44]

    North-Holland (1974)

    Rudeanu, S.: Boolean Functions and Equations. North-Holland (1974)

    1974

  37. [45]

    Schröder, E.: Vorlesungen über die Algebra der Logik, vol. 1. Teubner (1890)

  38. [46]

    In: Alechina, N., Baldoni, M., Logan, B

    Toluhi, D., Schmidt, R.A., Parsia, B.: Concept description and definition ex- traction for the ANEMONE system. In: Alechina, N., Baldoni, M., Logan, B. (eds.) Engineering Multi-Agent Systems (EMAS 2021), Revised Selected Papers. Lecture Notes in Computer Science, vol. 13190, p...

    2021 doi

  39. [47]

    In: Dixon, C., Finger, M

    Wernhard, C.: The Boolean Solution Problem from the Perspective of Predicate Logic. In: Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Computer Science, vol. 10483, pp. 333–350. Springer (2017). https://do...

    2017 doi

  40. [1139]

    https://doi.org/10.1145/3459637.3482307

    ACM (2021). https://doi.org/10.1145/3459637.3482307

    2021

Pith tools

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