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