@incollection(Mor12,
 author       = {Ben-Ari, Mordechai},
 year         = {2012},
 title        = {Propositional Logic: Formulas, Models, Tableaux},
 booktitle    = {Mathematical Logic for Computer Science},
 publisher    = {Springer London},
 pages        = {7--47},
 doi          = {10.1007/978-1-4471-4129-7_2},
)
@article(BMP83,
 author       = {Ben{-}Ari, Mordechai and Amir Pnueli and Zohar Manna},
 year         = {1983},
 title        = {The Temporal Logic of Branching Time},
 journal      = {Acta Inf.},
 volume       = {20},
 pages        = {207--226},
 doi          = {10.1007/BF01257083},
)
@inproceedings(DBLP:conf/ijcai/BertelloGMR16,
 author       = {Matteo Bertello and Nicola Gigante and Angelo Montanari and Mark Reynolds},
 year         = {2016},
 title        = {Leviathan: {A} New {LTL} Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau},
 editor       = {Subbarao Kambhampati},
 booktitle    = {Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, {IJCAI} 2016, New York, NY, USA, 9-15 July 2016},
 publisher    = {{IJCAI/AAAI} Press},
 pages        = {950--956},
 url          = {http://www.ijcai.org/Abstract/16/139},
)
@article(Beth55,
 author       = {E. Beth},
 year         = {1955},
 title        = {Semantic Entailment and Formal Derivability},
 journal      = {Mededelingen der Koninklijke Nederlandse Akad. van Wetensch},
 volume       = {18},
)
@inproceedings(BEM96,
 author       = {Julian C. Bradfield and Javier Esparza and Angelika Mader},
 year         = {1996},
 title        = {An Effective Tableau System for the Linear Time {$\mathrm{\mu}$}-Calculus},
 editor       = {Friedhelm Meyer auf der Heide and Burkhard Monien},
 booktitle    = {Automata, Languages and Programming, 23rd International Colloquium, ICALP96, Paderborn, Germany, 8-12 July 1996, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1099},
 publisher    = {Springer},
 pages        = {98--109},
 doi          = {10.1007/3-540-61440-0_120},
)
@article(BrL08,
 author       = {Kai Br{\"{u}}nnler and Martin Lange},
 year         = {2008},
 title        = {Cut-free sequent systems for temporal logic},
 journal      = {J. Log. Algebr. Program.},
 volume       = {76},
 number       = {2},
 pages        = {216--225},
 doi          = {10.1016/j.jlap.2008.02.004},
)
@inproceedings(Cimatti2002,
 author       = {Alessandro Cimatti and Edmund M. Clarke and Enrico Giunchiglia and Fausto Giunchiglia and Marco Pistore and Marco Roveri and Roberto Sebastiani and Armando Tacchella},
 year         = {2002},
 title        = {NuSMV 2: An OpenSource Tool for Symbolic Model Checking},
 editor       = {Ed Brinksma and Kim Guldstrand Larsen},
 booktitle    = {Computer Aided Verification, 14th International Conference, {CAV} 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2404},
 publisher    = {Springer},
 pages        = {359--364},
 doi          = {10.1007/3-540-45657-0_29},
)
@article(CGH97,
 author       = {Edmund M. Clarke and Orna Grumberg and Kiyoharu Hamaguchi},
 year         = {1997},
 title        = {Another Look at {LTL} Model Checking},
 journal      = {Formal Methods in System Design},
 volume       = {10},
 number       = {1},
 pages        = {47--71},
 doi          = {10.1023/A:1008615614281},
)
@book(Fos95,
 author       = {Ian T. Foster},
 year         = {1995},
 title        = {Designing and building parallel programs - concepts and tools for parallel software engineering},
 publisher    = {Addison-Wesley},
)
@article(DBLP:journals/entcs/GaintzarainHLN08,
 author       = {Joxe Gaintzarain and Montserrat Hermo and Paqui Lucio and Marisa Navarro},
 year         = {2008},
 title        = {Systematic Semantic Tableaux for {PLTL}},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {206},
 pages        = {59--73},
 doi          = {10.1016/j.entcs.2008.03.075},
)
@book(Girle00,
 author       = {Rod Girle},
 year         = {2000},
 title        = {Modal Logics and Philosophy},
 publisher    = {Acumen, Teddington, UK},
)
@article(Goranko2010113,
 author       = {Valentin Goranko and Angelo Kyrilov and Dmitry Shkatov},
 year         = {2010},
 title        = {Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {262},
 number       = {0},
 pages        = {113 -- 125},
 doi          = {10.1016/j.entcs.2010.04.009},
 note         = {Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)},
)
@techreport(Gou89,
 author       = {G. Gough},
 year         = {1989},
 title        = {Decision procedures for temporal logics},
 type         = {Technical Report},
 number       = {UMCS-89-10-1},
 institution  = {Department of Computer Science, University of Manchester},
)
@inproceedings(HSZ96,
 author       = {Alain Heuerding and Michael Seyfried and Heinrich Zimmermann},
 year         = {1996},
 title        = {Efficient Loop-Check for Backward Proof Search in Some Non-classical Propositional Logics},
 editor       = {Pierangelo Miglioli and Ugo Moscato and Daniele Mundici and Mario Ornaghi},
 booktitle    = {TABLEAUX},
 series       = {Lecture Notes in Computer Science},
 volume       = {1071},
 publisher    = {Springer},
 pages        = {210--225},
 doi          = {10.1007/3-540-61208-4_14},
)
@inproceedings(How97,
 author       = {Jacob M. Howe},
 year         = {1997},
 title        = {Two Loop Detection Mechanisms: {A} Comparision},
 editor       = {Didier Galmiche},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, {TABLEAUX} '97, Pont-{\`{a}}-Mousson, France, May 13-16, 1997, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1227},
 publisher    = {Springer},
 pages        = {188--200},
 doi          = {10.1007/BFb0027414},
)
@incollection(hustadt2003trp++,
 author       = {Ullrich Hustadt and Boris Konev},
 year         = {2003},
 title        = {{TRP++2.0:} {A} Temporal Resolution Prover},
 editor       = {Franz Baader},
 booktitle    = {Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2741},
 publisher    = {Springer},
 pages        = {274--278},
 doi          = {10.1007/978-3-540-45085-6_21},
)
@inproceedings(DBLP:conf/cav/KestenMMP93,
 author       = {Yonit Kesten and Zohar Manna and Hugh McGuire and Amir Pnueli},
 year         = {1993},
 title        = {A Decision Algorithm for Full Propositional Temporal Logic},
 editor       = {Costas Courcoubetis},
 booktitle    = {CAV},
 series       = {Lecture Notes in Computer Science},
 volume       = {697},
 publisher    = {Springer},
 pages        = {97--109},
 doi          = {10.1007/3-540-56922-7_9},
)
@inproceedings(LiY2014,
 author       = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He},
 year         = {2014},
 title        = {Aalta: an {LTL} satisfiability checker over Infinite/Finite traces},
 editor       = {Shing{-}Chi Cheung and Alessandro Orso and Margaret{-}Anne D. Storey},
 booktitle    = {Proceedings of the 22nd {ACM} {SIGSOFT} International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014},
 publisher    = {{ACM}},
 pages        = {731--734},
 doi          = {10.1145/2635868.2661669},
)
@article(DBLP:journals/aicom/LudwigH10,
 author       = {Michel Ludwig and Ullrich Hustadt},
 year         = {2010},
 title        = {Implementing a fair monodic temporal logic prover},
 journal      = {AI Commun.},
 volume       = {23},
 number       = {2-3},
 pages        = {69--96},
 doi          = {10.3233/AIC-2010-0457},
)
@article(DBLP:journals/corr/Reynolds16,
 author       = {Mark Reynolds},
 year         = {2016},
 title        = {A traditional tree-style tableau for {LTL}},
 journal      = {CoRR},
 volume       = {abs/1604.03962},
 url          = {https://arxiv.org/abs/1604.03962},
)
@inproceedings(DBLP:conf/spin/RozierV07,
 author       = {Kristin Y. Rozier and Moshe Y. Vardi},
 year         = {2007},
 title        = {LTL Satisfiability Checking},
 editor       = {Dragan Bosnacki and Stefan Edelkamp},
 booktitle    = {SPIN},
 series       = {Lecture Notes in Computer Science},
 volume       = {4595},
 publisher    = {Springer},
 pages        = {149--167},
 doi          = {10.1007/978-3-540-73370-6_11},
)
@inproceedings(RV11,
 author       = {Kristin Y. Rozier and Moshe Y. Vardi},
 year         = {2011},
 title        = {A Multi-encoding Approach for {LTL} Symbolic Satisfiability Checking},
 editor       = {Michael J. Butler and Wolfram Schulte},
 booktitle    = {{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6664},
 publisher    = {Springer},
 pages        = {417--431},
 doi          = {10.1007/978-3-642-21437-0_31},
)
@inproceedings(VSchuppanLDarmawan-ATVA-2011,
 author       = {Viktor Schuppan and Luthfi Darmawan},
 year         = {2011},
 title        = {Evaluating {LTL} Satisfiability Solvers},
 editor       = {Tevfik Bultan and Pao-Ann Hsiung},
 booktitle    = {ATVA'11},
 series       = {Lecture Notes in Computer Science},
 volume       = {6996},
 publisher    = {Springer},
 pages        = {397--413},
 doi          = {10.1007/978-3-642-24372-1_28},
)
@phdthesis(Sch98,
 author       = {Stefan Schwendimann},
 year         = {1998},
 title        = {Aspects of Computational Logic},
 type         = {{PhD}},
 address      = {Institut f{\"u}r Informatik und angewandte Mathematik},
 url          = {http://www.iam.unibe.ch/ltgpub/1998/sch98b.ps},
)
@incollection(Schwe98,
 author       = {Stefan Schwendimann},
 year         = {1998},
 title        = {A New One-Pass Tableau Calculus for {PLTL}},
 editor       = {Harrie C. M. de Swart},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, {TABLEAUX} '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1397},
 publisher    = {Springer},
 pages        = {277--292},
 doi          = {10.1007/3-540-69778-0_28},
)
@book(Smu68,
 author       = {R. Smullyan},
 year         = {1968},
 title        = {First-order Logic},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-86718-7},
)
@inproceedings(SuW2012,
 author       = {Martin Suda and Christoph Weidenbach},
 year         = {2012},
 title        = {A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance},
 editor       = {Bernhard Gramlich and Dale Miller and Uli Sattler},
 booktitle    = {Automated Reasoning - 6th International Joint Conference, {IJCAR} 2012, Manchester, UK, June 26-29, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7364},
 publisher    = {Springer},
 pages        = {537--543},
 doi          = {10.1007/978-3-642-31365-3_42},
)
@article(VaW94,
 author       = {Moshe Y. Vardi and Pierre Wolper},
 year         = {1994},
 title        = {Reasoning About Infinite Computations},
 journal      = {Inf. Comput.},
 volume       = {115},
 number       = {1},
 pages        = {1--37},
 doi          = {10.1006/inco.1994.1092},
)
@phdthesis(Wid10,
 author       = {Florian Rainer Widmann},
 year         = {2010},
 title        = {Tableaux-based decision procedures for fixed point logics},
 type         = {Thesis},
 url          = {http://users.cecs.anu.edu.au/~rpg/software.htm},
 note         = {Thesis (Ph.D.) -- ANU, 2010},
)
@article(Wol85,
 author       = {P. Wolper},
 year         = {1985},
 title        = {The tableau method for temporal logic: an overview},
 journal      = {Logique et Analyse},
 volume       = {28},
 pages        = {110--111},
)