MetTeL tableau prover generation platform | MetTeL2 : Towards a Prover Generation Platform


MetTeL 1 Online user manual	MetTeL 1 PDF user manual	ESSLLI 2011 Lecture Notes on Automated Synthesis of Tableau Calculi

Automated Reasoning About Metric and Topology (Hustadt, Ullrich, Tishkovsky, Dmitry, Wolter, Frank and Zakharyaschev, Michael), Chapter in Logics in Artificial Intelligence (Fisher, Michael, van der Hoek, Wiebe, Konev, Boris, Lisitsa, Alexei, eds.), Springer Berlin / Heidelberg, volume 4160, 2006, 10.1007/11853886_44. [bibtex] [pdf] [doi]

Using Tableau to Decide Expressive Description Logics with Role Negation (Schmidt, R. A. and Tishkovsky, D.), In The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11–15, 2007 (Aberer, K., Choi, K.-S., Fridman Noy, N., Allemang, D., Lee, K.-I., Nixon, L. J. B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P., eds.), Springer, volume 4825, 2007. [bibtex] [pdf] [doi]

Deciding ALBO with Tableau (Schmidt, R. A. and Tishkovsky, D.), In Proceedings of the 20th International Workshop on Description Logics (DL-2007) (Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., Turhan, A. Y., eds.), Bozen-Bolzano University Press, 2007. [bibtex] [pdf]

A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments (Schmidt, R. A. and Tishkovsky, D.), In Automated Reasoning (IJCAR 2008) (Armando, A., Baumgartner, P., Dowek, G., eds.), Springer, volume 5195, 2008. [bibtex] [pdf] [doi]

Automated Synthesis of Tableau Calculi (Schmidt, R. A. and Tishkovsky, D.), In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009) (Giese, M., Waaler, A., eds.), Springer, volume 5607, 2009. [bibtex] [pdf] [doi]

MetTeL: A Generic Tableau Prover. (D. Tishkovsky; R. A. Schmidt; M. Khodadadi.), In Proceedings of the 18th Workshop on Automated Reasoning (ARW2011) (Miller,A.;Kirwan,R., ed.), Dept of Computing Science, University of Glasgow, 2011. [bibtex] [pdf]

Synthesising Terminating Tableau Calculi for Relational Logics: Invited paper (Schmidt, R. A.), In Relational and Algebraic Methods in Computer Science (RAMiCS 12) (de Swart, H., ed.), Springer, volume 6663, 2011. [bibtex] [pdf] [doi]

Automated Synthesis of Tableau Calculi (Schmidt, R. A. and Tishkovsky, D.), In Logical Methods in Computer Science, volume 7, 2011. [bibtex] [url] [doi]

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] [pdf]

Terminating tableau calculi for modal logic K with global counting operators (M. Khodadadi, R. A. Schmidt, D. Tishkovsky and M. Zawidzki), 2012. [bibtex] [pdf]

MetTeL2: Towards a prover generation platform (D. Tishkovsky, R. A. Schmidt and M. Khodadadi.), 2012. [bibtex] [pdf]

Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics (Minic\ua, Ş., Khodadadi, M., Tishkovsky, D. and Schmidt, R. A.), 2012, Long version of the present paper, papers/IEL-long.pdf. [bibtex]

Labelled Tableaux for Temporal Logic with Cardinality Constraints (Dixon, Clare, Konev, Boris, Schmidt, Renate A. and Tishkovsky, Dmitry), In Proceedings of The 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'12), 2012. [bibtex] [pdf] [doi]

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (Mohammad Khodadadi, Renate A. Schmidt and Dmitry Tishkovsky), In Description Logics, 2013. [bibtex] [pdf]

Refinement in the Tableau Synthesis Framework (Tishkovsky, D. and Schmidt, R. A.), 2013, arXiv e-Print 1305.3131v1 [cs.LO]. [bibtex] [url]

Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete (Zawidzki, M., Schmidt, R. A. and Tishkovsky, D.), In Information Processing Letters, volume 113, 2013. [bibtex] [html] [doi]

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (Mohammad Khodadadi, Renate A. Schmidt and Dmitry Tishkovsky), In Tableaux13, 2013, To appear.. [bibtex]

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI - Extended version of Tableaux13 paper (M. Khodadadi, R. A. Schmidt, and D. Tishkovsky), Technical report, Department of Computer Science, The University of Manchester, 2013. [bibtex] [pdf]

Using Tableau to Decide Description Logics with Full Role Negation and Identity (Schmidt, R. A. and Tishkovsky, D.), In ACM Transactions on Computational Logic, volume 15, 2014. [bibtex] [html] [doi]

Tableau Development for a Bi-Intuitionistic Tense Logic (Stell, J. G., Schmidt, R. A. and Rydeheard, D.), In Relational and Algebraic Methods in Computer Science (RAMiCS 14) (Jipsen, P., Kahl, W., eds.), Springer, volume 8428, 2014. [bibtex] [html] [doi]

Tableau Development for a Bi-Intuitionistic Tense Logic (Stell, J. G., Schmidt, R. A. and Rydeheard, D.), In Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen (ARW-DT 2014) (Bolotov, A., Kerber, M., eds.), 2014. [bibtex] [pdf]

A Bi-Intuitionistic Modal Logic: Foundations and Automation (Stell, J. G., Schmidt, R. A. and Rydeheard, D.), In Journal of Logical and Algebraic Methods in Programming, volume 85, 2016. [bibtex] [html] [doi]

Other tableau provers

Other useful tools