The detailed objectives of the research were
We examined the two-dimensional classical combination of the most fundamental modal system, K, and showed how to construct finite models from mosaic-representations of the components, so establishing the `finite model property' for this combination of logics by a new and simple method. We determined the complexity of the satisfiability problem for formulas of modal depth two, thus making a significant step towards finding the complexity of this two-dimensional combination which is an important open problem in the area.
We solved the fundamental problem of the decidability of most important systems of dimension at least 3, as well as providing results on finite axiomatisability and the product finite model property.
Classical n-variable first-order logic is in effect a n-dimensional combined system. Here, we showed that each extra dimension above 4 introduces infinitely more complexity. This confirmed a conjecture about neat embeddings of cylindric algebras made in 1969 by J. D. Monk, confirmed a later conjecture by Maddux about relation algebras obtained from cylindric algebras, and solved a problem raised by Tarski and Givant (1987).
We also proved that locally cubic relativizations of products of modal logics are decidable, plus further strong results on complexity of relativised products of modal logics, and implementations were undertaken in workpackage E4 (see below).
In joint work with Wolter and Zakharyaschev, we combined classical and
temporal systems while syntactically limiting their interaction in a new
way. We defined a new kind of fragment of first-order temporal logic, the
monodic
fragment, where formulas beginning with a temporal operator are allowed
at most one free variable. We showed that given an oracle for
satisfiability of first-order logic, we can decide satisfiability of formulas
in the fragment. Our arguments cover most of the major flows of time and
both the arbitrary- and finite-domain cases. The oracle can be eliminated
by working in any of the commonly-used decidable fragments of first-order
logic. We can talk about objects in the intended domain using the full
power of the selected fragment; however, temporal operators may be used
to describe the development in time of only one object. Our results
seem to be near-optimal, since we can prove that only very small manipulations
of the fragments result in undecidable (and not even recursively enumerable)
logics.
The decision problem for first-order temporal logic was effectively
dead --- over thirty years, only negative results were known. Our paper
identifies the first interesting decidable fragment of first-order temporal
logic.
It opens up a new direction of research, namely the classification
of fragments of first-order temporal logic by their decidability.
There are potential applications in temporal databases and knowledge bases.
One aspect of this work was to vary the choice of operators. It was hoped to discover which operators were safe for good computational behaviour, and which were dangerous. We had already shown that any subreduct of the class of representable relation algebras whose similarity type includes intersection, relation composition and converse is a non-finitely axiomatizable quasivariety and that its equational theory is not finitely based. We extended this work to subreducts of representable cylindric algebras of dimension at least three whose similarity types include intersection and cylindrifications. A similar result was proved for subreducts of representable sequential algebras. In related work, we showed that the `network satisfaction problem', to determine consistency of a interlocking system of binary constraints, is in general undecidable.
We considered arrow logic augmented with various kinds of infinite counting modalities, such as `much more', `of good quantity', `many times'. It was shown that the addition of these modal operators to weakly associative arrow logic results in finitely axiomatisable and decidable logics --- the first such extensions of weakly associative arrow logic that do not have the finite model property.
Arrow logic with projections was long known to be extremely expressive. Still, it is quite surprising that adding projections can even spoil the robust decidability of weakly associative arrow logic: we proved that some of these systems are even not recursively enumerable, using a reduction of unsolvable Diophantine equations. This negative property was shown to be an artifact of the underlying set theory --- certain non-well-founded set theories interpret the meaning of projections so as to allow finite axiomatisability even of full arrow logic with projections. Variants of the algebraic analogues of these systems --- fork algebras --- were in part invented and widely investigated by the specification-verification community, and our results are notable contributions to this field.
We announced new kinds of dynamic relativised representations for relation algebras, preserving many classical features, such as commutativity of quantifiers up to a given complexity, yet with much better behaviour than their classical counterparts. The finite model property for many such systems follows from another of our results (see below).
We also developed the general methodology of algebraic logic in the dynamic paradigm. A general method of finding natural axioms for a wide range of dynamic systems was developed in joint work with Venema. The approach uses games. A still more general approach will appear in a forthcoming book, where even simpler axioms in an expanded signature related to Jonsson's Q-operators are given.
Further positive results were obtained in dynamic logic itself, on one of the most powerful dynamic-style logics, the loosely guarded fragment of first-order logic. The LGF was devised by van Benthem as a first-order version of modal logic. We showed using a Herwig-style construction that the LGF has the finite model property. This has already proved useful in extending other work. It fills a gap in knowledge of the LGF and contributes to the growing status of `guarded' quantification in dynamic logic.
Contacts:
Dr I. Hodkinson,
Department of Computing,
Imperial College,
180 Queen's Gate,
London SW7 2BZ, UK.
(imh@doc.ic.ac.uk)
Dr R Hirsch,
Department of Computer Science
University College London
Gower Street
London WC1
(R.Hirsch@cs.ucl.ac.uk)