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

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

1 2 next

  1. Alviano, Mario; Batsakis, Sotiris; Baryannis, George: Modal logic S5 satisfiability in answer set programming (2021)
  2. Muñoz-Velasco, Emilio; Pelegrín, Mercedes; Sala, Pietro; Sciavicco, Guido; Stan, Ionel Eduard: On coarser interval temporal logics (2019)
  3. Nalon, Cláudia; Pattinson, Dirk: A resolution-based calculus for preferential logics (2018)
  4. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
  5. Dyckhoff, Roy: Intuitionistic decision procedures since Gentzen (2016)
  6. Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
  7. Fariñas del Cerro, Luis; Herzig, Andreas; Su, Ezgi Iraz: Capturing equilibrium models in modal logic (2014)
  8. Gasquet, Olivier; Herzig, Andreas; Said, Bilal; Schwarzentruber, François: Kripke’s worlds. An introduction to modal logics via tableaux (2014)
  9. Bresolin, Davide; Della Monica, Dario; Montanari, Angelo; Sciavicco, Guido: A tableau system for right propositional neighborhood logic over finite linear orders: an implementation (2013)
  10. Broersen, Jan; Cranefield, Stephen; Elrakaiby, Yehia; Gabbay, Dov; Grossi, Davide; Lorini, Emiliano; Parent, Xavier; van der Torre, Leendert W. N.; Tummolini, Luca; Turrini, Paolo; Schwarzentruber, François: Normative reasoning and consequence (2013)
  11. Golińska-Pilarek, Joanna; Muñoz-Velasco, Emilio; Mora-Bonilla, Angel: Relational dual tableau decision procedure for modal logic K (2012)
  12. Aucher, Guillaume; Maubert, Bastien; Schwarzentruber, François: Tableau method and NEXPTIME-completeness of DEL-sequents (2011)
  13. Mora, A.; Muñoz-Velasco, E.; Golińska-Pilarek, J.: Implementing a relational theorem prover for modal logic K (2011)
  14. Schmidt, Renate A.; Tishkovsky, Dmitry: Automated synthesis of tableau calculi (2011)
  15. Schwarzentruber, François: LotrecScheme (2011)
  16. Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad: \textscMetTeL: a tableau prover with logic-independent inference engine (2011)
  17. 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)
  18. Bresolin, Davide; Goranko, Valentin; Montanari, Angelo; Sala, Pietro: Tableaux for logics of subinterval structures over dense orderings (2010)
  19. van Valkenhoef, Gert; van der Vaart, Elske; Verbrugge, Rineke: OOPS: an (S5_n) prover for educational settings (2010) ioport
  20. Abate, Pietro; Goré, Rajeev: The Tableau Workbench (2009)

1 2 next