@article(agcadipevi13a,
 author       = {Felicidad Aguado and Pedro Cabalar and Martin Di{\'e}guez and Gilberto P{\'e}rez and Concepci{\'o}n Vidal},
 year         = {2013},
 title        = {Temporal\, equilibrium\, logic:\, a survey},
 journal      = {Journal of Applied Non-Classical Logics},
 volume       = {23},
 number       = {1--2},
 pages        = {2--24},
 doi          = {10.1080/11663081.2013.798985},
)
@inproceedings(bedaei16a,
 author       = {Harald Beck and Dao-Tran, Minh and Thomas Eiter},
 year         = {2016},
 title        = {Equivalent Stream Reasoning Programs},
 editor       = {Kambhampati},
 pages        = {929--935},
)
@article(ar:BeckertPosegga95,
 author       = {Bernhard Beckert and Joachim Posegga},
 year         = {1995},
 title        = {lean{TAP}: Lean Tableau-based Deduction},
 journal      = {Journal of Automated Reasoning},
 volume       = {15},
 number       = {3},
 pages        = {339--358},
 doi          = {10.1007/BF00881804},
)
@book(bo:Bibel87,
 author       = {Wolfgang Bibel},
 year         = {1987},
 title        = {Automated Theorem Proving},
 series       = {Artificial intelligence},
 publisher    = {F. Vieweg und Sohn},
 address      = {Wiesbaden},
 doi          = {10.1007/978-3-322-90102-6},
)
@article(cafafa20a,
 author       = {Pedro Cabalar and Jorge Fandinno and {Fari{\~n}as del Cerro}, Luis},
 year         = {2020},
 title        = {Autoepistemic Answer Set Programming},
 journal      = {Artificial Intelligence},
 volume       = {289},
 pages        = {103382},
 doi          = {10.1016/j.artint.2020.103382},
)
@inproceedings(cakaossc16a,
 author       = {Pedro Cabalar and Roland Kaminski and Max Ostrowski and Torsten Schaub},
 year         = {2016},
 title        = {An {ASP} Semantics for Default Reasoning with Constraints},
 editor       = {Kambhampati},
 pages        = {1015--1021},
)
@misc(faglhaheliliscst25a,
 author       = {Jorge Fandinno and Christoph Glinzer and Zachary Hansen and Jan Heuer and Yuliya Lierler and Vladimir Lifschitz and Torsten Schaub and Tobias Stolzmann},
 year         = {2025},
 title        = {Anthem 2.0: Automated Reasoning for Answer Set Programming},
 url          = {https://arxiv.org/abs/2507.11704},
 note         = {(To appear in TPLP 2025)},
)
@article(falilusc20a,
 author       = {Jorge Fandinno and Vladimir Lifschitz and Patrick L{\"u}hne and Torsten Schaub},
 year         = {2020},
 title        = {Verifying Tight Logic Programs with anthem and {V}ampire},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {20},
 number       = {5},
 pages        = {735--750},
 doi          = {10.1017/S1471068420000344},
)
@book(bo:Fitting83,
 author       = {Melvin Fitting},
 year         = {1983},
 title        = {Proof Methods for Modal and Intuitionistic Logics},
 publisher    = {D.~Reidel},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-017-2794-5},
)
@inproceedings(gellif90a,
 author       = {Michael Gelfond and Vladimir Lifschitz},
 year         = {1990},
 title        = {Logic Programs with Classical Negation},
 editor       = {David Warren and P{\'e}ter Szeredi},
 booktitle    = {Proceedings of the Seventh International Conference on Logic Programming (ICLP'90)},
 publisher    = {{MIT} Press},
 pages        = {579--597},
)
@article(ar:Gentzen35,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"u}ber das {L}ogische {S}chlie{\ss}en},
 journal      = {Mathematische Zeit\-schrift},
 volume       = {39},
 pages        = {176--210, 405--431},
 doi          = {10.1007/BF01201353},
)
@article(goedel32a,
 author       = {Kurt G{\"o}del},
 year         = {1932},
 title        = {Zum intuitionistischen {A}ussagenkalk{\"u}l},
 journal      = {Anzeiger der Akademie der Wissenschaften in Wien},
 pages        = {65--66},
)
@incollection(heyting30a,
 author       = {Arend Heyting},
 year         = {1930},
 title        = {Die formalen {R}egeln der intuitionistischen {L}ogik},
 booktitle    = {Sitzungsberichte der Preussischen Akademie der Wissenschaften},
 publisher    = {Deutsche Akademie der Wissenschaften zu Berlin},
 pages        = {42--56},
)
@proceedings(ijcai16,
 editor       = {Subbarao Kambhampati},
 year         = {2016},
 title        = {Proceedings of the Twenty-fifth International Joint Conference on Artificial Intelligence (IJCAI'16)},
 publisher    = {IJCAI/AAAI Press},
)
@book(lifschitz19a,
 author       = {Vladimir Lifschitz},
 year         = {2019},
 title        = {Answer Set Programming},
 publisher    = {Springer},
 address      = {Cham},
 doi          = {10.1007/978-3-030-24658-7},
)
@article(lipeva01a,
 author       = {Vladimir Lifschitz and David Pearce and Agust{\'{\i}}n Valverde},
 year         = {2001},
 title        = {Strongly equivalent logic programs},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {2},
 number       = {4},
 pages        = {526--541},
 doi          = {10.1145/383779.383783},
)
@inproceedings(lipeva07a,
 author       = {Vladimir Lifschitz and David Pearce and Agust{\'{\i}}n Valverde},
 year         = {2007},
 title        = {A Characterization of Strong Equivalence for Logic Programs with Variables},
 editor       = {Chitta Baral and Gerhard Brewka and John Schlipf},
 booktitle    = {Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07)},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {4483},
 publisher    = {Springer},
 address      = {Heidelberg},
 pages        = {188--200},
 doi          = {10.1007/978-3-540-72200-7_17},
)
@article(ar:Mints10,
 author       = {Grigori Mints},
 year         = {2010},
 title        = {Cut-free formulations for a quantified logic of here and there},
 journal      = {Ann. Pure Appl. Log.},
 volume       = {162},
 number       = {3},
 pages        = {237--242},
 doi          = {10.1016/J.APAL.2010.09.009},
)
@inproceedings(inp:Otten97,
 author       = {Jens Otten},
 year         = {1997},
 title        = {{\mbox{\sf ilean$\!$T$\!$AP}}: An Intuitionistic Theorem Prover},
 editor       = {Didier Galmiche},
 booktitle    = {TABLEAUX 1997},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {1227},
 publisher    = {Springer},
 address      = {Heidelberg},
 pages        = {307--312},
 doi          = {10.1007/BFb0027422},
)
@article(ar:Otten10,
 author       = {Jens Otten},
 year         = {2010},
 title        = {Restricting backtracking in connection calculi},
 journal      = {AI Commun.},
 volume       = {23},
 number       = {2--3},
 pages        = {159--182},
 doi          = {10.3233/AIC-2010-0464},
)
@inproceedings(inp:Otten11,
 author       = {Jens Otten},
 year         = {2011},
 title        = {A Non-clausal Connection Calculus},
 editor       = {Kai Br{\"u}nnler and George Metcalfe},
 booktitle    = {TABLEAUX 2011},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {6793},
 publisher    = {Springer},
 address      = {Heidelberg},
 pages        = {226--241},
 doi          = {10.1007/978-3-642-22119-4_18},
)
@inproceedings(inp:Otten16,
 author       = {Jens Otten},
 year         = {2016},
 title        = {{{\sf nanoCoP}}: {A} Non-clausal Connection Prover},
 editor       = {Nicola Olivetti and Ashish Tiwari},
 booktitle    = {IJCAR 2016},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {9706},
 publisher    = {Springer},
 address      = {Heidelberg},
 pages        = {302--312},
 doi          = {10.1007/978-3-319-40229-1_21},
)
@inproceedings(inp:Otten17b,
 author       = {Jens Otten},
 year         = {2017},
 title        = {Non-clausal Connection Calculi for Non-classical Logics},
 editor       = {Renate Schmidt and Cl\'{a}udia Nalon},
 booktitle    = {TABLEAUX 2017},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {10501},
 publisher    = {Springer},
 address      = {Cham},
 pages        = {209--227},
 doi          = {10.1007/978-3-319-66902-1_13},
)
@inproceedings(inp:Otten21,
 author       = {Jens Otten},
 year         = {2021},
 title        = {The {{\sf nanoCoP} 2.0} Connection Provers for Classical, Intuitionistic and Modal Logics},
 editor       = {Anupam Das and Sara Negri},
 booktitle    = {TABLEAUX 2021},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {12842},
 publisher    = {Springer},
 address      = {Cham},
 pages        = {236--249},
 doi          = {10.1007/978-3-030-86059-2\_14},
)
@article(ar:OttenBibel03,
 author       = {Jens Otten and Wolfgang Bibel},
 year         = {2003},
 title        = {{{\sf leanCoP}}: lean connection-based theorem proving},
 journal      = {Journal of Symbolic Computation},
 volume       = {36},
 number       = {1--2},
 pages        = {139--161},
 doi          = {10.1016/S0747-7171(03)00037-3},
)
@inproceedings(inp:OttenBibel17,
 author       = {Jens Otten and Wolfgang Bibel},
 year         = {2017},
 title        = {Advances in Connection-Based Automated Theorem Proving},
 editor       = {Mike Hinchey and Jonathan P. Bowen and Ernst-R{\"u}diger Olderog},
 booktitle    = {Provably Correct Systems},
 series       = {NASA Monographs in Systems and Software Engineering},
 publisher    = {Springer},
 address      = {Cham},
 pages        = {211--241},
 doi          = {10.1007/978-3-319-48628-4_9},
)
@article(pearce06a,
 author       = {David Pearce},
 year         = {2006},
 title        = {Equilibrium logic},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 volume       = {47},
 number       = {1--2},
 pages        = {3--41},
 doi          = {10.1007/s10472-006-9028-z},
)
@inproceedings(peguva00a,
 author       = {David Pearce and {de Guzm{\'a}n}, Inmaculada and August{\'i}n Valverde},
 year         = {2000},
 title        = {A Tableau Calculus for Equilibrium Entailment},
 editor       = {Roy Dyckhoff},
 booktitle    = {Proceedings of the Ninth International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1847},
 publisher    = {Springer},
 address      = {Heidelberg},
 pages        = {352--367},
 doi          = {10.1007/10722086_28},
)
@article(peaval05a,
 author       = {David Pearce and August{\'i}n Valverde},
 year         = {2005},
 title        = {A First Order Nonmonotonic Extension of Constructive Logic},
 journal      = {Studia Logica},
 volume       = {30},
 number       = {2--3},
 pages        = {321--346},
 doi          = {10.1007/s11225-005-8473-8},
)
@article(ar:Pelletier86,
 author       = {Francis Jeffry Pelletier},
 year         = {1986},
 title        = {Seventy-Five Problems for Testing Automatic Theorem Provers},
 journal      = {Journal of Automated Reasoning},
 volume       = {2},
 number       = {2},
 pages        = {191--216},
 doi          = {10.1007/BF02432151},
)
@article(ar:RathsOttenKreitz07,
 author       = {Thomas Raths and Jens Otten and Christoph Kreitz},
 year         = {2007},
 title        = {The {ILTP} problem library for intuitionistic logic},
 journal      = {Journal of Automated Reasoning},
 volume       = {38},
 pages        = {261--271},
 doi          = {10.1007/s10817-006-9060-z},
)
@book(bo:Smullyan68,
 author       = {Raymond M. Smullyan},
 year         = {1968},
 title        = {First-Order Logic},
 series       = {Ergebnisse der Mathematik und ihrer Grenzgebiete},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg, New York},
 doi          = {10.1007/978-3-642-86718-7},
)
@book(bo:Wallen90,
 author       = {Lincoln A. Wallen},
 year         = {1990},
 title        = {Automated Deduction in Nonclassical Logics},
 publisher    = {MIT Press},
 address      = {Cambridge, Mass.},
)