 |
|
|
MANY-DIMENSIONAL MODAL LOGICS: THEORY AND APPLICATIONS, 148
| |
| | |
|
|
To order this title, and for more information, click here
By
A. Kurucz, King's College, London, UK
F. Wolter, University of Liverpool, UK
M. Zakharyaschev, King's College, London, UK
Dov M. Gabbay, King's College London, UK
Preface & Foreword
Modal logic is a discipline of many facets. It was baptized in
philosophy, and for a long time it was known as 'the logic of
necessity and possibility.' The modal analysis of the 'mathematical necessity'-provability-brought modal logic to the foundations of
mathematics. The discovery of topological and algebraic semantics for
modal logic connected it with general topology and universal algebra,
and the fact that first-order logic can be regarded as a propositional
modal logic opened a 'modal perspective' in classical mathematical
logic. But the most amazing metamorphosis happened when it turned out
that modal logic could provide languages for talking about various
relational structures, such as state transition systems for computer
programs, semantic networks for knowledge representation, or attribute
value structures in linguistics-languages that combined both
sufficient expressive power and effectiveness! This opened new rich
and rapidly growing application fields in computer science, artificial
intelligence, linguistics, as well as in mathematics itself.
A great many systems with various kinds of modal operators have been
constructed in the last few decades in order to provide effective
formalisms for talking about time, space, knowledge, beliefs, actions,
obligations, etc.: temporal, spatial, epistemic, dynamic, deontic, and
so forth. However, modern applications often require rather complex
formal models and corresponding languages that are capable of
reflecting different features of the application domain. For instance,
to analyze the behavior of a multi-agent distributed system we may
need a formalism containing both epistemic operators for capturing the
knowledge of agents and temporal operators for taking care of the
development of this knowledge in time. In other words, we should
construct a suitable combination of epistemic and temporal
logics. Borrowing the geometrical terminology, one can call the
resulting hybrid a many-dimensional modal logic (later on we
shall see that this name is not merely a nice metaphor).
The algorithmic properties of such many-dimensional hybrids that
appeared more or less independently and with different motivations in
computer science, artificial intelligence, algebraic logic, and modal
logic, turn out to be quite different from those of their well-known
and well-behaved one-dimensional components. In particular, the
complexity of decision algorithms may increase dramatically, even up
to undecidability; two fairly simple finitely axiomatizable systems
may give rise to a hybrid which is not even recursively enumerable,
etc.
To study the computational behavior of many-dimensional modal logics is
the main aim of this book. More precisely, as suggested by its title,
our aim is twofold. On the one hand, we are concerned with providing a
solid mathematical foundation for the discipline characterized in
(Blackburn et. al. 2001) as
... a branch of modal logic dealing with special
relational structures in which the states, rather than being
abstract entities, have some inner structure. More specifically,
these states are tuples or sequences over some base set ...
Furthermore, the accessibility relations between these states are
(partly) determined by this inner structure of the states.
On the other hand, we show that many seemingly different applied
many-dimensional systems (e.g., multi-agent systems, description
logics with epistemic, temporal and dynamic operators, spatio-temporal
logics, (fragments of) first-order temporal or epistemic logics, etc.)
fit in perfectly with this theoretical framework, and so their
computational behavior can be analyzed using the developed machinery.
Thus, we contribute to filling in the gap between the mathematical
theory of modal logic and applications in computer science and
artificial intelligence, which were developing in parallel, often
independently of each other (witness description logics created in the
field of knowledge representation and proved to be terminological
variants of well-known modal logics). This gap is clearly reflected in
the existing literature. Take, for example, two recent books:
(Fagin et. al. 1995) is an excellent exposition of applied epistemic
logic, but it avoids difficult proofs, say, the complexity results are
only formulated; the first monograph on multi-dimensional modal logics
(Marx and Venema 1997), on the contrary, considers mostly mathematical
aspects of modal systems originating in algebraic logic.
This book also reflects a new direction in applied logic in
general and in modal logic in particular that has become apparent
in the last few years: we mean the direction towards constructing
and investigating complex combined systems out of relatively
simple ones. It has manifested itself in a number of international
conferences (e.g., 'Frontiers of Combining Systems' FroCoS'96-FroCoS'02)
and subsequent volumes (Baader and Schulz 1996, de Rijke and Gabbay 2000,
Kirchner and Ringeissen 2000, Armando 2002), special issues of Notre Dame
Journal of Formal Logic (de Rijke and Blackburn 1996) and Studia Logica
(Gabbay and Pirri 1997, Kurucz et. al. 2002), and the monograph (Gabbay
1999).
Complex logical systems and knowledge representation formalisms
present many challenging problems for investigation. In this book we
concentrate on three of them that are regarded as fundamental in both
mathematical logic and theoretical computer science. These are:
- The DECISION PROBLEM, i.e., to find out whether there exists an
algorithm that is capable of deciding a given reasoning task (say,
satisfiability or entailment) for a logic.
- The COMPLEXITY PROBLEM, i.e., to find lower and upper bounds for the
computational complexity of a possible algorithmic solution to the
decision problem.
- The AXIOMATIZATION PROBLEM, i.e., to give an effective (preferably
finite) syntactical characterization of a semantically defined logic, or
to provide an adequate semantics for a syntactically defined one.
The first two problems are concerned with effectiveness (or
programmability) and efficiency (or fast programmability) of
logical systems, which make them fundamental in artificial intelligence
and other practical fields of computer science as well. The third
problem is connected with the proof-theoretic approach: it can be
understood as describing the most essential features of a logic starting
from which all others are derivable. Thus, the axiomatization problem
underpins possible implementations of decision procedures.
The direct practical use of decidability, complexity and
axiomatizability results may be not that obvious.
'Negative' results, say undecidability, are clearly useful: they warn
us not to waste time with implementing this or that 'decision'
algorithm. These results lead to a new research programme: (1) to
find semi-decision (i.e., sound but incomplete) procedures, (2) to
search for decidable fragments of the logic in question, (3) to modify
the logic by making it decidable, etc. Similarly, a result
establishing a high computational complexity or non-axiomatizability
may force the researcher to devise another language to model her
application domain.
On the other hand, a positive decidability result does not yet
guarantee that trying to implement a decision procedure is not a waste
of time: after all the British Museum algorithm is also a decision
procedure. It may seem that the only use of a positive solution to the
decision problem is the conclusion that it is not provable (with the
existing concepts in recursion and complexity theory) that
implementing a decision procedure is hopeless. (Even this
cautious claim may appear too strong. Here, for example, is a
citation from (Johnson 1990): 'Even those unimpressed with the
difficulty of problems in 2- or 3-EXPTIME will have to admit that if
a problem is decidable but not in ELEMENTARY, it might as well not
be decidable at all.' So, according to Johnson, there are concepts
in complexity theory which allow us to classify certain decidable
problems as 'non-implementable' ones. We do not agree with this for
the simple reason that a non-elementary problem may be solvable in
polynomial time in all practical cases. For certain highly
complex problems a useful and complete decision algorithm may
exist; see e.g. (Horrocks et. al. 1999, Hustadt and Schmidt 2000). Klarlund
et. al. (2000), writing about the prover MONA in monadic second-order logic,
observe that 'perhaps surprisingly, this [NONELEMENTARY] complexity also
contributes to successful applications, since it is provably linked to the
succinctness of the logic.') This interpretation of decidability
results can hardly justify spending an enormous amount of energy for
obtaining them.
Actually, it is not only the result itself, not only the first 'sanity
check' of the system, not only an indication of how to implement a
decision procedure that motivates the researcher, but also a deep
insight into properties of the logical system that can be extracted
from decidability and axiomatizability proofs. (That is
why decidability results obtained by means of embeddings into
extremely expressive formalisms (like monadic second-order logics
S1S or SomegaS) may appear somewhat disappointing.) It is the
proof of a complexity result that provides the researcher with
insights into the sources of high computational costs and can be used
to guide the search for more efficient languages-see (Gurevich 1990,
1995) for a similar position. To conclude this discussion: we believe that
the decidability, complexity, and axiomatizability theorems we present in
this book are of interest mainly because their proofs provide a better
understanding of the logical formalisms we consider and, at the same time,
are often useful for the design of practical procedures (to a certain
extent, this is illustrated in Chapter 15 which presents tableau calculi
for modal description logics).
The book is organized in the following way. Part I may serve as an
easy introduction to modal logic and its applications. Chapters 1
and 2 introduce the basic modal logics we deal with, explain their
roots, motivations, syntax, semantics and application fields. At
the end of Chapter 2 we show useful `semantical level' reductions
between many of these logics. In Chapter 3, we consider a number
of many-dimensional systems constructed in logic, artificial
intelligence and computer science, and establish connections
between the various formalisms.
Part II is the technical core of the book. Here we develop a
mathematical theory for handling a spectrum of 'abstract' combinations
of modal logics, ranging from fusions (known also as independent joins
or dovetailings), in which the modal operators of different components
do not interact at all, to products of modal logics, where such an
interaction is rather strong. The ideas, tools and techniques
developed in Part II as well as the obtained results will be used in
the subsequent two parts to investigate the computational behavior of
first-order modal and temporal logics and some combined knowledge
representation formalisms.
In Part III we consider first-order modal and temporal logics in the
two-dimensional perspective. It has been known since the 1960s that it
is extremely hard to deal with these logics (and that they can be very
important for applications). But in contrast to classical predicate
logic, where the early undecidability results of Turing and Church
stimulated research and led to a rich and profound theory concerned
with classifying fragments of first-order logic according to their
decidability (see, e.g., Borger et. al. 1997), there were no serious
attempts to convert the 'negative' results in first-order modal and
temporal logic into a classification problem. Apparently, the
extremely weak expressive power of the modal and temporal formulas
required to prove undecidability left no hope that any useful
decidable fragments located `between' propositional and first-order
modal and temporal logics could ever be found. However, the studies of
many-dimensional propositional modal logics have brought a new insight
into the first-order case. In Part III we present a number of recent
results concerning decidable and axiomatizable fragments of various
first-order modal and temporal logics, and try to draw a borderline
between 'the decidable' and 'the undecidable.'
Part IV applies the developed techniques and obtained results to
analyze the computational behavior of three kinds of knowledge
representation formalisms: temporal epistemic logics, description
logics with modal and temporal operators, and spatio-temporal
logics. In particular, we show how the method of quasimodels,
developed for proving decidability, can be used for devising
tableau decision procedures for some of these logics.
The genre of the book can be defined as a research monograph. It brings
the reader to the front line of current research in the field by
showing both recent achievements and directions of future investigations
(in particular, multiple open problems). On the other hand, well-known
results from modal and first-order logic are formulated without proofs
and supplied with references to accessible sources.
The intended audience of this book is primarily those researchers who
use logic in computer science and artificial intelligence. More
specific areas are, e.g., knowledge representation and reasoning, in
particular, terminological, temporal and spatial reasoning, or reasoning
about agents. For 'pure' logicians Parts II and III may be of chief
interest. Logicians looking for possible applications may find some
useful ideas in Parts I and IV. And we also believe that researchers
from certain other disciplines, say, temporal and spatial databases or
geographical information systems, will benefit from this book as well.
We conclude this preface by putting the subject of the book
into a more general perspective of ongoing and future research. As we
have said above, many-dimensional modal logics are just one example of
'combined logical systems.' And even within this smaller area there
may be different ways of constructing complex logics out of relatively
simple ones. Our approach is basically semantical: given two (or more)
classes of 'one-dimensional' Kripke frames characterizing logics
Li, we construct a class of two- (or higher-) dimensional Kripke
structures reflecting some desirable features of the target
combination of the Li, and then investigate the logic determined by
this class. However, logics do not always come equipped with their
Kripke semantics. They may be given by some kind of algebraic
structures or purely syntactically, as Hilbert-, Gentzen-, tableau-,
resolution-, etc. style calculi. Thus, we need a spectrum of
methodologies providing us with means of combining homogeneously
given logics (say, tableau systems) and perhaps meta-methodologies for
combining methodologies. These challenging problems are far beyond the
scope of this book; many of them are still open for investigation.
ACKNOWLEDGMENTS: We are indebted to our friends and colleagues Ian
Hodkinson, Robin Hirsch, Carsten Lutz, Roman Kontchakov and Valentin
Shehtman who not only helped us with numerous comments, but also
supplied us with some material for this book. Thanks are also due to
Alessandro Artale, Franz Baader, Brandon Bennett, Alexander Chagrov,
Anthony Cohn, Stephane Demri, Ulle Endriss, Jim Farrugia, Enrico
Franconi, David Gabelaia, Maarten Marx, Szabolcs Mikulas, Milenko
Mosurovich, Alexander Rabinovich, Mark Reynolds, Aleksey Romanov,
Holger Sturm, Yde Venema, and Rostislav Yavorski for stimulating
discussions and remarks on the preliminary versions of the book.
In different periods, the work on the book was supported by UK EPSRC
grants no. GR/L85978, GR/M36748 GR/N23028/01, GR/R45369/01 and
GR/R42474/01, by Hungarian National Foundation for Scientific Research
grants no. T30314 and 035192, by the DFG-grants Wo 583/3-1, Wo
583/3-3, and by grant no. 99-01-00968 from the Russian Foundation for
Basic Research.
D. Gabbay
A. Kurucz
King's College London
F. Wolter
University of Liverpool
M. Zakharyaschev
King's College London
REFERENCES:
Armando 2002. A.Armando, editor. Frontiers of Combining Systems IV,
volume 2309 of Lecture Notes in Artificial Intelligence. Springer, 2002.
Baader and Schulz 1996. F.Baader and K.Schulz, editors. Frontiers of
Combining Systems. Kluwer Academic Publishers, 1996.
Blackburn et. al. 2001. P.Blackburn, M.de Rijke, and Y.Venema. Modal Logic.
Cambridge University Press, 2001.
Borger et. al. 1997. E.Borger, E.Graedel, and Yu. Gurevich. The Classical
Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
Fagin et. al. 1995. R.Fagin, J.Halpern, Y.Moses, and M.Vardi. Reasoning
about Knowledge. MIT Press, 1995.
Gabbay 1999. D.Gabbay. Fibring Logics, volume 38 of Oxford Logic Guides.
Clarendon Press, Oxford, 1999.
Gabbay and Pirri 1997. D.Gabbay and F.Pirri, editors. Studia Logica,
volume 59 (1,2), 1997. Special Issue on Combining Logics.
Horrocks et. al. 1999. I.Horrocks, U.Sattler, and S.Tobies. Practical
reasoning for expressive description logics. In H.Ganzinger, D.McAllester,
and A.Voronkov, editors, Proceedings of the 6th International Conference on
Logic for Programming and Automated Reasoning (LPAR'99), volume 1705 of
Lecture Notes in Artificial Intelligence, pages 161-180. Springer, 1999.
Gurevich 1990. Yu. Gurevich. On the classical decision problem. The
Bulletin of EATCS, 42:140-150, 1990.
Gurevich 1995. Yu. Gurevich. The value, if any, of decidability. The
Bulletin of EATCS, 55:129-135, 1995.
Hustadt and Schmidt 2000. U.Hustadt and R.Schmidt. MSPASS: modal reasoning
by translation and first-order resolution. In D.Dyckhoff, editor,
Proceedings of TABLEAUX 2000, volume 1847 of Lecture Notes in Artificial
Intelligence, pages 67-71. Springer, 2000.
Johnson 1990. D.Johnson. A catalog of complexity classes. In J.van Leeuwen,
editor, Handbook of Theoretical Computer Science. Elsevier, North-Holland,
1990.
Kirchner and Ringeissen 2000. H.Kirchner and C.Ringeissen, editors.
Frontiers of Combining Systems III, volume 1794 of Lecture Notes in
Artificial Intelligence. Springer, 2000.
Klarlund et. al. 2002. N.Klarlund, A.Moller, and M.Schwartzbach. MONA
implementation secrets. International Journal of Foundations of Computer
Science, 13:571-586, 2002.
Kurucz et. al. 2002. A.Kurucz, F.Wolter, and M.Zakharyaschev, editors.
Studia Logica, volume 72, 2002. Special Issue on Many-Dimensional Logical
Systems.
Marx and Venema 1997. M.Marx and Y.Venema. Multi-Dimensional Modal Logic.
Kluwer Academic Publishers, 1997.
de Rijke and Blackburn 1996. M.de Rijke and P.Blackburn, editors. Notre
Dame Journal of Formal Logic, volume 37(2), 1996. Special Issue on
Combining Logics.
de Rijke and Gabbay 2000. M.de Rijke and D.Gabbay, editors. Frontiers of
Combining Systems II. Research Studies Press, England, 2000.
|
|
| |
| | |
|
|
| |
