Publications

• Books
• Surveys
• Automated reasoning / decidability / proof theory
• Reasoning about images and graphs
• Abductive and inductive reasoning
• Ontology extraction, ontology processing
• Forgetting, uniform interpolation, second-order quantifier elimination
• Querying
• Automated automated reasoning
• Model building / minimal model reasoning
• Benchmarking
• First-order logic
• Modal logic, dynamic modal logics
• Description logic, knowledge representation, ontology reasoning
• Intuitionistic logic and other non-classical logics
• Temporal logic
• Second-order logic
• Algebraic logic
• Agents
• System descriptions
• Special journal issues
• Proceedings
• Miscellaneous

Books

Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications. Back-cover, BiBTeX, Publisher's info. Order at amazon.co.uk, Order at amazon.com, Order at amazon.de.

Surveys

• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, Vol. 7797, 345-391. Springer (2013). Invited overview paper.
  Abstract, BiBTeX, DOI.
• Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49 (2011).
  Abstract, BiBTeX, DOI Link.
• Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262 221-229 (2010). Invited paper.
  Abstract, BiBTeX, PDF, DOI Link.
• Computational Modal Logic. Together with I. Horrocks, U. Hustadt, and U. Sattler. In Blackburn, P. and van Benthem, J. and Wolter, F. (eds), Handbook of Modal Logic. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, Amsterdam, 181-245 (2007). Commissioned overview paper.
  Abstract, Link to Elsevier, BiBTeX.
• A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276 (2004). Invited overview paper.
  Abstract, BiBTeX, PostScript, PDF.
• Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67 (2003). Survey commissioned for the Kickoff Volume of COST Action 274.
  Abstract, BiBTeX, PDF.
• On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics. Together with L. Georgieva and U. Hustadt. In Horrocks, I. and Tessaris, S. (eds), Proceedings of the 2002 International Workshop on Description Logics (DL'2002). CEUR Workshop Proceedings, Vol. CEUR-WS/Vol-53, 25-36 (2002).
  Abstract, BiBTeX, PostScript.
• Resolution-Based Methods for Modal Logics. Together with H. de Nivelle and U. Hustadt. Logic Journal of the IGPL 8 (3) 265-292 (2000).
  Abstract, BiBTeX, PostScript, Errata.
  

Automated reasoning / decidability / proof theory

• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. Journal of Automated Reasoning 64 (2) 197-251 (2020).
  Abstract, BiBTeX, Open access content sharing link from publisher.
• Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Together with O. Beyersdorff, J., Blinkhorn, L., Chew and M. Suda. Journal of Automated Reasoning 63 (3) 597-623 (2018).
  Abstract, BiBTeX, Open access DOI link.
• Rule Refinement for Semantic Tableau Calculi. Together with D. Tishkovsky. In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017). Lecture Notes in Artificial Intelligence, Vol. 10501, Springer, 228-244 (2017).
  Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
• Role Forgetting for ALCOQH(top)-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Sierra, C. (ed), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017). AAAI Press/IJCAI, 1354-1361 (2017).
  Abstract, BiBTeX, PDF.
• A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519, 2016.
  Abstract, BiBTeX, DOI Link to Elsevier.
• Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Lenzerini, M. and Penaloza, R. (eds), Proceedings of the 29th International Workshop on Description Logics (DL-2016). CEUR Workshop Proceedings, Vol. 1577, CEUR-WS.org, 2016.
  Abstract, BiBTeX, PDF.
• Modal Tableau Systems with Blocking and Congruence Closure. Together with U. Waldmann. In De Nivelle, H. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015). Lecture Notes in Computer Science, Vol. 9323, Springer, 38-53 (2015).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Arenas et al (eds), The Semantic Web, 14th International Semantic Web Conference, ISWC 2015. Lecture Notes in Computer Science, Vol. 9366, Springer, 587-602 (2015).
  Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
• LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. Together with Y. Zhao. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Saturation-Based Forgetting in the Description Logic SIF. Together with P. Koopmann. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. Together with P. Koopmann. In Bonet, B. and Koenig, S. (eds), Proc. AAAI-2015. AAAI Press, 175-181 (2015).
  Abstract, BiBTeX, PDF.
• Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497, 2014.
  Abstract, BiBTeX, PDF (final version available in the proceedings).
• Forgetting and Uniform Interpolation of ALC-Ontologies with ABoxes. Together with P. Koopmann. In M. Bienvenu and R. Rosati (eds), Proceedings of the 27th International Workshop on Description Logics (DL-2014). CEUR Workshop Proceedings, Vol. 1193, CEUR-WS.org, 245-257 (2014).
  Abstract, BiBTeX, PDF.
• Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Together with F. Papacchini. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395 (2014).
  Abstract, BiBTeX.
• Count and Forget: Uniform Interpolation of SHQ-Ontologies. Together with P. Koopmann. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448 (2014).
  Abstract, BiBTeX.
• Tableau Development for a Bi-Intuitionistic Tense Logic. Together with J. G. Stell and D. Rydeheard. In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds), Relational and Algebraic Methods in Computer Science (RAMiCS 14). Lecture Notes in Computer Science, Vol. 8428, Springer, 412-428 (2014).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. ACM Transactions on Computational Logic 15 (1) (2014).
  Abstract, BiBTeX, DOI link to TOCL.
• Forgetting Concept and Role Symbols in ALCH-Ontologies. Together with P. Koopmann. In McMillan, K., Middeldorp, A. and Voronkov, A. (eds), Proc. LPAR 2013. Lecture Notes in Computer Science, Vol. 8312, Springer, 552-567 (2013).
  Abstract, BiBTeX, PDF (final version will be available from Springer).
• Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12 (2013).
  Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
• Computing Minimal Models Modulo Subset-Simulation for Propositional Modal Logics. Together with F. Papacchini. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 279-294 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Uniform Interpolation of ALC-Ontologies Using Fixpoints. Together with P. Koopmann. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. Together with M. Khodadadi and D. Tishkovsky. In Galmiche, D. and Larchey-Wendling, D. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013). Lecture Notes in Computer Science, Vol. 8123 Springer, 188-202 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, Vol. 7797, 345-391. Springer (2013). Invited overview paper.
  Abstract, BiBTeX, DOI.
• Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete. Together with M. Zawidzki and D. Tishkovsky, Information Processing Letters 113 (1-2) 34-38 (2013).
  Abstract, BiBTeX, DOI.
• Labelled Tableaux for Temporal Logic with Cardinality Constraints. Together with C. Dixon, B. Konev, and D. Tishkovsky. Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). IEEE Computer Society, 111-118 (2012).
  Abstract, BiBTeX, DOI, PDF.
• The Tableau Prover Generator MetTeL2. Together with D. Tishkovsky and M. Khodadadi. In del Cerro, L. F. and Herzig, A. and Mengin, J. (eds), Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA 2012). Lecture Notes in Computer Science Vol. 7519, Springer, 492-495 (2012).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. arXiv e-Print 1208.1476v1 [cs.LO] (2012).
  Abstract, BiBTeX, arXiv Link.
• The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74 (2012).
  Abstract, BiBTeX, DOI.
• A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172 (2011).
  Abstract, BiBTeX, DOI Link.
• MetTeL: A Tableau Prover with Logic-Independent Inference Engine. Together with D. Tishkovsky and M. Khodadadi. 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 (2011).
  Abstract, BiBTeX, DOI Link.
• Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49 (2011).
  Abstract, BiBTeX, DOI Link.
• A Comparison of Solvers for Propositional Dynamic Logic. Together with U. Hustadt. In Konev, B. and Schmidt, R. and Schulz, S. (eds), Proceedings of the Second International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), EasyChair Proceedings, 60-69 (2010).
  Abstract, BiBTeX, PDF.
• Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262 221-229 (2010). Invited paper.
  Abstract, BiBTeX, PDF, DOI Link.
• A Tableau Method for Checking Rule Admissibility in S4. Together with S. Babenyshev, V. Rybakov and D. Tishkovsky. Electronic Notes in Theoretical Computer Science 262 17-32 (2010).
  Abstract, BiBTeX, PDF, DOI Link.
• Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• A New Methodology for Developing Deduction Methods. In Annals of Mathematics and Artificial Intelligence 55 (1-2) 155-187 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• Improved Second-Order Quantifier Elimination in Modal Logic. In Hölldobler, S., Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Computer Science, Vol. 5293, Springer, 375-388 (2008).
  Abstract, BiBTeX, DOI Link.
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. Together with D. Tishkovsky. In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209 (2008).
  Abstract, BiBTeX, DOI Link.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information. 17 (1) 109-129 (2008).
  Abstract, BiBTeX, Full text via Springer.
• Using Tableau to Decide Expressive Description Logics with Role Negation. Together with D. Tishkovsky. In Aberer, K. et al (eds), The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, Vol. 4825, Springer, 438-451 (2007).
  Abstract, BiBTeX, DOI Link.
• System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520 (2007).
  Abstract, BiBTeX, DOI Link.
• Deciding ALBO with Tableau. Together with D. Tishkovsky. In Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., and Turhan, A. Y. (eds), Proceedings of the 20th International Workshop on Description Logics (DL-2007), Bozen-Bolzano University Press, 135-146 (2007).
  Abstract, BiBTeX, PDF.
• Developing Modal Tableaux and Resolution Methods via First-Order Resolution. In Governatori, G. and Hodkinson, I. and Venema, Y. (eds), Advances in Modal Logic, Volume 6. College Publications, London, 1-26 (2006). Invited paper.
  Abstract, BiBTeX, PostScript.
• Computational Modal Logic. Together with I. Horrocks, U. Hustadt, and U. Sattler. In Blackburn, P. and van Benthem, J. and Wolter, F. (eds), Handbook of Modal Logic. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, Amsterdam, ??-?? (2006). Commissioned overview paper.
  Abstract, Link to Elsevier, BiBTeX.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).
  Abstract, Full text via Springer, BiBTeX.
• The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55 (2007).
  Abstract, BiBTeX, PDF, Final version at Elsevier via DOI Link.
• Deciding Monodic Fragments by Temporal Resolution. Together with U. Hustadt and B. Konev. In Nieuwenhuis, R. (eds), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Vol. 3632, Springer, 204-218 (2005).
  Abstract, BiBTeX, PDF, Full text via Springer.
• A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276 (2004). Invited overview paper.
  Abstract, BiBTeX, PostScript, PDF.
• SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 149-162 (2004).
  Abstract, BiBTeX, PDF.
• Two Proof Systems for Peirce Algebras. Together with E. Orlowska and U. Hustadt. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 238-251 (2004).
  Abstract, BiBTeX, Springer Link.
• Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67 (2003). Survey commissioned for the Kickoff Volume of COST Action 274.
  Abstract, BiBTeX, PDF.
• Fourth International Workshop on the Implementation of Logics. Together with B. Konev (eds). Technical Report ULCS-03-018, University of Liverpool (2003).
  Abstract, BiBTeX, PDF.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192 (2003).
  Abstract, ScienceDirect, BiBTeX.
• A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. In Baader, F. (ed.), Automated Deduction-CADE-19. Lecture Notes in Artificial Intelligence Vol. 2741, Springer, 412-426 (2003).
  Abstract, BiBTeX, PostScript, SpringerLink.
• A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester (2002). Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
  Abstract, BiBTeX, PostScript.
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence Vol. 2250, Springer, 85-99 (2001).
  Abstract, BiBTeX.
• A Resolution-Based Decision Procedure for Extensions of K4. Together with H. Ganzinger, U. Hustadt and C. Meyer. In Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H. (eds), Advances in Modal Logic, Volume 2. Lecture Notes 119, CSLI Publications, Stanford, 225-246 (2001).
  Abstract, BiBTeX, PostScript.
• MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71 (2000).
  Abstract, BiBTeX, PostScript.
• Normal Forms and Proofs in Combined Modal and Temporal Logics . Together with U. Hustadt, C. Dixon, and M. Fisher. In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence Vol. 1794, Springer, 73-87 (2000).
  Abstract, BiBTeX, PostScript.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112 (2000).
  Abstract, BiBTeX, PostScript.
• A Resolution Decision Procedure for Fluted Logic. Together with U. Hustadt. In McAllester, D. (ed), Automated Deduction-CADE-17. Lecture Notes in Artificial Intelligence Vol. 1831, Springer, 433-448 (2000).
  Abstract, BiBTeX.
• Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. In Gent, I. P. and van Maaren, H. and Walsh, T. (eds), SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications 63, IOS Press, Amsterdam (2000). Also in a special issue of Journal of Automated Reasoning.
  Abstract, BiBTeX, PostScript, DOI Link.
• Maslov's Class K Revisited. Together with U. Hustadt. In H. Ganzinger (ed.), Automated Deduction: CADE-16, Lecture Notes in Artificial Intelligence, Vol. 1632, Springer (1999).
  Abstract, BiBTeX, PostScript.
• MSPASS: Subsumption Testing with SPASS. Together with U. Hustadt and C. Weidenbach. In Lambrix, P. et al. (eds.), Proc. of Intern. Workshop on Description Logics'99, Linköping University, 136-137 (1999).
  Abstract, BiBTeX, PostScript.
• On the Relation of Resolution and Tableaux Proof Systems for Description Logics. Together with U. Hustadt. In Dean, T. (ed), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99). Vol. 1, Morgan Kaufmann, 110-115 (1999).
  Abstract, BiBTeX, PDF.
• Simplification and Backjumping in Modal Tableau. Together with U. Hustadt. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 187-201 (1998).
  Abstract, BiBTeX, PostScript.
• Optimised Functional Translation and Resolution. Together with U. Hustadt and C. Weidenbach. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 36-37 (1998). (Contribution to the comparison section of modal theorem provers).
  Abstract, BiBTeX, PostScript.
• Resolution is a Decision Procedure for Many Propositional Modal Logics. In Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 1, Lecture Notes 87, CSLI Publications, Stanford, 189-208 (1998).
  Abstract, BiBTeX.
• E-Unification for Subsystems of S4. In Nipkow, T. (ed.), Rewriting Techniques and Applications: 9th International Conference, RTA'98, Tsukuba, Japan, Proceedings, Lecture Notes in Computer Science Vol. 1379, Springer, 106-120 (1998).
  Abstract, BiBTeX, PostScript.
• Ordered E-Resolution and Path Logics. Manuscript. Submitted for publication (1998).
  Abstract, BiBTeX.
• Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken, Germany (1997).
  Abstract, BiBTeX, PostScript (851KB).
• Decidability by resolution for many modal logics. Extended abstract of a talk presented at ESSLLI'97, Aix-en-Provence, France (1997).
  Dvi.
• Resolution is a Decision Procedure for Many Propositional Modal Logics. Research Rep. MPI-I-97-2-002, MPI für Informatik, Saarbrücken (1997).
  Abstract, BiBTeX, PostScript.

Reasoning about images and graphs

• A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519, 2016.
  Abstract, BiBTeX, DOI Link to Elsevier.

Abductive and inductive reasoning

• Signature-Based Abduction for Expressive Description Logics. Together with P. Koopmann, W. Del-Pinto, and S. Tourret. In Calvanese, D. and Erdem, E. (eds), Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning. AI Press (2020).
  Abstract, BiBTeX, PDF.
• Extending Forgetting-Based Abduction Using Nominals. Together with W. Del-Pinto. In A. Herzig and A. Popescu (eds), Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). Lecture Notes in Artificial Intelligence, Vol. 11715, Springer, 185-202 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• ABox Abduction via Forgetting in ALC. Together with W. Del-Pinto. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 2768-2775 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.

Ontology extraction, ontology processing

• Extracting Subontologies from SNOMED CT Together with W. Del-Pinto and Y. Gao. In Groth, P. et al. (eds), The Semantic Web: ESWC 2022 Satellite Events. Lecture Notes in Computer Science, Vol. 13384, Springer, 291-294 (2022).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• Upwardly Abstracted Definition-Based Subontologies. Together with G. Alghamdi, W. Del-Pinto, and Y. Gao. In A. L. Gentile, and R. Goncalves (eds), K-CAP'21: Knowledge Capture Conference. ACM, 209-216 (2021).
  Abstract, BiBTeX, DOI link to ACM.
• Tracking Semantic Evolutionary Changes in Large-Scale Ontological Knowledge Bases. Together with Z. Liu, C. Lu, G. Alghamdi and Y. Zhao. In G. Demartini, and G. Zuccon, and J. S. Culpepper, Z. Huang and H. Tong (eds), CIKM'21: The 30th ACM International Conference on Information and Knowledge Management. ACM, 1130-1139 (2021).
  Abstract, BiBTeX, DOI link to ACM.
• Ontology Extraction for Large Ontologies via Modularity and Forgetting. Together with J. Chen, G. Alghamdi, D. Walther and Y. Gao. In Kejriwal, M. and Szekely, P. A. and Troncy, R. (eds), Proceedings of the 10th International Conference on Knowledge Capture (K-CAP'19). ACM, 45-52 (2019).
  Abstract, BiBTeX, PDF, DOI link to ACM.
• Extending Forgetting-Based Abduction Using Nominals. Together with W. Del-Pinto. In A. Herzig and A. Popescu (eds), Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). Lecture Notes in Artificial Intelligence, Vol. 11715, Springer, 185-202 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• ABox Abduction via Forgetting in ALC. Together with W. Del-Pinto. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 2768-2775 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach. Together with Y. Zhao, G. Alghamdi, H. Feng, G. Stoilos, D. Juric and M. Khodadadi. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 3116-3124 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Methods and Metrics for Knowledge Base Engineering and Integration. Together with G. Stoilos, D. Geleta, S. Wartak, S. Hall, M. Khodadadi, Y. Zhao, and G. Alghamdi. In 9th Workshop on Ontology Design and Patterns (WOP 2018). CEUR Workshop Proceedings, Vol. 2195, CEUR-WS.org, 72-86 (2018).
  Abstract, BiBTeX, PDF.

Forgetting, uniform interpolation, second-order quantifier elimination

• Semantic Forgetting in Expressive Description Logics. Together with M. Sakr. In B. Konev and G. Reger (eds), Frontiers of Combining Systems (FroCoS 2021). Lecture Notes in Computer Science, Vol. 12941, Springer, 118-136 (2021).
  Abstract, BiBTeX, DOI link to Springer.
• A Practical Approach to Forgetting in Description Logics with Nominals. Together with Y. Zhao, Y. Wang, X. Zhang, H. Feng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3073-3079 (2020).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Ontology Extraction for Large Ontologies via Modularity and Forgetting. Together with J. Chen, G. Alghamdi, D. Walther and Y. Gao. In Kejriwal, M. and Szekely, P. A. and Troncy, R. (eds), Proceedings of the 10th International Conference on Knowledge Capture (K-CAP'19). ACM, 45-52 (2019).
  Abstract, BiBTeX, PDF, DOI link to ACM.
• FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. Togther with Y. Zhao. In P. Fontaine (ed), Automated Deduction: CADE-27. Lecture Notes in Artificial Intelligence, Vol. 11716. Springer, 568-579 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach. Together with Y. Zhao, G. Alghamdi, H. Feng, G. Stoilos, D. Juric and M. Khodadadi. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 3116-3124 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• ABox Abduction via Forgetting in ALC. Together with W. Del-Pinto. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 2768-2775 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• On Concept Forgetting in Description Logics with Qualified Number Restrictions. Together with Y. Zhao. In Lang, J. (ed), Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018). AAAI Press/IJCAI, 1984-1990 (2018).
  Abstract, BiBTeX, PDF, Details at publisher.
• FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. Together with Y. Zhao. In Galmiche, D. and Schulz, S. and Sebastiani, R. (eds), Automated Reasoning (IJCAR 2018). Lecture Notes in Artificial Intelligence, Volume 10900, Springer, 19-27 (2018).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• Role Forgetting for ALCOQH(top)-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Sierra, C. (ed), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017). AAAI Press/IJCAI, 1354-1361 (2017).
  Abstract, BiBTeX, PDF.
• Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Lenzerini, M. and Penaloza, R. (eds), Proceedings of the 29th International Workshop on Description Logics (DL-2016). CEUR Workshop Proceedings, Vol. 1577, CEUR-WS.org, 2016.
  Abstract, BiBTeX, PDF.
• Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Arenas et al (eds), The Semantic Web, 14th International Semantic Web Conference, ISWC 2015. Lecture Notes in Computer Science, Vol. 9366, Springer, 587-602 (2015).
  Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
• LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. Together with Y. Zhao. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Saturation-Based Forgetting in the Description Logic SIF. Together with P. Koopmann. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. Together with P. Koopmann. In Bonet, B. and Koenig, S. (eds), Proc. AAAI-2015. AAAI Press, 175-181 (2015).
  Abstract, BiBTeX, PDF.
• Forgetting and Uniform Interpolation of ALC-Ontologies with ABoxes. Together with P. Koopmann. In M. Bienvenu and R. Rosati (eds), Proceedings of the 27th International Workshop on Description Logics (DL-2014). CEUR Workshop Proceedings, Vol. 1193, CEUR-WS.org, 245-257 (2014).
  Abstract, BiBTeX, PDF.
• Count and Forget: Uniform Interpolation of SHQ-Ontologies. Together with P. Koopmann. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448 (2014).
  Abstract, BiBTeX.
• Forgetting Concept and Role Symbols in ALCH-Ontologies. Together with P. Koopmann. In McMillan, K., Middeldorp, A. and Voronkov, A. (eds), Proc. LPAR 2013. Lecture Notes in Computer Science, Vol. 8312, Springer, 552-567 (2013).
  Abstract, BiBTeX, PDF (final version will be available from Springer).
• Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12 (2013).
  Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
• Uniform Interpolation of ALC-Ontologies Using Fixpoints. Together with P. Koopmann. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74 (2012).
  Abstract, BiBTeX, DOI.
• Improved Second-Order Quantifier Elimination in Modal Logic. In Hölldobler, S., Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Computer Science, Vol. 5293, Springer, 375-388 (2008).
  Abstract, BiBTeX, DOI Link.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 149-162 (2004).
  Abstract, BiBTeX, PDF.

Querying

• Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution. Together with S. Zheng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3080-3087 (2020).
  Abstract, BiBTeX, PDF, DOI link to publisher.

Automated automated reasoning

• Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools. Together with Y. Zohar, D. Tishkovsky and A. Zamansky. In Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y. and Wolter, F. (eds), Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, Vol. 11560, Springer, 610-638 (2019).
  Abstract, BiBTeX, DOI link to Publisher.
• Rule Refinement for Semantic Tableau Calculi. Together with D. Tishkovsky. In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017). Lecture Notes in Artificial Intelligence, Vol. 10501, Springer, 228-244 (2017).
  Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
• Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497, 2014.
  Abstract, BiBTeX, PDF (final version available in the proceedings).
• Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49 (2011).
  Abstract, BiBTeX, DOI Link.
• Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262 221-229 (2010). Invited paper.
  Abstract, BiBTeX, PDF, DOI Link.
• Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324 (2009).
  Abstract, BiBTeX, PDF, DOI Link.

Model building / minimal model reasoning

• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. Journal of Automated Reasoning 64 (2) 197-251 (2020).
  Abstract, BiBTeX, Open access content sharing link from publisher.
• Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Together with F. Papacchini. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395 (2014).
  Abstract, BiBTeX.
• Computing Minimal Models Modulo Subset-Simulation for Propositional Modal Logics. Together with F. Papacchini. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 279-294 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, Vol. 7797, 345-391. Springer (2013). Invited overview paper.
  Abstract, BiBTeX, DOI.
• A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172 (2011).
  Abstract, BiBTeX, DOI Link.
• Deciding ALBO with Tableau. Together with D. Tishkovsky. In Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., and Turhan, A. Y. (eds), Proceedings of the 20th International Workshop on Description Logics (DL-2007), Bozen-Bolzano University Press, 135-146 (2007).
  Abstract, BiBTeX, PDF.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).
  Abstract, Full text via Springer, BiBTeX.
• The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55 (2007).
  Abstract, BiBTeX, PDF, Final version at Elsevier via DOI Link.
• Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67 (2003). Survey commissioned for the Kickoff Volume of COST Action 274.
  Abstract, BiBTeX, PDF.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192 (2003).
  Abstract, ScienceDirect, BiBTeX.
• A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester (2002). Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
  Abstract, BiBTeX, PostScript.
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence Vol. 2250, Springer, 85-99 (2001).
  Abstract, BiBTeX.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112 (2000).
  Abstract, BiBTeX, PostScript.
• Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. In Gent, I. P. and van Maaren, H. and Walsh, T. (eds), SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications 63, IOS Press, Amsterdam (2000). Also in a special issue of Journal of Automated Reasoning.
  Abstract, BiBTeX, PostScript.

Benchmarking

• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. Journal of Automated Reasoning 64 (2) 197-251 (2020).
  Abstract, BiBTeX, Open access content sharing link from publisher.
• A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519, 2016.
  Abstract, BiBTeX, DOI Link to Elsevier.
• Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497, 2014.
  Abstract, BiBTeX, PDF (final version available in the proceedings).
• Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12 (2013).
  Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
• A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172 (2011).
  Abstract, BiBTeX, DOI Link.
• A Comparison of Solvers for Propositional Dynamic Logic. Together with U. Hustadt. In Konev, B. and Schmidt, R. and Schulz, S. (eds), Proceedings of the Second International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), EasyChair Proceedings, 60-69 (2010).
  Abstract, BiBTeX, PDF.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).
  Abstract, Full text via Springer, BiBTeX.
• Scientific Benchmarking with Temporal Logic Decision Procedures. Together with U. Hustadt. In Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A. (eds), Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR'2002). Morgan Kaufmann, 533-544 (2002).
  Abstract, BiBTeX, PDF.
• MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71 (2000).
  Abstract, BiBTeX, PostScript.
• An Empirical Analysis of Modal Theorem Provers. Together with U. Hustadt. Journal of Applied Non-Classical Logics 9(4) 479-522 (1999).
  Abstract, BiBTeX, PostScript.
• Simplification and Backjumping in Modal Tableau. Together with U. Hustadt. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 187-201 (1998).
  Abstract, BiBTeX, PostScript.
• On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. In Pollack, M. (ed), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), Vol. 1, Morgan Kaufmann, 202-207 (1997).
  Abstract, BiBTeX.
• On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. Research Rep. MPI-I-97-2-003, MPI für Informatik, Saarbrücken (1997).
  Abstract, BiBTeX, PostScript.

First-order logic

• Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution. Together with S. Zheng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3080-3087 (2020).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. Journal of Automated Reasoning 64 (2) 197-251 (2020).
  Abstract, BiBTeX, Open access content sharing link from publisher.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, Vol. 7797, 345-391. Springer (2013). Invited overview paper.
  Abstract, BiBTeX, DOI.
• Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262 221-229 (2010). Invited paper.
  Abstract, BiBTeX, PDF, DOI Link.
• Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• A New Methodology for Developing Deduction Methods. In Annals of Mathematics and Artificial Intelligence 55 (1-2) 155-187 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520 (2007).
  Abstract, BiBTeX, DOI Link.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).
  Abstract, Full text via Springer, BiBTeX.
• A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276 (2004). Invited overview paper.
  Abstract, BiBTeX, PostScript, PDF.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192 (2003).
  Abstract, ScienceDirect, BiBTeX.
• A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester (2002). Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
  Abstract, BiBTeX, PostScript.
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence Vol. 2250, Springer, 85-99 (2001).
  Abstract, BiBTeX.
• Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112 (2000).
  Abstract, BiBTeX, PostScript.
• A Resolution Decision Procedure for Fluted Logic. Together with U. Hustadt. In McAllester, D. (ed), Automated Deduction-CADE-17. Lecture Notes in Artificial Intelligence Vol. 1831, Springer, 433-448 (2000).
  Abstract, BiBTeX.
• Maslov's Class K Revisited. Together with U. Hustadt. In H. Ganzinger (ed.), Automated Deduction: CADE-16, Lecture Notes in Artificial Intelligence, Vol. 1632, Springer (1999).
  Abstract, BiBTeX, PostScript.

Modal logic, dynamic modal logics

See also Description logic, knowledge representation, ontology reasoning and Temporal logic

• A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519, 2016.
  Abstract, BiBTeX, DOI Link to Elsevier.
• Modal Tableau Systems with Blocking and Congruence Closure. Together with U. Waldmann. In De Nivelle, H. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015). Lecture Notes in Computer Science, Vol. 9323, Springer, 38-53 (2015).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497, 2014.
  Abstract, BiBTeX, PDF (final version available in the proceedings).
• Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Together with F. Papacchini. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395 (2014).
  Abstract, BiBTeX.
• Tableau Development for a Bi-Intuitionistic Tense Logic. Together with J. G. Stell and D. Rydeheard. In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds), Relational and Algebraic Methods in Computer Science (RAMiCS 14). Lecture Notes in Computer Science, Vol. 8428, Springer, 412-428 (2014).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Computing Minimal Models Modulo Subset-Simulation for Propositional Modal Logics. Together with F. Papacchini. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 279-294 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, Vol. 7797, 345-391. Springer (2013). Invited overview paper.
  Abstract, BiBTeX, DOI.
• Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete. Together with M. Zawidzki and D. Tishkovsky, Information Processing Letters 113 (1-2) 34-38 (2013).
  Abstract, BiBTeX, DOI.
• The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74 (2012).
  Abstract, BiBTeX, DOI.
• A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172 (2011).
  Abstract, BiBTeX, DOI Link.
• MetTeL: A Tableau Prover with Logic-Independent Inference Engine. Together with D. Tishkovsky and M. Khodadadi. 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 (2011).
  Abstract, BiBTeX, DOI Link.
• Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49 (2011).
  Abstract, BiBTeX, DOI Link.
• A Comparison of Solvers for Propositional Dynamic Logic. Together with U. Hustadt. In Konev, B. and Schmidt, R. and Schulz, S. (eds), Proceedings of the Second International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), EasyChair Proceedings, 60-69 (2010).
  Abstract, BiBTeX, PDF.
• Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262 221-229 (2010). Invited paper.
  Abstract, BiBTeX, PDF, DOI Link.
• A Tableau Method for Checking Rule Admissibility in S4. Together with S. Babenyshev, V. Rybakov and D. Tishkovsky. Electronic Notes in Theoretical Computer Science 262 17-32 (2010).
  Abstract, BiBTeX, PDF, DOI Link.
• Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• A New Methodology for Developing Deduction Methods. In Annals of Mathematics and Artificial Intelligence 55 (1-2) 155-187 (2009).
  Abstract, BiBTeX, PDF, DOI Link.
• Improved Second-Order Quantifier Elimination in Modal Logic. In Hölldobler, S., Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Computer Science, Vol. 5293, Springer, 375-388 (2008).
  Abstract, BiBTeX, DOI Link.
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. Together with D. Tishkovsky. In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209 (2008).
  Abstract, BiBTeX, DOI Link.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information. 17 (1) 109-129 (2008).
  Abstract, BiBTeX, Full text via Springer.
• System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520 (2007).
  Abstract, BiBTeX, DOI Link.
• Investigating Finite Models of Non-Classical Logics with Relation Algebra and RelView. Together with R. Berghammer. In de Swart, H. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Artficial intelligence Vol. 4342, Springer, 31-49 (2006).
  Abstract, BiBTeX, PDF.
• Developing Modal Tableaux and Resolution Methods via First-Order Resolution. In Governatori, G. and Hodkinson, I. and Venema, Y. (eds), Advances in Modal Logic, Volume 6. College Publications, London, 1-26 (2006). Invited paper.
  Abstract, BiBTeX, PostScript.
• Computational Modal Logic. Together with I. Horrocks, U. Hustadt, and U. Sattler. In Blackburn, P. and van Benthem, J. and Wolter, F. (eds), Handbook of Modal Logic. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, Amsterdam, 181-245 (2007). Commissioned overview paper.
  Abstract, Link to Elsevier, BiBTeX.
• The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55 (2007).
  Abstract, BiBTeX, PDF, Final version at Elsevier via DOI Link.
• Advances in Modal Logic, Volume 5. Together with I. Pratt-Hartmann, M. Reynolds, and H. Wansing (eds). King's College Publications, London (2005).
  Abstract, BiBTeX, Online version.
• AiML-2004: Advances in Modal Logic. Together with I. Pratt-Hartmann, M. Reynolds and H. Wansing (eds). Technical Report UMCS-04-09-01, University of Manchester, UK.
  Abstract, BiBTeX, PDF.
• SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 149-162 (2004).
  Abstract, BiBTeX, PDF.
• Two Proof Systems for Peirce Algebras. Together with E. Orlowska and U. Hustadt. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 238-251 (2004).
  Abstract, BiBTeX, Springer Link.
• Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67 (2003). Survey commissioned for the Kickoff Volume of COST Action 274.
  Abstract, BiBTeX, PDF.
• Combining Dynamic Logic with Doxastic Modal Logics. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 4. Chapter 18, King's College London Publications, 371-391 (2003).
  Abstract, BiBTeX.
• A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. In Baader, F. (ed.), Automated Deduction-CADE-19. Lecture Notes in Artificial Intelligence Vol. 2741, Springer, 412-426 (2003).
  Abstract, BiBTeX, PostScript, SpringerLink.
• On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics. Together with L. Georgieva and U. Hustadt. In Horrocks, I. and Tessaris, S. (eds), Proceedings of the 2002 International Workshop on Description Logics (DL'2002). CEUR Workshop Proceedings, Vol. CEUR-WS/Vol-53, 25-36 (2002).
  Abstract, BiBTeX, PostScript.
• On Axiomatic Products of PDL and S5: Substitution, Tests and Knowledge. Together with D. Tishkovsky. Bulletin of the Section of Logic 31 (1), 27-36 (2002).
  BiBTeX, PostScript.
• Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. Journal of Automated Reasoning 28 (2) 205-232 (2002).
  Abstract, BiBTeX, PostScript, DOI Link.
• A Resolution-Based Decision Procedure for Extensions of K4. Together with H. Ganzinger, U. Hustadt and C. Meyer. In Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H. (eds), Advances in Modal Logic, Volume 2. Lecture Notes 119, CSLI Publications, Stanford, 225-246 (2001).
  Abstract, BiBTeX, PostScript.
• MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71 (2000).
  Abstract, BiBTeX, PostScript.
• Resolution-Based Methods for Modal Logics. Together with H. de Nivelle and U. Hustadt. Logic Journal of the IGPL 8 (3) 265-292 (2000).
  Abstract, BiBTeX, PostScript, Errata.
  
• Normal Forms and Proofs in Combined Modal and Temporal Logics . Together with U. Hustadt, C. Dixon, and M. Fisher. In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence Vol. 1794, Springer, 73-87 (2000).
  Abstract, BiBTeX, PostScript.
• Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. In Gent, I. P. and van Maaren, H. and Walsh, T. (eds), SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications 63, IOS Press, Amsterdam (2000). Also in a special issue of Journal of Automated Reasoning.
  Abstract, BiBTeX, PostScript.
• An Empirical Analysis of Modal Theorem Provers. Together with U. Hustadt. Journal of Applied Non-Classical Logics 9(4) 479-522 (1999).
  Abstract, BiBTeX, PostScript.
• MSPASS: Subsumption Testing with SPASS. Together with U. Hustadt and C. Weidenbach. In Lambrix, P. et al. (eds.), Proc. of Intern. Workshop on Description Logics'99, Linköping University, 136-137 (1999).
  Abstract, BiBTeX, PostScript.
• Decidability by Resolution for Propositional Modal Logics. Journal of Automated Reasoning 22(4), 379-396 (1999).
  Abstract, BiBTeX, DOI Link.
• Simplification and Backjumping in Modal Tableau. Together with U. Hustadt. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 187-201 (1998).
  Abstract, BiBTeX, PostScript.
• Optimised Functional Translation and Resolution. Together with U. Hustadt and C. Weidenbach. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 36-37 (1998). (Contribution to the comparison section of modal theorem provers).
  Abstract, BiBTeX, PostScript.
• Resolution is a Decision Procedure for Many Propositional Modal Logics. In Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 1, Lecture Notes 87, CSLI Publications, Stanford, 189-208 (1998).
  Abstract, BiBTeX.
• E-Unification for Subsystems of S4. In Nipkow, T. (ed.), Rewriting Techniques and Applications: 9th International Conference, RTA'98, Tsukuba, Japan, Proceedings, Lecture Notes in Computer Science Vol. 1379, Springer, 106-120 (1998).
  Abstract, BiBTeX, PostScript.
• Ordered E-Resolution and Path Logics. Manuscript. Submitted for publication (1998).
  Abstract, BiBTeX.
• Functional Translation and Second-Order Frame Properties of Modal Logics. Together with H.J. Ohlbach. Journal of Logic and Computation 7(5), 581-603 (1997).
  Abstract, BiBTeX.
• On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. In Pollack, M. (ed), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), Vol. 1, Morgan Kaufmann, 202-207 (1997).
  Abstract, BiBTeX.
• Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken, Germany (1997).
  Abstract, BiBTeX, PostScript (851KB).
• Decidability by resolution for many modal logics. Extended abstract of a talk presented at ESSLLI'97, Aix-en-Provence, France (1997).
  Dvi.
• On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. Research Rep. MPI-I-97-2-003, MPI für Informatik, Saarbrücken (1997).
  Abstract, BiBTeX, PostScript.
• Resolution is a Decision Procedure for Many Propositional Modal Logics. Research Rep. MPI-I-97-2-002, MPI für Informatik, Saarbrücken (1997).
  Abstract, BiBTeX, PostScript.
• Translating Graded Modalities into Predicate Logic. Together with H.J. Ohlbach and U.Hustadt. In H. Wansing (ed), Proof Theory for Modal Logic, Applied Logic Series 2, Kluwer, 253-291 (1996).
  Abstract, BiBTeX.
• Symbolic Arithmetical Reasoning with Qualified Number Restrictions. Together with H.J. Ohlbach and U. Hustadt. In Proc. of Intern. Workshop on Description Logics'95 (held in Rome, 2-3 June 1995), Rap.07.95, Dipartimento di Informatica e Sistemistica, Univ. degli studia di Roma, 89-95 (1995).
  Abstract, BiBTeX, PostScript
• The Optimised Functional Translation and Graded Modal Logics. Together with H.J. Ohlbach. Combined abstract of talks held at the RelMiCs'96 Workshop in Parati, Brasil, 10-14 July (1995).
  Abstract, BiBTeX, DVI, PostScript

Description logic, knowledge representation, ontology reasoning

See also Modal logic, dynamic modal logics

• A Practical Approach to Forgetting in Description Logics with Nominals. Together with Y. Zhao, Y. Wang, X. Zhang, H. Feng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3073-3079 (2020).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Ontology Extraction for Large Ontologies via Modularity and Forgetting. Together with J. Chen, G. Alghamdi, D. Walther and Y. Gao. In Kejriwal, M. and Szekely, P. A. and Troncy, R. (eds), Proceedings of the 10th International Conference on Knowledge Capture (K-CAP'19). ACM, 45-52 (2019).
  Abstract, BiBTeX, PDF, DOI link to ACM.
• Extending Forgetting-Based Abduction Using Nominals. Together with W. Del-Pinto. In A. Herzig and A. Popescu (eds), Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). Lecture Notes in Artificial Intelligence, Vol. 11715, Springer, 185-202 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. Togther with Y. Zhao. In P. Fontaine (ed), Automated Deduction: CADE-27. Lecture Notes in Artificial Intelligence, Vol. 11716. Springer, 568-579 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• ABox Abduction via Forgetting in ALC. Together with W. Del-Pinto. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 2768-2775 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach. Together with Y. Zhao, G. Alghamdi, H. Feng, G. Stoilos, D. Juric and M. Khodadadi. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 3116-3124 (2019).
  Abstract, BiBTeX, PDF, DOI link to publisher.
• Methods and Metrics for Knowledge Base Engineering and Integration. Together with G. Stoilos, D. Geleta, S. Wartak, S. Hall, M. Khodadadi, Y. Zhao, and G. Alghamdi. In 9th Workshop on Ontology Design and Patterns (WOP 2018). CEUR Workshop Proceedings, Vol. 2195, CEUR-WS.org, 72-86 (2018).
  Abstract, BiBTeX, PDF.
• On Concept Forgetting in Description Logics with Qualified Number Restrictions. Together with Y. Zhao. In Lang, J. (ed), Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018). AAAI Press/IJCAI, 1984-1990 (2018).
  Abstract, BiBTeX, PDF, Details at publisher.
• FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. Together with Y. Zhao. In Galmiche, D. and Schulz, S. and Sebastiani, R. (eds), Automated Reasoning (IJCAR 2018). Lecture Notes in Artificial Intelligence, Volume 10900, Springer, 19-27 (2018).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• Role Forgetting for ALCOQH(top)-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Sierra, C. (ed), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017). AAAI Press/IJCAI, 1354-1361 (2017).
  Abstract, BiBTeX, PDF.
• Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Lenzerini, M. and Penaloza, R. (eds), Proceedings of the 29th International Workshop on Description Logics (DL-2016). CEUR Workshop Proceedings, Vol. 1577, CEUR-WS.org, 2016.
  Abstract, BiBTeX, PDF.
• Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Arenas et al (eds), The Semantic Web, 14th International Semantic Web Conference, ISWC 2015. Lecture Notes in Computer Science, Vol. 9366, Springer, 587-602 (2015).
  Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
• LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. Together with Y. Zhao. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Saturation-Based Forgetting in the Description Logic SIF. Together with P. Koopmann. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. Together with P. Koopmann. In Bonet, B. and Koenig, S. (eds), Proc. AAAI-2015. AAAI Press, 175-181 (2015).
  Abstract, BiBTeX, PDF.
• Forgetting and Uniform Interpolation of ALC-Ontologies with ABoxes. Together with P. Koopmann. In M. Bienvenu and R. Rosati (eds), Proceedings of the 27th International Workshop on Description Logics (DL-2014). CEUR Workshop Proceedings, Vol. 1193, CEUR-WS.org, 245-257 (2014).
  Abstract, BiBTeX, PDF.
• Count and Forget: Uniform Interpolation of SHQ-Ontologies. Together with P. Koopmann. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448 (2014).
  Abstract, BiBTeX.
• Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. ACM Transactions on Computational Logic 15 (1) (2014).
  Abstract, BiBTeX, DOI link to TOCL.
• Forgetting Concept and Role Symbols in ALCH-Ontologies. Together with P. Koopmann. In McMillan, K., Middeldorp, A. and Voronkov, A. (eds), Proc. LPAR 2013. Lecture Notes in Computer Science, Vol. 8312, Springer, 552-567 (2013).
  Abstract, BiBTeX, PDF (final version will be available from Springer).
• Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12 (2013).
  Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
• Uniform Interpolation of ALC-Ontologies Using Fixpoints. Together with P. Koopmann. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. Together with M. Khodadadi and D. Tishkovsky. In Galmiche, D. and Larchey-Wendling, D. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013). Lecture Notes in Computer Science, Vol. 8123 Springer, 188-202 (2013).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. arXiv e-Print 1208.1476v1 [cs.LO] (2012).
  Abstract, BiBTeX, arXiv Link.
• An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting. Together with M. Khodadadi and D. Tishkovsky. In Kazakov, Y. and Lembo, D. and Wolter, F. (eds), Proceedings of the 2012 International Workshop on Description Logics (DL-2012)., CEUR Workshop Proceedings 846, CEUR-WS.org (2012).
  Abstract, BiBTeX, PDF.
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. Together with D. Tishkovsky. In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209 (2008).
  Abstract, BiBTeX, DOI Link.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• Using Tableau to Decide Expressive Description Logics with Role Negation. Together with D. Tishkovsky. In Aberer, K. et al (eds), The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, Vol. 4825, Springer, 438-451 (2007).
  Abstract, BiBTeX, DOI Link.
• System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520 (2007).
  Abstract, BiBTeX, DOI Link.
• Deciding ALBO with Tableau. Together with D. Tishkovsky. In Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., and Turhan, A. Y. (eds), Proceedings of the 20th International Workshop on Description Logics (DL-2007), Bozen-Bolzano University Press, 135-146 (2007).
  Abstract, BiBTeX, PDF.
• A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276 (2004). Invited overview paper.
  Abstract, BiBTeX, PostScript, PDF.
• On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics. Together with L. Georgieva and U. Hustadt. In Horrocks, I. and Tessaris, S. (eds), Proceedings of the 2002 International Workshop on Description Logics (DL'2002). CEUR Workshop Proceedings, Vol. CEUR-WS/Vol-53, 25-36 (2002).
  Abstract, BiBTeX, PostScript.
• Relational Grammars for Knowledge Representation. In Böttner, M. and Thümmel, W. (eds), Variable-Free Semantics. Artikulation und Sprache, Vol. 3, secolo Verlag, Osnabrück, Germany, 162-180 (2000).
  Abstract, BiBTeX, PostScript.
• Issues of Decidability for Description Logics in the Framework of Resolution. Together with U. Hustadt. In Caferra, R. and Salzer, G. (eds), Automated Deduction in Classical and Non-Classical Logic, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, 191-205 (2000).
  Abstract, BiBTeX, PostScript.
• On the Relation of Resolution and Tableaux Proof Systems for Description Logics. Together with U. Hustadt. In Dean, T. (ed), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99). Vol. 1, Morgan Kaufmann, 110-115 (1999).
  Abstract, BiBTeX, PDF.
• Description Logics for Natural Language Processing. Together with D. Fehrer, U. Hustadt, M. Jaeger, A. Nonnengart, H.J. Ohlbach, Ch. Weidenbach and E. Weydert. In Proc. of Intern. Workshop on Description Logics'94, Document D-94-10, DFKI, Saarbrücken, 80-84 (1994).
  Abstract, BiBTeX, PostScript
• Existential Graphs for Terminological Logics. Manuscript (1994).
  Abstract, BiBTeX
• Terminological Representation, Natural Language and Relation Algebra. In Ohlbach, H. J. (Ed.), Proc. of the sixteenth German AI Conf. (GWAI'92), Lecture Notes in Artificial Intelligence Vol. 671, Springer, Berlin, 357-371 (1993).
  Abstract, BiBTeX, PostScript
• Subsumption Computed Algebraically. Together with C. Brink. Computers and Mathematics with Applications 23 (2-9), Special edition on Semantic Networks in Artificial Intelligence, 329-342 (1992).
  Abstract, BiBTeX, DOI Link.
• MOTEL User Manual. Together with U. Hustadt A. Nonnengart and J. Timm. Tech. Rep. MPI-I-92-236, MPI für Informatik, Saarbrücken (1992).
  Abstract, BiBTeX, DVI, PostScript
• Algebraic Terminological Representation. Tech. Rep. MPI-I-91-216, MPI für Informatik, Saarbrücken (1991).
  Abstract, BiBTeX, DVI, PostScript

Intuitionistic logic and other non-classical logics

• A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519, 2016.
  Abstract, BiBTeX, DOI Link to Elsevier.
• Tableau Development for a Bi-Intuitionistic Tense Logic. Together with J. G. Stell and D. Rydeheard. In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds), Relational and Algebraic Methods in Computer Science (RAMiCS 14). Lecture Notes in Computer Science, Vol. 8428, Springer, 412-428 (2014).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324 (2009).
  Abstract, BiBTeX, PDF, DOI Link.

Temporal logic

• Labelled Tableaux for Temporal Logic with Cardinality Constraints. Together with C. Dixon, B. Konev, and D. Tishkovsky. Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). IEEE Computer Society, 111-118 (2012).
  Abstract, BiBTeX, DOI, PDF.
• Investigating Finite Models of Non-Classical Logics with Relation Algebra and RelView. Together with R. Berghammer. In de Swart, H. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Artficial intelligence Vol. 4342, Springer, 31-49 (2006).
  Abstract, BiBTeX, PDF.
• Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors, Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series, Springer (2006).
  Abstract, BiBTeX, PDF.
• Deciding Monodic Fragments by Temporal Resolution. Together with U. Hustadt and B. Konev. In Nieuwenhuis, R. (eds), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Vol. 3632, Springer, 204-218 (2005).
  Abstract, BiBTeX, PDF, Full text via Springer.
• Scientific Benchmarking with Temporal Logic Decision Procedures. Together with U. Hustadt. In Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A. (eds), Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR'2002). Morgan Kaufmann, 533-544 (2002).
  Abstract, BiBTeX, PDF.
• Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Together with U. Hustadt. In Giunchiglia, E. and Massacci, F. (eds), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitä degli Studi di Siena, Siena, Italy, 68-76 (2001).
  Abstract, BiBTeX, PostScript.
• Normal Forms and Proofs in Combined Modal and Temporal Logics . Together with U. Hustadt, C. Dixon, and M. Fisher. In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence Vol. 1794, Springer, 73-87 (2000).
  Abstract, BiBTeX, PostScript.
• Reasoning about Agents in the KARO Framework. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Bettini, C. and Montanari, A. (eds), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME'2001). IEEE Computer Society, 206-213 (2001).
  Abstract, BiBTeX.

Second-order logic

• The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74 (2012).
  Abstract, BiBTeX, DOI.
• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.

Algebraic logic

• Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications (2008).
  Back-cover, BiBTeX, Publisher's info.
• Investigating Finite Models of Non-Classical Logics with Relation Algebra and RelView. Together with R. Berghammer. In de Swart, H. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Artficial intelligence Vol. 4342, Springer, 31-49 (2006).
  Abstract, BiBTeX, PDF.
• Two Proof Systems for Peirce Algebras. Together with E. Orlowska and U. Hustadt. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 238-251 (2004).
  Abstract, BiBTeX, Springer Link.
• Relational Grammars for Knowledge Representation. In Böttner, M. and Thümmel, W. (eds), Variable-Free Semantics. Artikulation und Sprache, Vol. 3, secolo Verlag, Osnabrück, Germany, 162-180 (2000).
  Abstract, BiBTeX, PostScript.
• Peirce Algebras. Together with C. Brink and K. Britz. Formal Aspects of Computing 6 (3), 339-358 (1994).
  Abstract, BiBTeX, DVI, PostScript
• Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract. SIGALA Newsletter 2 (1) 27 (1994). Abstract of a talk held at the Dagstuhl Seminar on Relational Methods in Computer Science, Dagstuhl, Germany (January 1994).
  Abstract, BiBTeX, DVI, PostScript
• Terminological Logics and Conceptual Graphs: An Historical Perspective. Extended Abstract. In Kunze, J. and Stoyan, H. (eds), KI-94 Workshops: Extended Abstracts, Gesellschaft für Informatik, Bonn (1994).
  Abstract, BiBTeX, DVI, PostScript
• Representations as Full Peirce algebras: Extended Abstract. Manuscript (1994).
  Abstract, BiBTeX
• Peirce Algebras and Relation Algebras are equipollent. Manuscript (1994).
  Abstract, BiBTeX
• Terminological Representation, Natural Language and Relation Algebra. In Ohlbach, H. J. (Ed.), Proc. of the sixteenth German AI Conf. (GWAI'92), Lecture Notes in Artificial Intelligence Vol. 671, Springer, Berlin, 357-371 (1993).
  Abstract, BiBTeX, PostScript
• Subsumption Computed Algebraically. Together with C. Brink. Computers and Mathematics with Applications 23 (2-9), Special edition on Semantic Networks in Artificial Intelligence, 329-342 (1992).
  Abstract, BiBTeX, DOI Link.
• Algebraic Terminological Representation. Tech. Rep. MPI-I-91-216, MPI für Informatik, Saarbrücken (1991).
  Abstract, BiBTeX, DVI, PostScript

Agents

• Concept Description and Definition Extraction for the ANEMONE System. Together with D. Toluhi and B. Parsia. In Alechina, N. and Baldoni, M. and Logan, B. (eds), Engineering Multi-Agent Systems (EMAS 2021), Revised Selected Papers. Lecture Notes in Computer Science, Vol. 13190, Springer, Cham, 352-372 (2021).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information. 17 (1) 109-129 (2008).
  Abstract, BiBTeX, Full text via Springer.
• Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors, Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series, Springer (2006).
  Abstract, BiBTeX, PDF.
• Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic. Together with D. Tishkovsky and U. Hustadt. Studia Logica. To appear.
  Abstract, BiBTeX, SpringerLink.
• Multi-Agent Dynamic Logics with Informational Test. Together with D. Tishkovsky. Annals of Mathematics and Artificial Intelligence 42 (1-3), 5-36 (2004).
  Abstract, BiBTeX, SpringerLink.
• Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic Together with D. Tishkovsky and U. Hustadt. Preprint Series CSPP-27, University of Manchester, UK (2003).
  Abstract, BiBTeX, PostScript.
• Combining Dynamic Logic with Doxastic Modal Logics. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 4. Chapter 18, King's College London Publications, 371-391 (2003).
  Abstract, BiBTeX.
• Multi-Agent Logic of Dynamic Belief and Knowledge. Together with D. Tishkovsky. In Flesca, S. and Greco, S. and Leone, N. and Ianni, G. (eds), Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Artificial Intelligence Vol. 2424, Springer, 38-49 (2002).
  Abstract, BiBTeX, PostScript.
• Reasoning about Agents in the KARO Framework. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Bettini, C. and Montanari, A. (eds), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME'2001). IEEE Computer Society, 206-213 (2001).
  Abstract, BiBTeX.
• Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Rash, J. L., Rouff, C. A., Truszkowski, W., Gordon, D. and Hinchey, M. G. (eds), Formal Approaches to Agent-Based Systems. Lecture Notes in Artificial Intelligence Vol. 1871, Springer, 33-47 (2001).
  Abstract, BiBTeX.

System descriptions

• FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. Togther with Y. Zhao. In P. Fontaine (ed), Automated Deduction: CADE-27. Lecture Notes in Artificial Intelligence, Vol. 11716. Springer, 568-579 (2019).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. Together with Y. Zhao. In Galmiche, D. and Schulz, S. and Sebastiani, R. (eds), Automated Reasoning (IJCAR 2018). Lecture Notes in Artificial Intelligence, Volume 10900, Springer, 19-27 (2018).
  Abstract, BiBTeX, PDF, DOI link to Springer.
• LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org (2015).
  Abstract, BiBTeX, PDF.
• The Tableau Prover Generator MetTeL2. Together with D. Tishkovsky and M. Khodadadi. In del Cerro, L. F. and Herzig, A. and Mengin, J. (eds), Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA 2012). Lecture Notes in Computer Science Vol. 7519, Springer, 492-495 (2012).
  Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
• MetTeL: A Tableau Prover with Logic-Independent Inference Engine. Together with D. Tishkovsky and M. Khodadadi. 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 (2011).
  Abstract, BiBTeX, DOI Link.
• System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520 (2007).
  Abstract, BiBTeX, DOI Link.
• MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71 (2000).
  Abstract, BiBTeX, PostScript.
• MSPASS: Subsumption Testing with SPASS. Together with U. Hustadt and C. Weidenbach. In Lambrix, P. et al. (eds.), Proc. of Intern. Workshop on Description Logics'99, Linköping University, 136-137 (1999).
  Abstract, BiBTeX, PostScript.

Special journal issues

• Special Issue of Selected Extended Papers of CADE-22. Together with Brigitte Pientka (eds). Journal of Automated Reasoning 47 (2) (2011).
  BiBTeX, Editorial, Special issue.
• Special issue on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). AI Communications 23 (2-3) (2010).
  BiBTeX, Editorial, Special issue.
• Special issue on Empirically Successful Computerized Reasoning. Together with G. Sutcliffe and S. Schulz (eds). Journal of Applied Logic 7 (1) (2009).
  Abstract, BiBTeX, Link to JAL.
• Special issue on Relations and Kleene Algebras in Computer Science. Together with G. Struth (eds). Journal of Logic and Algebraic Programming 76 (1) (2008).
  Abstract, BiBTeX, Link to JLAP.
• Special issue on Implementation of Logics. Together with B. Konev and S. Schulz (eds). Journal of Applied Non-Classical Logic 16 (1-2) (2006).
  Abstract, BiBTeX, Full text via JANCL.

Proceedings

• Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021). Together with C. Wernhard and Y. Zhao (eds) (2021). CEUR Workshop Proceedings, Vol. 3009, CEUR-WS.org (2021).
  Abstract, BiBTeX, Proceedings.
• Proceedings of the 34th International Workshop on Description Logics (DL 2021). Together with M. Homola and V. Ryzhikov (eds) (2021) CEUR Workshop Proceedings, Vol. 2954, CEUR-WS.org (2021).
  Abstract, BiBTeX, Proceedings.
• Automated Reasoning with Analytic Tableaux and Related Methods. The 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28, 2017, Proceedings. Together with C. Nalon (eds), Lecture Notes in Artificial Intelligence, Vol. 10501, Springer (2017).
  Abstract, BiBTeX, DOI Link.
• Frontiers of Combining Systems-FroCoS 2013. 9th International Symposium on Frontiers of Combining Systems, Nancy, September 18-20, 2013. Proceedings. Together with P. Fontaine and C. Ringeissen (eds). Lecture Notes in Artificial Intelligence, Vol. 8152, Springer (2013).
  Abstract, BiBTeX, DOI Link.
• PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. Together with P. Fontaine and S. Schulz (eds). EPiC Series, Vol. 21, EasyChair (2013).
  Abstract, BiBTeX, Proceedings.
• Proceedings of the 19th Automated Reasoning Workshop. Together with F. Papacchini (eds). Escholar uk-ac-man-scw:161817, The University of Manchester, UK (2012).
  Abstract, BiBTeX, Proceedings.
• PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). EPiC Series, Vol. 9, EasyChair (2012).
  Abstract, BiBTeX, Proceedings.
• Automated Deduction-CADE-22. 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Schmidt, R. A. (ed), Lecture Notes in Artificial Intelligence, Vol. 5663, Springer (2009).
  Abstract, BiBTeX, DOI Link.
• Reasoning Web: Semantic Technologies for Information Systems. 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30-September 4, 2009, Tutorial Lectures. Together with Tessaris, S., Franconi, E., Eiter, Th., Gutierrez, C., Handschuh, S., Rousset, M.-C. (eds), Lecture Notes in Computer Science: Information Systems and Applications, incl. Internet/Web, and HCI, Vol. 5689, Springer (2009).
  Abstract, BiBTeX, DOI Link.
• Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (KEAPPA & IWIL 2008). Together with Rudnicki, P., Sutcliffe, G., Konev, B., and Schulz, S. (eds), CEUR Workshop Proceedings, Vol. 418 (2008).
  Abstract, BiBTeX, Full text via CEUR.
• Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning (PAAR-2008/ESHOL-2008). Together with B. Konev and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 373 (2008).
  Abstract, BiBTeX, Full text via CEUR.
• Relations and Kleene Algebra in Computer Science: Proceedings of RelMiCS/AKA 2006. Schmidt, R. A. (ed), Lecture Notes in Computer Science, Vol. 4136, Springer (2006).
  Abstract, BiBTeX, Full text via Springer.
• Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), 3rd International Joint Conference on Automated Reasoning. Together with G. Sutcliffe and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 192 (2006).
  Abstract, BiBTeX, Full text via CEUR.
• Advances in Modal Logic, Volume 5. Together with I. Pratt-Hartmann, M. Reynolds, and H. Wansing (eds). King's College Publications, London (2005).
  Abstract, BiBTeX, Online version.
• AiML-2004: Advances in Modal Logic. Together with I. Pratt-Hartmann, M. Reynolds and H. Wansing (eds). Technical Report UMCS-04-09-01, University of Manchester, UK (2004).
  Abstract, BiBTeX, PDF.
• Fourth International Workshop on the Implementation of Logics. Together with B. Konev (eds). Technical Report ULCS-03-018, University of Liverpool (2003).
  Abstract, BiBTeX, PDF.

Miscellaneous

• Editorial: The possibility of generating true conjectures. Together with H. J. Ohlbach. Journal of Logic and Computation, 3(4), 341-343 (1993).
  BiBTeX.
• Autodescriptivity: Beware! Together with C. Brink and I.M. Rewitzky. The Computer Journal 34 (4), 380-381 (1991).
  Abstract, BiBTeX, DOI Link.

---

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

---

Last modified: 23 Jul 22

Copyright © 1996-2020 Renate A. Schmidt, School of Computer Science, Univ. Man., schmidt@cs.man.ac.uk