References

  1. Wilhelm Ackermann (1935): Untersuchungen über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen 110(1), pp. 390–413, doi:10.1007/BF01448035.
  2. Heinrich Behmann (1950): Das Auflösungsproblem in der Klassenlogik. Archiv für mathematische Logik und Grundlagenforschung 1(1), pp. 17–29, doi:10.1007/BF01976313. First of two parts.
  3. Heinrich Behmann (1951): Das Auflösungsproblem in der Klassenlogik. Archiv für mathematische Logik und Grundlagenforschung 1(2), pp. 33–51, doi:10.1007/BF01982011. Second of two parts.
  4. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015): Horn Clause Solvers for Program Verification. In: Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner & Wolfram Schulte: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Lecture Notes in Computer Science 9300. Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
  5. Andreas Blass & Yuri Gurevich (1987): Existential Fixed-Point Logic. In: Egon Börger: Computation Theory and Logic, In Memory of Dieter Rödding, Lecture Notes in Computer Science 270. Springer, pp. 20–36, doi:10.1007/3-540-18170-9_151.
  6. Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Robert M. Graham, Michael A. Harrison & Ravi Sethi: 4th ACM Symposium on Principles of Programming Languages. ACM, pp. 238–252, doi:10.1145/512950.512973.
  7. Anuj Dawar & Yuri Gurevich (2002): Fixed point logics. Bulletin of Symbolic Logic 8(1), pp. 65–88, doi:10.2178/bsl/1182353853.
  8. Patrick Doherty, Witold Lukaszewicz & Andrzej Szalas (1997): Computing Circumscription Revisited: A Reduction Algorithm. Journal of Automated Reasoning 18(3), pp. 297–336, doi:10.1023/A:1005722130532.
  9. Patrick Doherty, Witold Łukaszewicz & Andrzej Szałas (1998): General Domain Circumscription and its Effective Reductions. Fundamenta Informaticae 36(1), pp. 23–55, doi:10.3233/FI-1998-3612.
  10. Sebastian Eberhard & Stefan Hetzl (2015): Inductive theorem proving based on tree grammars. Annals of Pure and Applied Logic 166(6), pp. 665–700, doi:10.1016/j.apal.2015.01.002.
  11. Herbert B. Enderton (2001): A Mathematical Introduction to Logic, 2nd edition. Academic Press.
  12. Carsten Fritz (2001): Some Fixed Point Basics. In: Erich Grädel, Wolfgang Thomas & Thomas Wilke: Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science 2500. Springer, pp. 359–364, doi:10.1007/3-540-36387-4_20.
  13. Dov Gabbay & Hans Jürgen Ohlbach (1992): Quantifier Elimination in Second Order Predicate Logic. South African Computer Journal 7, pp. 35–43.
  14. Dov M. Gabbay, Renate A. Schmidt & Andrzej Szałas (2008): Second-Order Quantifier Elimination. College Publications.
  15. Erich Grädel (1991): The Expressive Power of Second Order Horn Logic. In: Christian Choffrut & Matthias Jantzen: 8th Annual Symposium on Theoretical Aspects of Computer Science (STACS), Lecture Notes in Computer Science 480. Springer, pp. 466–477, doi:10.1007/BFb0020821.
  16. Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2014): Generalised Interpolation by Solving Recursion-Free Horn Clauses. In: Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko & Valerio Senni: Proceedings First Workshop on Horn Clauses for Verification and Synthesis (HCVS), EPTCS 169, pp. 31–38, doi:10.4204/EPTCS.169.5.
  17. Arie Gurfinkel & Nikolaj Bjørner (2019): The Science, Art, and Magic of Constrained Horn Clauses. In: 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC. IEEE, pp. 6–10, doi:10.1109/SYNASC49474.2019.00010.
  18. Leon Henkin (1950): Completeness in the Theory of Types. Journal of Symbolic Logic 15(2), pp. 81–91, doi:10.2307/2266967.
  19. Stefan Hetzl & Sebastian Zivota (2020): Decidability of affine solution problems. Journal of Logic and Computation 30(3), pp. 697–714, doi:10.1093/logcom/exz033.
  20. Krystof Hoder, Nikolaj Bjørner & Leonardo Mendonça de Moura (2011): μZ - An Efficient Engine for Fixed Points with Constraints. In: Ganesh Gopalakrishnan & Shaz Qadeer: 23rd International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 6806. Springer, pp. 457–462, doi:10.1007/978-3-642-22110-1_36.
  21. Neil Immerman (1999): Descriptive complexity. Springer, doi:10.1007/978-1-4612-0539-5.
  22. Joxan Jaffar & Michael J. Maher (1994): Constraint Logic Programming: A Survey. The Journal of Logic Programming 19/20, pp. 503–581, doi:10.1016/0743-1066(94)90033-7.
  23. Bishoksan Kafle, John P. Gallagher & José F. Morales (2016): Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In: Swarat Chaudhuri & Azadeh Farzan: 28th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 9779. Springer, pp. 261–268, doi:10.1007/978-3-319-41528-4_14.
  24. Michael Karr (1976): Affine Relationships Among Variables of a Program. Acta Informatica 6, pp. 133–151, doi:10.1007/BF00268497.
  25. Johannes Kloibhofer (2020): A fixed-point theorem for Horn formula equations. TU Wien, Austria.
  26. Ursula Martin & Tobias Nipkow (1989): Boolean Unification – The Story So Far. Journal of Symbolic Computation 7(3-4), pp. 275–293, doi:10.1016/S0747-7171(89)80013-6.
  27. Kenneth L. McMillan (2003): Interpolation and SAT-Based Model Checking. In: Warren A. Hunt Jr. & Fabio Somenzi: Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science 2725. Springer, pp. 1–13, doi:10.1016/S0747-7171(86)80028-1.
  28. Kenneth L. McMillan & Andrey Rybalchenko (2012): Solving Constrained Horn Clauses using Interpolation. Technical Report. Microsoft Research. MSR-TR-2013-06.
  29. Andreas Nonnengart & Andrzej Szałas (1998): A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory, pp. 307–328, Studies in Fuzziness and Soft Computing 24. Springer.
  30. Sergiu Rudeanu (1974): Boolean Functions and Equations. North-Holland.
  31. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Classifying and Solving Horn Clauses for Verification. In: Ernie Cohen & Andrey Rybalchenko: 5th International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Lecture Notes in Computer Science 8164. Springer, pp. 1–21, doi:10.1007/978-3-642-54108-7_1.
  32. Ernst Schröder (1890): Vorlesungen über die Algebra der Logik 1. Teubner.
  33. M. H. Van Emden & R. A. Kowalski (1976): The Semantics of Predicate Logic as a Programming Language. Journal of the ACM 23(4), pp. 733742, doi:10.1145/321978.321991.
  34. Christoph Wernhard: Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas. In: Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017).
  35. Christoph Wernhard (2017): The Boolean Solution Problem from the Perspective of Predicate Logic. In: 11th International Symposium on Frontiers of Combining Systems (FroCoS), Lecture Notes in Computer Science 10483. Springer, pp. 333–350, doi:10.1007/978-3-319-66167-4_19.
  36. Glynn Winskel (1993): The Formal Semantics of Programming Languages – An Introduction. Foundation of computing series. MIT Press, doi:10.7551/mitpress/3054.001.0001.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org