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

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

1 2 next

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

1 2 next