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