Publications

• Books
• Surveys
• Automated reasoning / decidability / proof theory
• Second-order quantifier elimination
• Model building / minimal model reasoning
• Benchmarking
• First-order logic
• Modal logic, dynamic modal logics
• Description logic, knowledge representation, ontology reasoning
• Temporal logic
• Second-order logic
• Algebraic logic
• Agents
• System descriptions
• Special 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

• 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.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Springer. To appear. Invited overview paper.
  Abstract, BiBTeX, PDF.
• 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

• 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.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Springer. To appear. Invited overview paper.
  Abstract, BiBTeX, PDF.
• 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, DOI Link to journal.
• 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, 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.
• 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.

Second-order quantifier elimination

• 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.

Model building / minimal model reasoning

• 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.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Springer. To appear. Invited overview paper.
  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, DOI Link to journal.
• 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

• 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

• 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.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Springer. To appear. Invited overview paper.
  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.
• 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

• 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.
• First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Springer. To appear. Invited overview paper.
  Abstract, BiBTeX, PDF.
• 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, DOI Link to journal.
• 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 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, PostScript.
• 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

Temporal logic

• 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

• 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

• 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 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 International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010). Together with B. Konev and S. Schulz (eds). Edinburgh, UK, July 14, 2010, EasyChair Proceedings (2010).
  Abstract, BiBTeX.
• 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: 02 Feb 12

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