LoTREC: Logical tableaux research engineering companion In this paper we describe a generic tableaux system for building models or counter-models and testing satisfiability of formulas in modal and description logics. This system is called LoTREC2.0. It is characterized by a high-level language for tableau rules and strategies. It aims at covering all Kripke-semantic based logics. It is implemented in Java and characterized by a user-friendly graphical interface. It can be used as a learning system for possible worlds semantics and tableaux based proof methods.

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
  2. Fariñas del Cerro, Luis; Herzig, Andreas; Su, Ezgi Iraz: Capturing equilibrium models in modal logic (2014)
  3. Gasquet, Olivier; Herzig, Andreas; Said, Bilal; Schwarzentruber, François: Kripke’s worlds. An introduction to modal logics via tableaux (2014)
  4. Golińska-Pilarek, Joanna; Muñoz-Velasco, Emilio; Mora-Bonilla, Angel: Relational dual tableau decision procedure for modal logic K (2012)
  5. Aucher, Guillaume; Maubert, Bastien; Schwarzentruber, François: Tableau method and NEXPTIME-completeness of DEL-sequents (2011)
  6. Mora, A.; Muñoz-Velasco, E.; Golińska-Pilarek, J.: Implementing a relational theorem prover for modal logic K (2011)
  7. Schmidt, Renate A.; Tishkovsky, Dmitry: Automated synthesis of tableau calculi (2011)
  8. Schwarzentruber, François: LotrecScheme (2011)
  9. Baral, C.; Gelfond, G.; Pontelli, E.; Son, T.: Logic programming for finding models in the logics of knowledge and its applications: a case study (2010)
  10. Bresolin, Davide; Goranko, Valentin; Montanari, Angelo; Sala, Pietro: Tableaux for logics of subinterval structures over dense orderings (2010)
  11. van Valkenhoef, Gert; van der Vaart, Elske; Verbrugge, Rineke: OOPS: an $S5_n$ prover for educational settings (2010)
  12. Holen, Bjarne; Johnsen, Einar Broch; Waaler, Arild: Proof search for the first-order connection calculus in Maude (2009)
  13. Goré, Rajeev; Nguyen, Linh Anh: EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies (2007)
  14. Formisano, Andrea; Nicolosi-Asmundo, Marianna: An efficient relational deductive system for propositional non-classical logics (2006)
  15. Gasquet, Olivier; Herzig, Andreas; Sahade, Mohamad: Terminating modal tableaux with simple completeness proof (2006)
  16. Gasquet, Olivier; Herzig, Andreas; Longin, Dominique; Sahade, Mohamad: LoTREC: Logical tableaux research engineering companion (2005)
  17. Fariñas del Cerro, Luis; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique: Lotrec: The generic tableau prover for modal and description logics (2001)