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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 2 standard articles )
Showing results 1 to 8 of 8.
- Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
- Stell, John G.; Schmidt, Renate A.; Rydeheard, David: A bi-intuitionistic modal logic: foundations and automation (2016)
- Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
- Schmidt, Renate A.; Waldmann, Uwe: Modal tableau systems with blocking and congruence closure (2015)
- Schmidt, Renate A.; Tishkovsky, Dmitry: Using tableau to decide description logics with full role negation and identity (2014)
- Stell, John G.; Schmidt, Renate A.; Rydeheard, David: Tableau development for a bi-intuitionistic tense logic (2014)
- Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad: The tableau prover generator METTEL2 (2012) ioport
- Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad: MetTeL: a tableau prover with logic-independent inference engine (2011)
Further publications can be found at: http://www.mettel-prover.org/papers.php