@article(ABN98,
 author       = {Hajnal Andr{\'e}ka and Johan van Benthem and Istvan N\'{e}meti},
 year         = {1998},
 title        = {Modal Languages and Bounded Fragments of Predicate Logic},
 journal      = {Journal of Philosophical Logic},
 volume       = {27},
 pages        = {217--274},
 doi          = {10.1023/A:1004275029985},
)
@article(AndrekaHN99,
 author       = {Hajnal Andr{\'{e}}ka and Ian M. Hodkinson and Istv{\'{a}}n N{\'{e}}meti},
 year         = {1999},
 title        = {Finite Algebras of Relations Are Representable on Finite Sets},
 journal      = {J. Symb. Log.},
 volume       = {64},
 number       = {1},
 pages        = {243--267},
 doi          = {10.2307/2586762},
)
@article(BaranyB12,
 author       = {Vince B{\'{a}}r{\'{a}}ny and Miko{\l}aj Boja{\'{n}}czyk},
 year         = {2012},
 title        = {Finite satisfiability for guarded fixpoint logic},
 journal      = {Inf. Process. Lett.},
 volume       = {112},
 number       = {10},
 pages        = {371--375},
 doi          = {10.1016/j.ipl.2012.02.005},
)
@article(BtCS15,
 author       = {Vince B{\'{a}}r{\'{a}}ny and Balder ten Cate and Luc Segoufin},
 year         = {2015},
 title        = {Guarded Negation},
 journal      = {J. {ACM}},
 volume       = {62},
 number       = {3},
 pages        = {22},
 doi          = {10.1145/2701414},
)
@article(BGO13,
 author       = {Vince B{\'{a}}r{\'{a}}ny and Georg Gottlob and Martin Otto},
 year         = {2014},
 title        = {Querying the Guarded Fragment},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {2},
 doi          = {10.2168/LMCS-10(2:3)2014},
)
@book(HandbookML,
 editor       = {Patrick Blackburn and Johan van Benthem and Frank Wolter},
 year         = {2006},
 title        = {Handbook of Modal Logic},
 publisher    = {Elsevier Science Inc.},
 address      = {New York},
)
@article(BDM11,
 author       = {Miko{\l}aj Boja{\'{n}}czyk and Claire David and Anca Muscholl and Thomas Schwentick and Luc Segoufin},
 year         = {2011},
 title        = {Two-variable logic on data words},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {12},
 number       = {4},
 pages        = {27},
 doi          = {10.1145/1970398.1970403},
)
@inproceedings(CW15,
 author       = {Witold Charatonik and Piotr Witkowski},
 year         = {2015},
 title        = {Two-variable Logic with Counting and a Linear Order},
 booktitle    = {Computer Science Logic},
 series       = {LIPIcs},
 volume       = {41},
 publisher    = {Schlo{\ss} Dagsuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {631--647},
 doi          = {10.4230/LIPIcs.CSL.2015.631},
)
@article(FischerL79,
 author       = {Michael J. Fischer and Richard E. Ladner},
 year         = {1979},
 title        = {Propositional Dynamic Logic of Regular Programs},
 journal      = {J. Comput. Syst. Sci.},
 volume       = {18},
 number       = {2},
 pages        = {194--211},
 doi          = {10.1016/0022-0000(79)90046-1},
)
@incollection(gabbay1981,
 author       = {Dov M Gabbay},
 year         = {1981},
 title        = {An irreflexivity lemma with applications to axiomatizations of conditions on tense frames},
 booktitle    = {Aspects of philosophical logic},
 publisher    = {Springer},
 pages        = {67--89},
 doi          = {10.1007/978-94-009-8384-7_3},
)
@inproceedings(GMV99,
 author       = {Harald Ganzinger and Christoph Meyer and Margus Veanes},
 year         = {1999},
 title        = {The Two-Variable Guarded Fragment with Transitive Relations},
 booktitle    = {14th Annual {IEEE} Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999},
 pages        = {24--34},
 doi          = {10.1109/LICS.1999.782582},
)
@article(Gra99,
 author       = {Erich Gr{\"{a}}del},
 year         = {1999},
 title        = {On The Restraining Power of Guards},
 journal      = {J. Symb. Log.},
 volume       = {64},
 number       = {4},
 pages        = {1719--1742},
 doi          = {10.2307/2586808},
)
@article(GKV97,
 author       = {Erich Gr{\"a}del and Phokion Kolaitis and Moshe Vardi},
 year         = {1997},
 title        = {On the decision problem for two-variable first-order logic},
 journal      = {Bulletin of Symbolic Logic},
 volume       = {3},
 number       = {1},
 pages        = {53--69},
 doi          = {10.2307/421196},
)
@inproceedings(GOR97,
 author       = {Erich Gr{\"{a}}del and Martin Otto and Eric Rosen},
 year         = {1997},
 title        = {Two-Variable Logic with Counting is Decidable},
 booktitle    = {Proceedings, 12th Annual {IEEE} Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997},
 pages        = {306--317},
 doi          = {10.1109/LICS.1997.614957},
)
@article(GOR99,
 author       = {Erich Gr{\"{a}}del and Martin Otto and Eric Rosen},
 year         = {1999},
 title        = {Undecidability results on two-variable logics},
 journal      = {Arch. Math. Log.},
 volume       = {38},
 number       = {4-5},
 pages        = {313--354},
 doi          = {10.1007/s001530050130},
)
@inproceedings(GW99,
 author       = {Erich Gr{\"{a}}del and Igor Walukiewicz},
 year         = {1999},
 title        = {Guarded Fixed Point Logic},
 booktitle    = {14th Annual {IEEE} Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999},
 pages        = {45--54},
 doi          = {10.1109/LICS.1999.782585},
)
@inproceedings(GarciaLS14,
 author       = {Ib{\'{a}}{\~{n}}ez{-}Garc{\'{\i}}a, Yazmin Ang{\'{e}}lica and Carsten Lutz and Thomas Schneider},
 year         = {2014},
 title        = {Finite Model Reasoning in Horn Description Logics},
 booktitle    = {Principles of Knowledge Representation and Reasoning: Proceedings of the 14th International Conference, {KR} 2014, Vienna, Austria, July 20-24, 2014},
 url          = {http://www.aaai.org/ocs/index.php/KR/KR14/paper/view/7927},
)
@article(KMW62,
 author       = {A.S. Kahr and E.F. Moore and H. Wang},
 year         = {1962},
 title        = {Entscheidungsproblem reduced to the $\forall\exists \forall$ case},
 journal      = {Proc. Nat. Acad. Sci. U.S.A.},
 volume       = {48},
 pages        = {365--377},
 doi          = {10.1073/pnas.48.3.365},
)
@phdthesis(Kaz06,
 author       = {Y. Kazakov},
 year         = {2006},
 title        = {Saturation-based decision procedures for extensions of the guarded fragment},
 school       = {Universit\"at des Saarlandes},
 address      = {Saarbr\"ucken, Germany},
)
@inproceedings(Kie03,
 author       = {Emanuel Kiero\'{n}ski},
 year         = {2003},
 title        = {The Two-Variable Guarded Fragment with Transitive Guards Is 2EXPTIME-Hard},
 booktitle    = {Foundations of Software Science and Computational Structures, 6th International Conference, {FOSSACS} 2003, Warsaw, Poland, April 7-11, 2003, Proceedings},
 pages        = {299--312},
 doi          = {10.1007/3-540-36576-1_19},
)
@inproceedings(Kie05,
 author       = {Emanuel Kiero\'{n}ski},
 year         = {2005},
 title        = {Results on the Guarded Fragment with Equivalence or Transitive Relations},
 booktitle    = {Computer Science Logic, 19th International Workshop, {CSL} 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings},
 pages        = {309--324},
 doi          = {10.1007/11538363_22},
)
@inproceedings(Kie2011,
 author       = {Emanuel Kiero\'{n}ski},
 year         = {2011},
 title        = {Decidability Issues for Two-Variable Logics with Several Linear Orders},
 booktitle    = {Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, {CSL} 2011, September 12-15, 2011, Bergen, Norway, Proceedings},
 pages        = {337--351},
 doi          = {10.4230/LIPIcs.CSL.2011.337},
)
@article(KMP-HT14,
 author       = {Emanuel Kiero\'{n}ski and Jakub Michaliszyn and Pratt-Hartmann, Ian and Lidia Tendera},
 year         = {2014},
 title        = {Two-variable first-order logic with equivalence closure},
 journal      = {SIAM Journal of Computing},
 volume       = {43},
 number       = {3},
 pages        = {1012--1063},
 doi          = {10.1137/120900095},
)
@inproceedings(KO05,
 author       = {Emanuel Kiero\'{n}ski and M. Otto},
 year         = {2005},
 title        = {Small Substructures and Decidability Issues for First-Order Logic with Two Variables},
 booktitle    = {20th {IEEE} Symposium on Logic in Computer Science {(LICS} 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings},
 pages        = {448--457},
 doi          = {10.1109/LICS.2005.49},
)
@article(KP-HT15,
 author       = {Emanuel Kiero\'nski and Pratt-Hartmann, Ian and Lidia Tendera},
 year         = {2015},
 title        = {Equivalence closure in the two-variable guarded fragment},
 journal      = {Journal of Logic and Computation},
 doi          = {10.1093/logcom/exv075},
)
@inproceedings(KT09,
 author       = {Emanuel Kiero\'{n}ski and L. Tendera},
 year         = {2009},
 title        = {On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations},
 booktitle    = {Proceedings of the 24th Annual {IEEE} Symposium on Logic in Computer Science, {LICS} 2009, 11-14 August 2009, Los Angeles, CA, {USA}},
 pages        = {123--132},
 doi          = {10.1109/LICS.2009.39},
)
@unpublished(KT-FinSatGFTG,
 author       = {Emanuel Kiero\'{n}ski and Lidia Tendera},
 title        = {Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants},
 url          = {https://arxiv.org/abs/1611.03267},
 note         = {Submitted},
)
@inproceedings(KT07,
 author       = {Emanuel Kiero\'{n}ski and Lidia Tendera},
 year         = {2007},
 title        = {On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, {LPAR} 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings},
 pages        = {318--332},
 doi          = {10.1007/978-3-540-75560-9_24},
)
@inproceedings(Kosaraju82,
 author       = {S. Rao Kosaraju},
 year         = {1982},
 title        = {Decidability of Reachability in Vector Addition Systems (Preliminary Version)},
 booktitle    = {Proceedings of the 14th Annual {ACM} Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, {USA}},
 pages        = {267--281},
 doi          = {10.1145/800070.802201},
)
@article(LST05,
 author       = {Carsten Lutz and Ulrike Sattler and Lidia Tendera},
 year         = {2005},
 title        = {The complexity of finite model reasoning in description logics},
 journal      = {Inf. Comput.},
 volume       = {199},
 number       = {1-2},
 pages        = {132--171},
 doi          = {10.1016/j.ic.2004.11.002},
)
@inproceedings(Michaliszyn09,
 author       = {Jakub Michaliszyn},
 year         = {2009},
 title        = {Decidability of the Guarded Fragment with the Transitive Closure},
 booktitle    = {Automata, Languages and Programming, 36th Internatilonal Colloquium, {ICALP} 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part {II}},
 pages        = {261--272},
 doi          = {10.1007/978-3-642-02930-1_22},
)
@inproceedings(MichOW12,
 author       = {Jakub Michaliszyn and Jan Otop and Piotr Witkowski},
 year         = {2012},
 title        = {Satisfiability vs. Finite Satisfiability in Elementary Modal Logics},
 editor       = {Marco Faella and Aniello Murano},
 booktitle    = {Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2012, Napoli, Italy, September 6-8, 2012.},
 series       = {{EPTCS}},
 volume       = {96},
 pages        = {141--154},
 doi          = {10.4204/EPTCS.96.11},
)
@article(Mor75,
 author       = {M. Mortimer},
 year         = {1975},
 title        = {On languages with two variables},
 journal      = {Zeitschrift f{\"{u}}r Mathematische Logik und Grundlagen der Mathematik},
 volume       = {21},
 pages        = {135--140},
 doi          = {10.1002/malq.19750210118},
)
@article(Otto01,
 author       = {Martin Otto},
 year         = {2001},
 title        = {Two Variable First-Order Logic over Ordered Domains},
 journal      = {J. Symb. Log.},
 volume       = {66},
 number       = {2},
 pages        = {685--702},
 doi          = {10.2307/2695037},
)
@article(Otto04,
 author       = {Martin Otto},
 year         = {2004},
 title        = {Modal and guarded characterisation theorems over finite transition systems},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {130},
 number       = {1-3},
 pages        = {173--205},
 doi          = {10.1016/j.apal.2004.04.003},
)
@inproceedings(PST97,
 author       = {Leszek Pacholski and Wieslaw Szwast and Lidia Tendera},
 year         = {1997},
 title        = {Complexity of Two-Variable Logic with Counting},
 booktitle    = {Proceedings, 12th Annual {IEEE} Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997},
 pages        = {318--327},
 doi          = {10.1109/LICS.1997.614958},
)
@article(PH05,
 author       = {Pratt{-}Hartmann, Ian},
 year         = {2005},
 title        = {Complexity of the Two-Variable Fragment with Counting Quantifiers},
 journal      = {Journal of Logic, Language and Information},
 volume       = {14},
 number       = {3},
 pages        = {369--395},
 doi          = {10.1007/s10849-005-5791-1},
)
@article(PH07,
 author       = {Pratt{-}Hartmann, Ian},
 year         = {2007},
 title        = {Complexity of the Guarded Two-variable Fragment with Counting Quantifiers},
 journal      = {J. Log. Comput.},
 volume       = {17},
 number       = {1},
 pages        = {133--155},
 doi          = {10.1093/logcom/exl034},
)
@inproceedings(P-HST16,
 author       = {Pratt{-}Hartmann, Ian and Wieslaw Szwast and Lidia Tendera},
 year         = {2016},
 title        = {Quine's Fluted Fragment is Non-Elementary},
 booktitle    = {25th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2016, August 29 - September 1, 2016, Marseille, France},
 pages        = {39:1--39:21},
 doi          = {10.4230/LIPIcs.CSL.2016.39},
)
@article(Pur96,
 author       = {William C. Purdy},
 year         = {1996},
 title        = {Fluted Formulas and the Limits of Decidability},
 journal      = {J. Symb. Log.},
 volume       = {61},
 number       = {2},
 pages        = {608--620},
 doi          = {10.2307/2275678},
)
@article(purdy:purdy99,
 author       = {William C. Purdy},
 year         = {1999},
 title        = {Quine's 'Limits of Decision'},
 journal      = {J. Symb. Log.},
 volume       = {64},
 number       = {4},
 pages        = {1439--1466},
 doi          = {10.2307/2586789},
)
@article(purdy:purdy02,
 author       = {William C. Purdy},
 year         = {2002},
 title        = {Complexity and Nicety of Fluted Logic},
 journal      = {Studia Logica},
 volume       = {71},
 number       = {2},
 pages        = {177--198},
 doi          = {10.1023/A:1016596721799},
)
@inproceedings(purdy:quine69,
 author       = {W. V. Quine},
 year         = {1969},
 title        = {On the limits of decision},
 booktitle    = {Proceedings of the 14th International Congress of Philosophy},
 volume       = {III},
 publisher    = {University of Vienna},
 pages        = {57--62},
)
@incollection(purdy:quine76b,
 author       = {W. V. Quine},
 year         = {1976},
 title        = {The variable},
 booktitle    = {The Ways of Paradox},
 edition      = {revised and enlarged},
 publisher    = {Harvard University Press},
 pages        = {272--282},
)
@article(Rab69,
 author       = {Michael O. Rabin},
 year         = {1969},
 title        = {Decidability of Second-Order Theories and Automata on Infinite Trees},
 journal      = {Transactions of the American Mathematical Society},
 volume       = {141},
 pages        = {pp. 1--35},
 doi          = {10.1090/S0002-9947-1969-0246760-1},
)
@inproceedings(Rosati08,
 author       = {Riccardo Rosati},
 year         = {2008},
 title        = {Finite Model Reasoning in {DL}-Lite},
 editor       = {Sean Bechhofer and Manfred Hauswirth and J{\"{o}}rg Hoffmann and Manolis Koubarakis},
 booktitle    = {The Semantic Web: Research and Applications, 5th European Semantic Web Conference, {ESWC} 2008, Tenerife, Canary Islands, Spain, June 1-5, 2008, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5021},
 publisher    = {Springer},
 pages        = {215--229},
 doi          = {10.1007/978-3-540-68234-9_18},
)
@inproceedings(Rudolph16,
 author       = {Sebastian Rudolph},
 year         = {2016},
 title        = {The Curse of Finiteness: Undecidability of Database-Inspired Reasoning Problems in Very Expressive Description Logics},
 editor       = {Maurizio Lenzerini and Pe{\~{n}}aloza, Rafael},
 booktitle    = {Proceedings of the 29th International Workshop on Description Logics, Cape Town, South Africa, April 22-25, 2016.},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {1577},
 publisher    = {CEUR-WS.org},
 url          = {http://ceur-ws.org/Vol-1577},
)
@article(RudolphG10,
 author       = {Sebastian Rudolph and Birte Glimm},
 year         = {2010},
 title        = {Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!},
 journal      = {J. Artif. Intell. Res. {(JAIR)}},
 volume       = {39},
 pages        = {429--481},
 doi          = {10.1613/jair.3029},
)
@article(SZ12,
 author       = {Thomas Schwentick and Thomas Zeume},
 year         = {2012},
 title        = {Two-Variable Logic with Two Order Relations},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 number       = {1},
 doi          = {10.2168/LMCS-8(1:15)2012},
)
@article(StC13,
 author       = {Luc Segoufin and Balder ten Cate},
 year         = {2013},
 title        = {Unary negation},
 journal      = {Logical Methods in Computer Science},
 volume       = {9},
 number       = {3},
 doi          = {10.2168/LMCS-9(3:25)2013},
)
@inproceedings(ST01,
 author       = {Wies{\l}aw Szwast and Lidia Tendera},
 year         = {2001},
 title        = {On the Decision Problem for the Guarded Fragment with Transitivity},
 booktitle    = {16th Annual {IEEE} Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings},
 pages        = {147--156},
 doi          = {10.1109/LICS.2001.932491},
)
@inproceedings(ST13,
 author       = {Wies{\l}aw Szwast and Lidia Tendera},
 year         = {2013},
 title        = {\unhbox\voidb@x \hbox{FO}{2} with one transitive relation is decidable},
 booktitle    = {30th International Symposium on Theoretical Aspects of Computer Science, {STACS} 2013, February 27 - March 2, 2013, Kiel, Germany},
 pages        = {317--328},
 doi          = {10.4230/LIPIcs.STACS.2013.317},
)
@article(Tra50,
 author       = {Boris A. Trakhtenbrot},
 year         = {1950},
 title        = {Impossibility of an algorithm for the decision problem in finite classes},
 journal      = {Doklady Akademii Nauk SSSR},
 volume       = {70},
 pages        = {569–572},
 note         = {English translation in \cite{Tra63}},
)
@article(Tra63,
 author       = {Boris A. Trakhtenbrot},
 year         = {1950},
 title        = {Impossibility of an algorithm for the decision problem in finite classes},
 journal      = {American Mathematical Society Translations},
 volume       = {23},
 pages        = {1--6},
 doi          = {10.1090/trans2/023/01},
)
@article(Tra53,
 author       = {Boris A. Trakhtenbrot},
 year         = {1953},
 title        = {On recursive separability},
 journal      = {Doklady Akademii Nauk SSSR},
 volume       = {88(6)},
 pages        = {953--956},
)
@article(Tur37,
 author       = {A. M. Turing},
 year         = {1937},
 title        = {On computable numbers, with an application to the \unhbox\voidb@x \hbox{Entscheidungsproblem}},
 journal      = {Proc. London Math. Soc.},
 volume       = {42},
 pages        = {230--265},
 doi          = {10.1112/plms/s2-42.1.230},
 note         = {Correction in vol. 43, pp. 544-546},
)
@inproceedings(Var97,
 author       = {Moshe Y. Vardi},
 year         = {1996},
 title        = {Why is Modal Logic So Robustly Decidable?},
 booktitle    = {Descriptive Complexity and Finite Models, Proceedings of a {DIMACS} Workshop 1996, Princeton, New Jersey, USA, January 14-17, 1996},
 pages        = {149--184},
 url          = {http://dimacs.rutgers.edu/Volumes/Vol31.html},
)