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 4 articles , 2 standard articles )
Showing results 1 to 4 of 4.
- Stell, John G.; Schmidt, Renate A.; Rydeheard, David: A bi-intuitionistic modal logic: foundations and automation (2016)
- 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