MetTeL: A Tableau Prover with Logic-Independent Inference Engine

Tishkovsky, D., Schmidt, R. A. and Khodadadi, M. (2011)

In Brunnler, K. and Metcalfe, G. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011). Lecture Notes in Artificial Intelligence, Vol. 6793, Springer, 242-247. BiBTeX, DOI Link.

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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 06 Jul 12
Copyright © 2011 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk