Path-Based Reasoning for Guarded Formulae, EPSRC Project GR/M36700/02

General

Dates

• Start date: 01/09/1999
• End date: 31/08/2002

Personnel

• Principal investigator: Renate Schmidt
• PhD student: Lilia Georgieva

Co-authors

• Dixon, C.
• Fisher, M.
• Ganzinger, H.
• Hustadt, U.
• Meyer-Kirsch, C.
• De Nivelle, H.

Outputs

Implementations

• The MSPASS theorem prover (Hustadt and Schmidt 2000a) - an enhancement of the first-order theorem prover SPASS with a translator of modal and description logic formulae into first-order logic with equality. Development started in 1998 and was continued within this project.
• The TABSPASS theorem prover (Hustadt and Schmidt 2000b, Hustadt and Schmidt 2002a) - a modified version of the first-order theorem prover SPASS which simulates derivations of tableaux-based decision procedures for basic modal logic.
• The TRP theorem prover (Hustadt and Schmidt 2001, Hustadt and Schmidt 2002b) - a protoypical implementation of a temporal resolution calculus for propositional linear-time logic.

Publications

2002

A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester. Also to appear 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.

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.

Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation. To appear.
Abstract, BiBTeX.

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

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