Publications

To appear

Special issue on Empirically Successful Computerized Reasoning. Together with G. Sutcliffe and S. Schulz (eds). Journal of Applied Logic.
Abstract, BiBTeX, Link to JAL.

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

2008

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.
Abstract, BiBTeX, Full text via CEUR.

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.
Abstract, BiBTeX, DOI Link.

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.
Abstract, BiBTeX, Full text via CEUR.

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.
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. Back-cover, BiBTeX, Publisher's info. Order at amazon.co.uk, Order at amazon.com, Order at amazon.de.

Special issue on Relations and Kleene Algebras in Computer Science. Together with G. Struth (eds). Journal of Logic and Algebraic Programming 76 (1). Abstract, BiBTeX, Link to JLAP.

On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information 17 (1) 109-129.
Abstract, BiBTeX, Full text via Springer.

2007

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.
Abstract, BiBTeX, DOI Link.

The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55.
Abstract, BiBTeX, DOI Link to journal.

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.
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.
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. Commissioned overview paper.
Abstract, BiBTeX, Link to Elsevier.

2006

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.
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. Invited paper.
Abstract, BiBTeX, PostScript.

Relations and Kleene Algebra in Computer Science: Proceedings of RelMiCS/AKA 2006. Schmidt, R. A. (ed), Lecture Notes in Computer Science, Vol. 4136, Springer. Abstract, BiBTeX, Full text via Springer.

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.
Abstract, BiBTeX, Full text via Springer.

Special issue on Implementation of Logics. Together with B. Konev and S. Schulz (eds). Journal of Applied Non-Classical Logic 16 (1-2). Abstract, BiBTeX, Full text via JANCL.

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.
Abstract, BiBTeX, Full text via CEUR.

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.
Abstract, BiBTeX, PDF.

2005

Advances in Modal Logic, Volume 5. Together with I. Pratt-Hartmann, M. Reynolds, and H. Wansing (eds). King's College Publications, London. Abstract, BiBTeX, Online version.

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.
Abstract, BiBTeX, PDF, Full text via Springer.

2004

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. Invited overview paper.
Abstract, BiBTeX, PostScript, PDF.

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. Preprint Series CSPP-22, University of Manchester, UK.
Abstract, BiBTeX, PostScript, SpringerLink.

Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Together with D. Tishkovsky and U. Hustadt. Studia Logica 78 (3), 381-415.
Abstract, BiBTeX, SpringerLink.

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.

Multi-Agent Dynamic Logics with Informational Test. Together with D. Tishkovsky. Annals of Mathematics and Artificial Intelligence 42 (1-3), 5-36.
Abstract, BiBTeX, SpringerLink.

SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R., 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.
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.
Abstract, BiBTeX.

2003

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.
Abstract, BiBTeX, PostScript.

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. 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.
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.
Abstract, BiBTeX.

Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192.
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.
Abstract, BiBTeX, PostScript.

2002

Logics with Commuting Action and Informational Modalities. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. (eds), Advances in Modal Logic, Workshop Proceedings AiML'2002. 91-108.
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.
Abstract, BiBTeX, PostScript.

A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester. Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
Abstract, BiBTeX, PostScript.

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.
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.
BiBTeX, PostScript.

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.
Abstract, BiBTeX, PDF.

Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. Journal of Automated Reasoning 28 (2) 205-232.
Abstract, BiBTeX, PostScript.

2001

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.
Abstract, BiBTeX.

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.
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.
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.
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.
Abstract, BiBTeX, PostScript.

2000

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.
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.
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.
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.
Abstract, BiBTeX.

Resolution-Based Methods for Modal Logics. Together with H. de Nivelle and U. Hustadt. Logic Journal of the IGPL 8 (3) 265-292.
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.
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. Also in a special issue of Journal of Automated Reasoning.
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.
Abstract, BiBTeX, PostScript.

1999

An Empirical Analysis of Modal Theorem Provers. Together with U. Hustadt. Journal of Applied Non-Classical Logics 9(4) 479-522.
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.
Abstract, BiBTeX, PostScript.

Decidability by Resolution for Propositional Modal Logics. Journal of Automated Reasoning 22(4), 379-396.
Abstract, BiBTeX, DOI Link.

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.
Abstract, BiBTeX, PostScript.

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.
Abstract, BiBTeX, PostScript.

1998

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.
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. (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.
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.
Abstract, BiBTeX, PostScript.

Ordered E-Resolution and Path Logics. Manuscript. Submitted for publication.
Abstract, BiBTeX.

1997

Functional Translation and Second-Order Frame Properties of Modal Logics. Together with H.J. Ohlbach. Journal of Logic and Computation 7(5), 581-603.
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.
Abstract, BiBTeX.

Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken, Germany.
Abstract, BiBTeX, PostScript (851KB).

Decidability by resolution for many modal logics. Extended abstract of a talk presented at ESSLLI'97, Aix-en-Provence, France.
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.
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.
Abstract, BiBTeX, PostScript.

1996

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.
Abstract, BiBTeX.

1995

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.
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.
Abstract, BiBTeX, DVI, PostScript

1994

Peirce Algebras. Together with C. Brink and K. Britz. Formal Aspects of Computing 6 (3), 339-358.
Abstract, BiBTeX, DVI, PostScript

Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract. SIGALA Newsletter 2 (1) 27. Abstract of a talk held at the Dagstuhl Seminar on Relational Methods in Computer Science, Dagstuhl, Germany (January 1994).
Abstract, BiBTeX, DVI, 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.
Abstract, BiBTeX, 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.
Abstract, BiBTeX, DVI, PostScript

Representations as Full Peirce algebras: Extended Abstract. Manuscript.
Abstract, BiBTeX

Existential Graphs for Terminological Logics. Manuscript.
Abstract, BiBTeX

Peirce Algebras and Relation Algebras are equipollent. Manuscript.
Abstract, BiBTeX

1993

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.
Abstract, BiBTeX, PostScript

Editorial: The possibility of generating true conjectures. Together with H. J. Ohlbach. Journal of Logic and Computation, 3(4), 341-343.
BiBTeX.

1992

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.
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.
Abstract, BiBTeX, DVI, PostScript

1991

Autodescriptivity: Beware! Together with C. Brink and I.M. Rewitzky. The Computer Journal 34 (4), 380-381.
Abstract, BiBTeX, DOI Link.

Algebraic Terminological Representation. Tech. Rep. MPI-I-91-216, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, DVI, PostScript