EPSRC Funded PhD Studentship in Logic and Theorem-Proving

An EPSRC funded PhD studentship is available in the Logic and Computation Group in the Department of Computing at Manchester Metropolitan University. The Logic and Computation research group is one of the most active and successful groups within the University and well known internationally.

The studentship is available from as soon as possible (September 1999 at the latest) for up to 3 years with a grant of 6455 pounds per annum, payment of fees (EU rate) and travel money for attending conferences and workshops.

The title of the project is Path-Based Reasoning about Guarded Formulae and will be supervised by Dr. Renate Schmidt. The ideal candidate will have a background and a keen interest in at least one of the following: formal methods, logic (first-order logic and non-classical logics) and automated deduction. Some programming experience is advisable.

Deadline for applications is 17 May 1999.

To apply for this studentship, send a CV, names of two referees and covering letter to:

: Dr. Renate Schmidt, Department of Computing and Mathematics, Manchester Metropolitan University, Chester Street, Manchester M1 5GD, United Kingdom.
Email: R.A.Schmidt@doc.mmu.ac.uk, Tel: +44 161 247 1490, Fax: +44 161 247 1483.

Email submission of PostScript or plain text is acceptable.

If you require any further details concerning this project, please contact Renate Schmidt (R.A.Schmidt@doc.mmu.ac.uk).

Overview

The aim of this project is to facilitate automated reasoning for first-order generalisations of propositional modal logics, which have recently received considerable attention in the research community. In particular, the project involves studying and applying a new path-based translation approach, which has already brought forth useful new techniques and results for propositional modal logics.

Background

Modal logics, including temporal logics, are widely accepted to provide appropriate formal frameworks for an ever increasing number of different application areas of computer science. In the field of knowledge representation concerned with description logics, modal logics arise in the form of the basic multi-modal logic and propositional dynamic logic. Propositional dynamic logic also forms the basis of many agent-based systems. Arrow logic is a general logic of transitions (relations) and provides a wide application area from philosophy to computer science. Other important areas where complex modal and temporal logics are beginning to be used are accident analysis, legal reasoning, distributed systems, natural language analysis, configuration of technical systems and maintenance of terminology servers for a medical domain. The popularity of (extended) modal logics can be attributed to their simple language, their natural semantics and decidability. In the light of this, the growing interest in sophisticated and efficient theorem provers (evident, for example, in the current series of comparison sessions of modal theorem provers at events, like TABLEAUX'98 and DL'98) is not surprising.

We use existing resolution theorem provers on first-order translations of modal logics [1,2,3]. This enables us to make use of the power of both first-order logic and the resolution framework, especially the saturation-based method of [4,5]. Our work shows this approach has several advantages: often not much effort is needed to obtain terminating proof procedures [6,7,8], and, there are sophisticated first-order theorem provers which allow for efficient modal theorem proving [9,10,11]. Translation-based approaches also circumvent the limitations that special purpose modal reasoners have regarding extendibility. Existing modal theorem provers are mostly tuned for a small set of the weakest modal logics and description logics (K, KT, S4, KD45, S5, K(m), ALC), but experience shows users want more expressiveness in the form of additional operations.

The guarded and loosely guarded fragments, which we intend to study, encompass many extended modal logics and description logics, and despite the increased expressiveness the guarded fragments have many of the desirable properties of propositional modal logics, most notably decidability. As with modal logics this makes them attractive for applications in computer science. The guarded fragments were introduced in [12,13,14] in an endeavour to generalise the modal approach of using conditional quantifiers and accessibility constraints for first-order logic. In the guarded fragment, quantifiers are allowed to have the following form (or its dual).

: exists y (R x, y /\ phi(x, y))

R x, y denotes an atom in which every argument is a variable. The variables in the finite sequences x and y may occur in any multiplicity and order. In the loosely guarded fragment, quantifiers are a generalisation in which the guards need not be one literal but may consist of a conjunction of literals. In recent work, de Nivelle [14] introduces resolution decision procedures for both fragments. The procedures require special ordering refinements not standardly available in existing theorem provers.

This project will explore a new approach exploiting more of the semantic properties of the logics, which we envisage will result in more effective theorem proving systems, possibly avoiding non-standard refinement strategies. Just as the guarded fragments generalise modal logics, we will attempt to generalise the optimised functional translation approach of propositional modal logics [15,16,17] and apply it to the guarded fragments. We believe the proposed approach will have some of computational advantages that the functional translation approach has over the standard relational translation approach of propositional modal logic.

References

H. J. Ohlbach and R. A. Schmidt. Functional translation and second-order frame properties of modal logics. J. Logic Computat., 7(5):581-603, 1997.
H. J. Ohlbach, R. A. Schmidt, and U. Hustadt. Translating graded modalities into predicate logic. In H. Wansing, editor, Proof Theory of Modal Logic, volume 2 of Applied Logic Series, pages 253-291. Kluwer, 1996.
R. A. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Univ. d. Saarlandes, Germany, 1997.
L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. J. Logic Computat., 4(3):217-247, 1994.
L. Bachmair and H. Ganzinger. A theory of resolution. Research Report MPI-I-97-2-005, MPI f. Informatik, Saarbrücken, 1997. To appear in the Handbook of Automated Reasoning.
R. A. Schmidt. Resolution is a decision procedure for propositional modal logics. To appear in Journal of Automated Reasoning, 1998.
U. Hustadt and R. A. Schmidt. Issues of Decidability for Description Logics in the Framework of Resolution. In Caferra, R. and Salzer, G. (eds), First-order Theorem Proving - FTP'98, Technical Report E1852-GS-981, Technische Universität Wien, Vienna, Austria, 152-161. To appear in Lecture Notes in Computer Science, Springer.
H. Ganzinger, U. Hustadt, C. Meyer and R. A. Schmidt. A Resolution-Based Decision Procedure for Extensions of K4. To appear in Advances in Modal Logic, Volume 2, CSLI Publications, Stanford.
U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logics. In M. Pollack, editor, Proc. IJCAI'97, pages 202-207. Morgan Kaufmann, 1997.
U. Hustadt and R. A. Schmidt. An empirical analysis of modal theorem provers. To appear in J. Appl. Non-Classical Logics, 1998.
U. Hustadt, R. A. Schmidt, and C. Weidenbach. Optimised functional translation and resolution. In Proc. TABLEAUX'98, LNCS 1397, pages 36-37. Springer, 1998.
H. Andréka, J. van Benthem, and I. Neméti. Back and forth between modal logic and classical logic. Bull. IGPL, 3(5):685-720, 1995.
H. Andréka, I. Neméti, and J. van Benthem. Modal languages and bounded fragments of predicate logic. J. Phil. Logic, 27(3):217-274, 1998.
J. van Benthem. Dynamic bits and pieces. Research Report LP-1997-01, ILLC, Univ. Amsterdam, 1997.
H. de Nivelle. A Resolution Decision Procedure for the Guarded Fragment. In Automated Deduction: CADE-15, LNAI 1421, pages 191-204. Springer, 1998.
H. J. Ohlbach. Semantics based translation methods for modal logics. J. Logic Computat., 1(5):691-746, 1991.
Y. Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint. J. Logic Computat., 2(3):247-297, 1992.
L. Fariñas del Cerro and A. Herzig. Modal deduction with applications in epistemic and temporal logics. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming: Epistemic and Temporal Reasoning, volume 4, pages 499-594. Clarendon Press, 1995.

Last modified: 16 Apr 99