pith. machine review for the scientific record. sign in

arxiv: 2604.27939 · v1 · submitted 2026-04-30 · 💻 cs.LO

Recognition: unknown

Computing Witnesses Using the SCAN Algorithm

Fabian Achammer , Stefan Hetzl , Renate A. Schmidt
Authors on Pith no claims yet

Pith reviewed 2026-05-07 07:07 UTC · model grok-4.3

classification 💻 cs.LO
keywords second-order quantifier eliminationSCAN algorithmwitness computationclause setssaturationfirst-order logiclogical equivalencequantifier elimination
0
0 comments X

The pith

The SCAN algorithm on clause sets can be extended to compute witnesses for second-order quantifiers that yield logically equivalent first-order formulas.

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

This paper shows how to modify the SCAN algorithm, a saturation-based procedure for eliminating second-order quantifiers from clause sets, so that it also produces a witness for those quantifiers. The witness is a first-order formula that, when substituted for the second-order predicates, gives a formula logically equivalent to the input. The extension works by tracking substitutions throughout the saturation steps while preserving the original algorithm's termination and equivalence properties. A prototype implementation confirms that the method is feasible in practice. Readers interested in computational logic would care because explicit witnesses support further tasks such as interpolation or proof extraction that depend on the elimination result.

Core claim

The paper establishes that the SCAN algorithm can be extended on clause sets to solve the more general problem of finding a witness for the second-order quantifiers. This witness, when used to replace the second-order predicates, produces a first-order formula that is logically equivalent to the original formula containing second-order quantifiers. The extension is achieved by adapting the saturation process to compute and maintain the witness information. The paper additionally provides a prototype implementation of the proposed method.

What carries the argument

The modified saturation process of SCAN that tracks and preserves witness substitutions for second-order predicates during resolution and simplification steps on clause sets.

Load-bearing premise

The modifications to the saturation process correctly compute and preserve the witness while maintaining logical equivalence and the termination properties of the original SCAN algorithm.

What would settle it

A concrete input clause set for which the extended SCAN produces a witness W such that the first-order formula obtained by substituting W for the second-order predicates is not logically equivalent to the original formula, or on which the extended algorithm fails to terminate while the original SCAN succeeds.

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 saturation-based SCAN algorithm. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding a witness for the second-order quantifiers that results in a logically equivalent first-order formula. In addition, we provide a prototype implementation of the proposed method.

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

0 major / 3 minor

Summary. The paper extends the SCAN saturation algorithm for second-order quantifier elimination on clause sets to compute not only an equivalent first-order formula but also a witness for the eliminated second-order quantifiers. The extension augments the generation of resolvents with witness terms and extracts both the formula and witness from the saturated clause set. A prototype implementation is provided.

Significance. If the modifications preserve SCAN's termination and equivalence properties while correctly recording witnesses, the result would be a useful generalization with applications in automated reasoning, model generation, and explanation tasks. The prototype strengthens the practical contribution by enabling direct experimentation.

minor comments (3)
  1. The abstract and introduction claim that the extension maintains logical equivalence and termination, but the text would benefit from an explicit statement (perhaps in a dedicated subsection) of the precise conditions under which these properties are preserved, analogous to the original SCAN analysis.
  2. The prototype is mentioned but receives no description of its input language, output format, or test cases; adding a short implementation section or appendix with usage examples would improve reproducibility and allow readers to verify the witness extraction step.
  3. Notation for witness terms and their integration into resolvents is introduced without a consolidated table or running example that shows the full input-to-output transformation on a small clause set; this would clarify the augmentation process.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our paper and for recommending minor revision. The assessment correctly captures the core contribution: extending SCAN to compute witnesses alongside quantifier elimination. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; extension is explicitly algorithmic

full rationale

The derivation consists of an explicit modification to the SCAN saturation procedure: resolvents are augmented with witness terms during generation, and a first-order formula plus witness is extracted from the saturated clause set. This is presented with a full algorithmic description and a prototype implementation, allowing independent verification of equivalence preservation and termination. No equation or step reduces by construction to a fitted input or self-definition; the central claim does not rely on load-bearing self-citations whose content is itself unverified within the paper. The work builds directly on the independently established SCAN algorithm without renaming known results or smuggling ansatzes via citation chains.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper extends an existing algorithm in logic, relying on standard background results rather than introducing new fitted parameters or entities. Assessment is limited by abstract-only access.

axioms (1)
  • standard math Standard properties of first-order logic, clause sets, and saturation under resolution-like rules
    The SCAN algorithm and its extension presuppose these background results from computational logic.

pith-pipeline@v0.9.0 · 5392 in / 1078 out tokens · 47242 ms · 2026-05-07T07:07:21.932767+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

53 extracted references · 31 canonical work pages

  1. [1]

    South African Computer Journal7, 35–43 (1992) 56

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

    1992

  2. [2]

    College Publications, London (2008)

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

    2008

  3. [3]

    Computers and Mathematics with Applications29(2), 73–90 (1995) https://doi.org/10.1016/ 0898-1221(94)00217-9

    Brink, C., Gabbay, D.M., Ohlbach, H.J.: Towards automating duality. Computers and Mathematics with Applications29(2), 73–90 (1995) https://doi.org/10.1016/ 0898-1221(94)00217-9

    1995

  4. [4]

    In: Berghammer, R., M¨ oller, B., Struth, G

    Goranko, V., Hustadt, U., Schmidt, R.A., Vakarelov, D.: SCAN is complete for all Sahlqvist formulae. In: Berghammer, R., M¨ oller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science, vol. 3051, pp. 149–162. Springer, Berlin, Heidelberg (2003). https://doi.org/10.1007/978-3-540-2...

    work page doi:10.1007/978-3-540-24771-5 2003

  5. [5]

    The core algorithm SQEMA

    Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic: I. The core algorithm SQEMA. Logical Meth- ods in Computer Science2(1:5), 1–26 (2006) https://doi.org/10.2168/LMCS-2(1: 5)2006

    work page doi:10.2168/lmcs-2(1: 2006

  6. [6]

    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, Cham (2014). https://doi.org/10.1007/978-3-319-06025-5 36

    work page doi:10.1007/978-3-319-06025-5 2014

  7. [7]

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

    1994

  8. [8]

    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.org/papers09/Papers/IJCAI09-142.pdf

    2009

  9. [9]

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

    Koopmann, P., Schmidt, R.A.: Uniform interpolation ofALC-ontologies using fixpoints. 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 Intelligence, vol. 8152, pp. 87–102. Springer, Berlin, Heidelberg (2013). https://doi.org/10....

    work page doi:10.1007/978-3-642-40885-4 2013

  10. [10]

    https://doi.org/10.1007/978-3-642-45221-5 44

    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). Lecture Notes in Computer Science, vol. 8312, pp. 552–567. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5 37

    work page doi:10.1007/978-3-642-45221-5 2013

  11. [11]

    Journal of Artificial Intelligence Research60, 1165–1213 (2017) https://doi.org/10.1613/JAIR.5530

    Delgrande, J.P.: A knowledge level account of forgetting. Journal of Artificial Intelligence Research60, 1165–1213 (2017) https://doi.org/10.1613/JAIR.5530

    work page doi:10.1613/jair.5530 2017

  12. [12]

    In: Benzm¨ uller, C., Heule, M.J.H., Schmidt, R.A

    F´ er´ ee, H., Giessen, I., Gool, S., Shillito, I.: Mechanised uniform interpolation for modal logics k, gl, and isl. In: Benzm¨ uller, C., Heule, M.J.H., Schmidt, R.A. 57 (eds.) Automated Reasoning (IJCAR 2024). Lecture Notes in Computer Sci- ence, vol. 14740, pp. 43–60. Springer, Cham (2024). https://doi.org/10.1007/ 978-3-031-63501-4 3

    2024

  13. [13]

    In: Nebel, B

    Doherty, P., Lukaszewicz, W., Szalas, A.: Computing strongest necessary and weakest sufficient conditions of first-order formulas. In: Nebel, B. (ed.) Proceed- ings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 145–154. Morgan Kaufmann, San Francisco (2001)

    2001

  14. [14]

    K¨ unstliche Intelligenz33(1), 9–33 (2019) https://doi.org/10.1007/S13218-018-0564-6

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

    work page doi:10.1007/s13218-018-0564-6 2019

  15. [15]

    Theory and Practice of Logic Programming23(1), 111–156 (2023) https: //doi.org/10.1017/S1471068421000570

    Gon¸ calves, R., Knorr, M., Leite, J.: Forgetting in answer set programming: A survey. Theory and Practice of Logic Programming23(1), 111–156 (2023) https: //doi.org/10.1017/S1471068421000570

    work page doi:10.1017/s1471068421000570 2023

  16. [16]

    In: Proceedings of the 10th International Conference on Knowl- edge Capture (K-CAP)

    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. ACM, New York (2019). https://doi.org/10. 1145/3360901.3364424

    work page arXiv 2019

  17. [17]

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

    Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting forALC 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

  18. [18]

    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 and Knowledge Management, pp. 1130–1139. ACM, New York (2021). https://doi.org/...

    work page doi:10.1145/3459637.3482307 2021

  19. [19]

    19 Domenico Lembo, Maurizio Lenzerini, Riccardo Rosati, Marco Ruzzi, and Domenico Fabio Savo

    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 Reasoning (KR 2020), pp. 592–602. AI Press, ??? (2020). https://doi.org/10.24963/kr.2020/59

    work page doi:10.24963/kr.2020/59 2020

  20. [20]

    Sledgehammer: Judgement day,

    Hoder, K., Kov´ acs, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., H¨ ahnle, R. (eds.) Automated Reasoning (IJCAR 2010). Lecture Notes in Computer Science, vol. 6173, pp. 188–195. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1 16

    work page doi:10.1007/978-3-642-14203-1 2010

  21. [21]

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

    Khasidashvili, Z., Korovin, K.: Predicate elimination for preprocessing in first- order theorem proving. In: Creignou, N., Berre, D.L. (eds.) Theory and 58 Applications of Satisfiability Testing (SAT 2016). Lecture Notes in Computer Science, vol. 9710, pp. 361–372. Springer, Cham (2016). https://doi.org/10.1007/ 978-3-319-40970-2 22

    2016

  22. [22]

    In: Konev, B., Reger, G

    Peuter, D., Sofronie-Stokkermans, V.: Symbol elimination and applications to parametric entailment problems. In: Konev, B., Reger, G. (eds.) Frontiers of Com- bining Systems (FroCoS 2021). Lecture Notes in Computer Science, vol. 12941, pp. 43–62. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-86205-3 3

    work page doi:10.1007/978-3-030-86205-3 2021

  23. [23]

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

    Doherty, P., Szalas, A.: On the correspondence between approximations and sim- ilarity. 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–152. Springer, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25929-9 16

    work page doi:10.1007/978-3-540-25929-9 2004

  24. [24]

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

    Toluhi, D., Schmidt, R.A., Parsia, B.: Concept description and definition extrac- tion for the ANEMONE system. In: Alechina, N., Baldoni, M., Logan, B. (eds.) Engineering Multi-Agent Systems (EMAS 2021), Revised Selected Papers. Lec- ture Notes in Computer Science, vol. 13190, pp. 352–372. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-97457-2 20

    work page doi:10.1007/978-3-030-97457-2 2021

  25. [25]

    Journal of Automated Reasoning18(3), 297–336 (1997) https://doi.org/10.1023/A:1005722130532

    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

    work page doi:10.1023/a:1005722130532 1997

  26. [26]

    Fundamenta Informaticae36(1), 23–55 (1998) https://doi

    Doherty, P., Lukaszewicz, W., Sza las, A.: General domain circumscription and its effective reductions. Fundamenta Informaticae36(1), 23–55 (1998) https://doi. org/10.3233/FI-1998-3612

    work page doi:10.3233/fi-1998-3612 1998

  27. [27]

    In: Or lowska, E

    Nonnengart, A., Sza las, A.: A fixpoint approach to second-order quantifier elimi- nation with applications to correspondence theory. In: Or lowska, E. (ed.) Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa. Studies in Fuzziness and Soft Computing, vol. 24, pp. 307–328. Springer, ??? (1998)

    1998

  28. [28]

    Diplomar- beit, Fachbereich Informatik, Universit¨ at des Saarlandes, Saarbr¨ ucken, Germany (October 1996)

    Engel, T.: Quantifier elimination in second-order predicate logic. Diplomar- beit, Fachbereich Informatik, Universit¨ at des Saarlandes, Saarbr¨ ucken, Germany (October 1996)

    1996

  29. [29]

    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, Berlin, Heidelberg (1996). https: //doi.org/10.1007/3-540-61511-3 77

    work page doi:10.1007/3-540-61511-3 1996

  30. [30]

    Applicable Algebra in Engineering, Communication and Computing5, 193–212 (1994) https://doi.org/10.1007/BF01190829 59

    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 59

    work page doi:10.1007/bf01190829 1994

  31. [31]

    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, Cham (2019). https://doi.org/10.1007/978-3-030-22102-7 2

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

  32. [32]

    Mathematische Annalen110(1), 390–413 (1935) https://doi.org/10

    Ackermann, W.: Untersuchungen ¨ uber das Eliminationsproblem der mathematis- chen Logik. Mathematische Annalen110(1), 390–413 (1935) https://doi.org/10. 1007/BF01448035

    1935

  33. [33]

    In: Olivetti, N., Tiwari, A

    Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: Gapt 2.0. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning, pp. 293–301. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1 20

    work page doi:10.1007/978-3-319-40229-1 2016

  34. [34]

    In: Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceed- ings, pp

    Achammer, F., Hetzl, S., Schmidt, R.A.: Computing witnesses using the SCAN algorithm. In: Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceed- ings, pp. 511–531. Springer, Berlin, Heidelberg (2025). https://doi.org/10.1007/ 978-3-031-99984-0 27

    2025

  35. [35]

    Schr¨ oder, E.: Vorlesungen ¨ uber die Algebra der Logik vol. 1. Teubner, Leipzig (1890)

  36. [36]

    North-Holland, Amsterdam (1974)

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

    1974

  37. [37]

    Journal of Symbolic Computation7(3-4), 275–293 (1989) https://doi.org/10.1016/ S0747-7171(89)80013-6

    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

  38. [38]

    Archiv f¨ ur mathe- matische Logik und Grundlagenforschung1(1), 17–29 (1950) https://doi.org/10

    Behmann, H.: Das Aufl¨ osungsproblem in der Klassenlogik. Archiv f¨ ur mathe- matische Logik und Grundlagenforschung1(1), 17–29 (1950) https://doi.org/10. 1007/BF01976313 . first of two parts

    1950

  39. [39]

    Archiv f¨ ur mathe- matische Logik und Grundlagenforschung1(2), 33–51 (1951) https://doi.org/10

    Behmann, H.: Das Aufl¨ osungsproblem in der Klassenlogik. Archiv f¨ ur mathe- matische Logik und Grundlagenforschung1(2), 33–51 (1951) https://doi.org/10. 1007/BF01982011 . second of two parts

    1951

  40. [40]

    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. Lec- ture Notes in Computer Science, vol. 9300, pp. 24–5...

    work page doi:10.1007/978-3-319-23534-9 2015

  41. [41]

    Implementing crash-resistance and non-interference in logic-based argumen- tation

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

    work page doi:10.1093/logcom/ 2017

  42. [42]

    In: Hojjat, H., Kafle, B

    Hetzl, S., Kloibhofer, J.: A fixed-point theorem for Horn formula equations. In: Hojjat, H., Kafle, B. (eds.) 8th Workshop on Horn Clauses for Verifica- tion and Synthesis (HCVS). Electronic Proceedings in Theoretical Computer Science, vol. 344, pp. 65–78. Open Publishing Association, ??? (2021). https: //doi.org/10.4204/EPTCS.344.5

    work page doi:10.4204/eptcs.344.5 2021

  43. [43]

    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.) Pro- ceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE). CEUR Workshop Proceedings, vol. 3009, pp. 59–60. CEUR-WS.org, ??? (2021).https://ceur-ws.org/Vol-3009/abstract2.pdf

    2021

  44. [44]

    ACM Transactions on Computational Logic (2025) https://doi.org/ 10.1145/3779416

    Hetzl, S., Kloibhofer, J.: An abstract fixed-point theorem for Horn formula equations. ACM Transactions on Computational Logic (2025) https://doi.org/ 10.1145/3779416

    work page doi:10.1145/3779416 2025

  45. [45]

    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, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4 19

    work page doi:10.1007/978-3-319-66167-4 2017

  46. [46]

    Gr \" a del, W

    Fritz, C.: In: Gr¨ adel, E., Thomas, W., Wilke, T. (eds.) Some fixed point basics, pp. 359–364. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/ 3-540-36387-4 20 .https://doi.org/10.1007/3-540-36387-4 20

    work page doi:10.1007/3-540-36387-4 2002

  47. [47]

    In: Robinson, A., Voronkov, A

    Nieuwenhuis, R., Rubio, A.: Chapter 7 - Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Hand- book of Automated Reasoning, pp. 371–443. North-Holland, Amsterdam (2001). https://doi.org/10.1016/B978-044450813-3/50009-6

    work page doi:10.1016/b978-044450813-3/50009-6 2001

  48. [48]

    https://infoscience.epfl.ch/handle/20.500.14299/ 214698

    Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An Overview of the Scala Programming Language (2004). https://infoscience.epfl.ch/handle/20.500.14299/ 214698

    2004

  49. [49]

    Formal Methods in System Design47(1), 1–25 (2015) https://doi

    R¨ ummer, P., Hojjat, H., Kuncak, V.: On recursion-free Horn clauses and Craig interpolation. Formal Methods in System Design47(1), 1–25 (2015) https://doi. org/10.1007/s10703-014-0219-7

    work page doi:10.1007/s10703-014-0219-7 2015

  50. [50]

    In: Baier, C., Tinelli, C

    Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free Horn clauses via sampling. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems, pp. 149–163. Springer, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0 10

    work page doi:10.1007/978-3-662-46681-0 2015

  51. [51]

    Cambridge University Press, New York (1997) 61

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

    1997

  52. [52]

    In: Bonet, B., Koenig, S

    Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting forALC ontologies 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). https://doi.org/10.1609/aaai.v29i1.9206

    work page doi:10.1609/aaai.v29i1.9206 2015

  53. [53]

    In: Fern´ andez-Duque, D., Palmigiano, A., Pinchinat, S

    Alassaf, R., Schmidt, R.A., Sattler, U.: Saturation-based uniform interpolation for multi-modal logics. In: Fern´ andez-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 62

    2022