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 21 articles )

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

1 2 next

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

1 2 next