by Tishkovsky, D., Schmidt, R. A. and Khodadadi, M.
Abstract:
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.
Reference:
MetTeL: A Tableau Prover with Logic-Independent Inference Engine (Tishkovsky, D., Schmidt, R. A. and Khodadadi, M.), In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011) (Brünnler, K., Metcalfe, G., eds.), Springer, volume 6793, 2011.
Bibtex Entry:
@INPROCEEDINGS{TishkovskySchmidtKhodadadi11,
AUTHOR = {Tishkovsky, D. and Schmidt, R. A. and Khodadadi, M.},
YEAR = {2011},
TITLE = {MetTeL: A Tableau Prover with Logic-Independent Inference Engine},
EDITOR = {Br\"unnler, K. and Metcalfe, G.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6793},
PAGES = {242--247},
PUBLISHER = {Springer},
URL = {http://www.springerlink.com/content/m33u1262575w046n/fulltext.pdf},
ABSTRACT = {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.
},
}