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 (, , and ), Chapter in Logics in Artificial Intelligence (Fisher, Michael, van der Hoek, Wiebe, Konev, Boris, Lisitsa, Alexei, eds.), Springer Berlin / Heidelberg, volume 4160, , 10.1007/11853886_44. [bibtex] [pdf] [doi]

Using Tableau to Decide Expressive Description Logics with Role Negation ( and ), 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, . [bibtex] [pdf] [doi]

Deciding ALBO with Tableau ( and ), 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, . [bibtex] [pdf]

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

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

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

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

Automated Synthesis of Tableau Calculi ( and ), In Logical Methods in Computer Science, volume 7, . [bibtex] [url] [doi]

MetTeL: A Tableau Prover with Logic-Independent Inference Engine (, and ), In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011) (Brünnler, K., Metcalfe, G., eds.), Springer, volume 6793, . [bibtex] [pdf]

Terminating tableau calculi for modal logic K with global counting operators (, , and ), . [bibtex] [pdf]

MetTeL2: Towards a prover generation platform (, and ), . [bibtex] [pdf]

Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics (, , and ), , Long version of the present paper, papers/IEL-long.pdf. [bibtex]

Labelled Tableaux for Temporal Logic with Cardinality Constraints (, , and ), In Proceedings of The 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'12), . [bibtex] [pdf] [doi]

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (, and ), In Description Logics, . [bibtex] [pdf]

Refinement in the Tableau Synthesis Framework ( and ), , arXiv e-Print 1305.3131v1 [cs.LO]. [bibtex] [url]

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

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (, and ), In Tableaux13, , To appear.. [bibtex]

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

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

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

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

A Bi-Intuitionistic Modal Logic: Foundations and Automation (, and ), In Journal of Logical and Algebraic Methods in Programming, volume 85, . [bibtex] [html] [doi]