MetTeL

MetTeL: A tableau prover with logic-independent inference engine. MetTeL is a generic tableau prover for various modal, intuitionistic, hybrid, description and metric logics. The core component of MetTeL is a logic-independent tableau inference engine. A novel feature is that users have the ability to flexibly specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism or unrestricted blocking.


References in zbMATH (referenced in 15 articles , 2 standard articles )

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

  1. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  2. Bel’tyukov, Anatoliĭ Petrovich; Abbasi, Mohsin Manshad: Logical analysis of emotions in text from natural language (2019)
  3. Zohar, Yoni; Tishkovsky, Dmitry; Schmidt, Renate A.; Zamansky, Anna: Automating automated reasoning. The case of two generic automated reasoning tools (2019)
  4. Sindoni, Giulia; Sano, Katsuhiko; Stell, John G.: Axiomatizing discrete spatial relations (2018)
  5. Steen, Alexander; Benzmüller, Christoph: The higher-order prover Leo-III (2018)
  6. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
  7. Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph: Theorem provers for every normal modal logic (2017)
  8. Stell, John G.; Schmidt, Renate A.; Rydeheard, David: A bi-intuitionistic modal logic: foundations and automation (2016)
  9. Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
  10. Schmidt, Renate A.; Waldmann, Uwe: Modal tableau systems with blocking and congruence closure (2015)
  11. Schmidt, Renate A.; Tishkovsky, Dmitry: Using tableau to decide description logics with full role negation and identity (2014)
  12. Stell, John G.; Schmidt, Renate A.; Rydeheard, David: Tableau development for a bi-intuitionistic tense logic (2014)
  13. Khodadadi, Mohammad; Schmidt, Renate A.; Tishkovsky, Dmitry: A refined tableau calculus with controlled blocking for the description logic (\mathcalSHOI) (2013)
  14. Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad: The tableau prover generator METTEL2 (2012) ioport
  15. Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad: \textscMetTeL: a tableau prover with logic-independent inference engine (2011)


Further publications can be found at: http://www.mettel-prover.org/papers.php