References

  1. 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.
  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.
  3. 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.
  4. E. Beth (1955): Semantic Entailment and Formal Derivability. Mededelingen der Koninklijke Nederlandse Akad. van Wetensch 18.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. Ian T. Foster (1995): Designing and building parallel programs - concepts and tools for parallel software engineering. Addison-Wesley.
  10. 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.
  11. Rod Girle (2000): Modal Logics and Philosophy. Acumen, Teddington, UK.
  12. 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).
  13. G. Gough (1989): Decision procedures for temporal logics. Technical Report UMCS-89-10-1. Department of Computer Science, University of Manchester.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. Mark Reynolds (2016): A traditional tree-style tableau for LTL. CoRR abs/1604.03962. Available at https://arxiv.org/abs/1604.03962.
  21. 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.
  22. 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.
  23. 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.
  24. Stefan Schwendimann (1998): Aspects of Computational Logic. PhD, Institut für Informatik und angewandte Mathematik. Available at http://www.iam.unibe.ch/ltgpub/1998/sch98b.ps.
  25. 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.
  26. R. Smullyan (1968): First-order Logic. Springer, doi:10.1007/978-3-642-86718-7.
  27. 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.
  28. Moshe Y. Vardi & Pierre Wolper (1994): Reasoning About Infinite Computations. Inf. Comput. 115(1), pp. 1–37, doi:10.1006/inco.1994.1092.
  29. 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.
  30. P. Wolper (1985): The tableau method for temporal logic: an overview. Logique et Analyse 28, pp. 110–111.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org