2016
[22] A Bi-Intuitionistic Modal Logic: Foundations and Automation (J. G. Stell, R. A. Schmidt, D. Rydeheard), In Journal of Logical and Algebraic Methods in Programming, volume 85, 2016. [bib] [pdf] [doi]
2014
[21] Tableau Development for a Bi-Intuitionistic Tense Logic (J. G. Stell, R. A. Schmidt, D. Rydeheard), In Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen (ARW-DT 2014) (A. Bolotov, M. Kerber, eds.), 2014. [bib] [pdf]
[20] Tableau Development for a Bi-Intuitionistic Tense Logic (J. G. Stell, R. A. Schmidt, D. Rydeheard), In Relational and Algebraic Methods in Computer Science (RAMiCS 14) (P. Jipsen, W. Kahl, eds.), Springer, volume 8428, 2014. [bib] [pdf] [doi]
[19] Using Tableau to Decide Description Logics with Full Role Negation and Identity (R. A. Schmidt, D. Tishkovsky), In ACM Transactions on Computational Logic, volume 15, 2014. [bib] [pdf] [doi]
2013
[18] A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI - Extended version of Tableaux13 paper (R. A. Schmidt M. Khodadadi, D. Tishkovsky), Technical report, Department of Computer Science, The University of Manchester, 2013. [bib] [pdf]
[17] A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky), In Tableaux13, 2013. (To appear.) [bib]
[16] Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete (M. Zawidzki, R. A. Schmidt, D. Tishkovsky), In Information Processing Letters, volume 113, 2013. [bib] [pdf] [doi]
[15] Refinement in the Tableau Synthesis Framework (D. Tishkovsky, R. A. Schmidt), arXiv e-Print 1305.3131v1 [cs.LO], 2013. (arXiv e-Print 1305.3131v1 [cs.LO]) [bib] [pdf]
[14] A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI (Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky), In Description Logics, 2013. [bib] [pdf]
2012
[13] Labelled Tableaux for Temporal Logic with Cardinality Constraints (Clare Dixon, Boris Konev, Renate A. Schmidt, Dmitry Tishkovsky), In Proceedings of The 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'12), 2012. [bib] [pdf] [doi]
[12] Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics (\cS. Minic\ua, M. Khodadadi, D. Tishkovsky, R. A. Schmidt), Long version of the present paper, http://www.mettel-prover.org/papers/IEL-long.pdf, 2012. (Long version of the present paper, http://www.mettel-prover.org/papers/IEL-long.pdf) [bib]
[11] MetTeL2: Towards a prover generation platform (D. Tishkovsky, R. A. Schmidt, M. Khodadadi.), 2012. [bib] [pdf]
[10] Terminating tableau calculi for modal logic K with global counting operators (M. Khodadadi, R. A. Schmidt, D. Tishkovsky, M. Zawidzki), 2012. [bib] [pdf]
2011
[9] MetTeL: A Tableau Prover with Logic-Independent Inference Engine (D. Tishkovsky, R. A. Schmidt, M. Khodadadi), In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011) (K. Brünnler, G. Metcalfe, eds.), Springer, volume 6793, 2011. [bib] [pdf]
[8] Automated Synthesis of Tableau Calculi (R. A. Schmidt, D. Tishkovsky), In Logical Methods in Computer Science, volume 7, 2011. [bib] [pdf] [doi]
[7] Synthesising Terminating Tableau Calculi for Relational Logics: Invited paper (R. A. Schmidt), In Relational and Algebraic Methods in Computer Science (RAMiCS 12) (H. de Swart, ed.), Springer, volume 6663, 2011. [bib] [pdf] [doi]
[6] MetTeL: A Generic Tableau Prover. (D. Tishkovsky; R. A. Schmidt; M. Khodadadi.), In Proceedings of the 18th Workshop on Automated Reasoning (ARW2011) (A.;Kirwan R. Miller, ed.), Dept of Computing Science, University of Glasgow, 2011. [bib] [pdf]
2009
[5] Automated Synthesis of Tableau Calculi (R. A. Schmidt, D. Tishkovsky), In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009) (M. Giese, A. Waaler, eds.), Springer, volume 5607, 2009. [bib] [pdf] [doi]
2008
[4] A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments (R. A. Schmidt, D. Tishkovsky), In Automated Reasoning (IJCAR 2008) (A. Armando, P. Baumgartner, G. Dowek, eds.), Springer, volume 5195, 2008. [bib] [pdf] [doi]
2007
[3] Deciding ALBO with Tableau (R. A. Schmidt, D. Tishkovsky), In Proceedings of the 20th International Workshop on Description Logics (DL-2007) (D. Calvanese, E. Franconi, V. Haarslev, D. Lembo, B. Motik, S. Tessaris, A. Y. Turhan, eds.), Bozen-Bolzano University Press, 2007. [bib] [pdf]
[2] Using Tableau to Decide Expressive Description Logics with Role Negation (R. A. Schmidt, D. Tishkovsky), In The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11--15, 2007 (K. Aberer, K.-S. Choi, N. Fridman Noy, D. Allemang, K.-I. Lee, L. J. B. Nixon, J. Golbeck, P. Mika, D. Maynard, R. Mizoguchi, G. Schreiber, P. Cudré-Mauroux, eds.), Springer, volume 4825, 2007. [bib] [pdf] [doi]
2006
[1] Automated Reasoning About Metric and Topology (Ullrich Hustadt, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev), Chapter in Logics in Artificial Intelligence (Michael Fisher, Wiebe van der Hoek, Boris Konev, Alexei Lisitsa, eds.), Springer Berlin / Heidelberg, volume 4160, 2006. (10.1007/11853886_44) [bib] [pdf] [doi]
Powered by bibtexbrowser
MetTeL 1 Online user manual MetTeL 1 PDF user manual ESSLLI 2011 Lecture Notes on Automated Synthesis of Tableau Calculi