Wilhelm Ackermann (1935):
Untersuchungen über das Eliminationsproblem der mathematischen Logik.
Mathematische Annalen 110(1),
pp. 390–413,
doi:10.1007/BF01448035.
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.
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.
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.
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.
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.
Anuj Dawar & Yuri Gurevich (2002):
Fixed point logics.
Bulletin of Symbolic Logic 8(1),
pp. 65–88,
doi:10.2178/bsl/1182353853.
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.
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.
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.
Herbert B. Enderton (2001):
A Mathematical Introduction to Logic,
2nd edition.
Academic Press.
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.
Dov Gabbay & Hans Jürgen Ohlbach (1992):
Quantifier Elimination in Second Order Predicate Logic.
South African Computer Journal 7,
pp. 35–43.
Dov M. Gabbay, Renate A. Schmidt & Andrzej Szałas (2008):
Second-Order Quantifier Elimination.
College Publications.
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.
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.
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.
Leon Henkin (1950):
Completeness in the Theory of Types.
Journal of Symbolic Logic 15(2),
pp. 81–91,
doi:10.2307/2266967.
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.
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.
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.
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.
Michael Karr (1976):
Affine Relationships Among Variables of a Program.
Acta Informatica 6,
pp. 133–151,
doi:10.1007/BF00268497.
Johannes Kloibhofer (2020):
A fixed-point theorem for Horn formula equations.
TU Wien,
Austria.
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.
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.
Kenneth L. McMillan & Andrey Rybalchenko (2012):
Solving Constrained Horn Clauses using Interpolation.
Technical Report.
Microsoft Research.
MSR-TR-2013-06.
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.
Sergiu Rudeanu (1974):
Boolean Functions and Equations.
North-Holland.
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.
Ernst Schröder (1890):
Vorlesungen über die Algebra der Logik 1.
Teubner.
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.
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).
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.
Glynn Winskel (1993):
The Formal Semantics of Programming Languages – An Introduction.
Foundation of computing series.
MIT Press,
doi:10.7551/mitpress/3054.001.0001.