LoTREC

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

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

1 2 next

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

1 2 next