Combinations of Modal Logics.
There is increasing use of combinations of modal logics in both foundational and applied research areas. This article provides an introduction to both the principles of such combinations and to the variety of techniques that have been developed for them. In addition, the article outlines many key research problems yet to be tackled within this callenging area of work.
Introduction
Combining logics for modelling purposes has become a rapidly expanding enterprise that
is inspired mainly by concerns about modularity and the wish to join together different
kinds of information. As any interesting real world system is a complex, composite entity,
decomposing its descriptive requirements (for design, verification, or maintenance pur-
poses) into simpler, more restricted, reasoning tasks is not only appealing but is often the
only plausible way forward. It would be an exaggeration to claim that we currently have a
thorough understanding of 'combined methods.' However, a core body of notions, questions
and results has emerged for an important class of combined logics, and we are beginning to
understand how this core theory behaves when it is applied outside this particular class.
In this paper we will consider the combination of modal (including temporal) logics,
identifying leading edge research that we, and others, have carried out. Such combined
systems have a wide variety of applications that we will describe, but also have significant
problems, often concerning interactions that occur between the separate modal
dimensions. However, we begin by reviewing why we might want to use modal logics at
all.
z Corresponding author. Current address: Department of Computer Science, University of Liverpool,
Liverpool L69 7ZF, UK.
This document was developed from a panel session in the 1999 UK Automated Reasoning Workshop,
which was held as part of the AISB symposium in Edinburgh. All the authors were panelists, except for
Michael Fisher who chaired the panel and edited this document.
c
2000 Kluwer Academic Publishers. Printed in the Netherlands.
2. Why Use Modal Logics?
2.1. MOTIVATION
Over the past decades our perception of computers and computer programs has changed
several times in quite dramatic ways, with consequences reaching far into our societies.
With the rise of the personal computer we began to view the computer as an extension of
our office desks and computer programs replaced traditional office tools such as typewrit-
ers, calculators, and filling cabinets with word processors, spreadsheets, and databases.
Now, the advent of the electronic information age changes our view again: Computers and
their programs turn into ubiquitous digital assistants (or digital agents). Digital agents
have become necessary due to the vast extent and scattered nature of the information
landscape. In addition, today's average computer user is neither able nor willing to learn
how to navigate through the information landscape with the help of more traditional tools.
Digital agents have now become possible for almost the same reason. For the first time
there is sufficient free information and a sufficient number of services available which can
be accessed and manipulated by a computer program without direct intervention by the
human computer user.
Like the personal computer, digital agents will have a substantial impact on our econ-
omy. But do they also have an impact on research in computer science? One should note
that computer hardware design is still generally based on the von Neumann architecture
and that computer programs are still Turing-machine equivalent. However, are techniques
and results already available in computer science research that could have an impact on
the way digital agents (both current and future) are developed and implemented?
Modal logics (Chellas, 1980) or, more precisely, combinations of modal logics, are good
candidates for a formal theory that can be helpful for the specification, development, and
even the execution of digital agents. Modal logics can be used for modelling both digital
agents and (aspects of) their human users. A digital agent should have an understanding
of its own abilities, knowledge, and beliefs. It should also have a representation of the
knowledge, beliefs, and goals of its user and of other digital agents with whom it might
have to cooperate in order to achieve its goals.
Modal logics seem to be perfectly suited as a representation formalism in this setting.
However, there are also some obstacles for the use of the well-studied propositional modal
logics:
propositional logic is often insufficient for more complex real world situations - a
first-order, or even higher-order, language might be necessary;
a monotonic logic might not be sufficient - in many situations our knowledge about
the world is incomplete and much of our knowledge is actually only a default or only
holds with a certain probability; hence, to come to useful conclusions we might have
to rely on a nonmonotonic or probabilistic logic.
Thus, an appropriate representation formalism for digital agents may use combinations of
(propositional or first-order) modal logics.
2.2. REPRESENTING AGENTS
Agent-based systems are a rapidly growing area of interest, in both industry and academia,
(Wooldridge and Jennings, 1995). In particular, the characterisation of complex distributed
components as intelligent or rational agents allows the system designer to analyse applications
at a much higher level of abstraction. In order to reason about such agents, a
number of theories of rational agency have been developed, such as the BDI (Rao and
Georgeff, 1991) and KARO (van Linder et al., 1996) frameworks. These frameworks are
usually represented as combined modal logics. In addition to their use in agent theories,
where the basic representation of agency and rationality is explored, these logics form
the basis for agent-based formal methods. The leading agent theories and formal methods
generally share similar logical properties. In particular, the logics used have:
an informational component, such as being able to represent an agent's beliefs or
knowledge,
a dynamic component, allowing the representation of dynamic activity, and,
a motivational component, often representing the agents desires, intentions or goals.
These aspects are typically represented as follows:
Information - modal logic of belief (KD45) or knowledge (S5);
Dynamism - temporal or dynamic logic;
Motivation - modal logic of intention (KD) or desire (KD).
Thus, the predominant approaches use relevant combinations. For example: Moore (Moore,
combines propositional dynamic logic and a modal logic of knowledge (S5); the BDI
framework (Rao and Georgeff, 1991; Rao, 1995) uses linear or branching temporal logic,
together with modal logics of belief (KD45) or knowledge (S5) , desire (KD), and intention
Halpern et al. (Halpern and Vardi, 1989; Fagin et al., 1996) use linear and
branching-time temporal logics combined with a multi-modal (S5) logic of knowledge; and
the KARO framework (van Linder et al., 1996; van der Hoek et al., 1997) uses propositional
dynamic logic, together with modal logics of belief (KD45) and wishes (KD).
If we assume that combinations of modal logics play an important part in modelling
digital agents, it is an obvious step to consider the question whether we are able to verify
specified requirements or properties of an agent using formal methods. Unfortunately,
many of these combinations, particularly those using dynamic logic, become too complex
(not only undecidable, but incomplete) to use in practical situations. Thus, much
current research activity concerning agent theories centres around developing simpler
combinations of logics that can express many of the same properties as the more complex
combinations, yet are simpler to mechanise. For example, some of our work in this area
has involved developing a simpler logical basis for BDI-like agents (Fisher, 1997b).
2.3. SPATIAL LOGICS
While the traditional uses of modal logics are for representing interacting propositional
attitudes such as belief, knowledge, intention, etc., recent work has investigated the representation
of spatial information in combined modal logics. For example, in (Bennett,
1996; Bennett, 1997), Bennett uses the topological interpretation of the S4 modality as an
interior operator, in combination with an S5 modality in order to encode a large class of
topological relations.
2.4. DESCRIPTION LOGICS
Although not originally characterised in this way, one of the most successful uses of combinations
of modal logics has been the development of expressive Description Logics (Sat-
tler, 1996; De Giacomo and Massacci, 1996; Horrocks, 1998b). Description logics have
found many practical applications, for example in reasoning about database schemata
and queries (Calvanese et al., 1998a; Calvanese et al., 1998b). Since description logics
have been shown to correspond directly to certain combinations of modal logics, such
combinations are also useful.
The application concerning schema and query reasoning that was described above is
very promising, as are ontological engineering applications (Rector et al., 1997; Baker
et al., 1998). In this, and other, contexts description logics that combine transitive, non-transitive
and inverse roles (Horrocks and Sattler, 2000) have proved particularly useful
as they enable many common conceptual data modelling formalisms (including Entity-Relationship
models) to be captured while still allowing for empirically tractable implementations
(Horrocks, 2000).
Another successful combination of modal logics within a description logic framework is
motivated by the attempt to add a temporal dimension to the knowledge representation
language (Artale and Franconi, 2000; Artale and Franconi, 2001). Typical applications of
such temporally extended description logics have been the representation of actions and
plans in Artificial Intelligence (Artale and Franconi, 1998; Artale and Franconi, 1999a),
and reasoning with conceptual models of (federated) temporal databases (Artale and Fran-
coni, 1999b). A temporal description logic can be obtained by combining the description
logic with a standard point-based tense logic (Schild, 1993; Wolter and Zakharyaschev,
1998) or with a variant of the HS interval-based propositional temporal logic (Halpern
and Shoham, 1991).
Given that combinations of modal logics have a number of real and potential uses, it is
important to remember the general technical problems that can occur with such combina-
tions; this we do in the next section.
3. Problems with Combinations
and L 2
be two logics - typically, these are special purpose logics with limited
expressive power, as it often does not make sense to put together logics with universal
expressive power. Let P be a property that logics may have, say decidability, or axiomatic
completeness. The transfer problem is this: if L 1
and L 2
enjoy the property P, does their
combination
have P as well? Transfer problems belong to the main mathematical
questions that logicians have been concerned with in the area of combining logics.
When, and for which properties, do we have transfer or failure of transfer? As a rule of
thumb, in the absence of interaction between the component logics, we do have
here, absence of interaction means that the component languages do not share any sym-
bols, except maybe the booleans and atomic symbols (we will say more about interactions
in Section 5). Properties that do transfer in this restricted case include the finite model
property, decidability, and (under suitable restrictions on the classes of models and the
complexity class) complexity upper bounds.
The positive proofs in the area are usually based on two key intuitions: divide and
conquer and hide and unpack. That is: try to split problems and delegate sub-problems to
the component logics; and when working inside one of the component logics view information
relating to other component logics as alien information and 'hide' it - don't unpack
the hidden information until we have reduced a given problem to a sub-problem in the
relevant component logic. Neither of these key intuitions continues to work in the presence
of interaction. For instance, consider two modal languages L 1
and L 2
with modal operators
and , respectively; there are logics L 1 and L 2 in L 1 and L 2 whose satisfiability problem
is in NP, while the satisfiability problem for the combined language plus the interaction
principle
4. Reasoning Methods
So, we have seen that combinations of modal logics are, or at least have the potential
to be, very useful. However, we must also be careful in combining such logics. In all the
application areas discussed in Section 2, the notion of proof is important. In agent theories,
for example, a proof allows us to examine properties of the overall theory and, in some
cases, to characterise computation within that theory. In agent-based formal methods, a
proof is clearly important in developing verification techniques.
But how do we go about developing proof techniques for combined logics? Since there are
a wide variety of reasoning systems for individual modal logics, it is natural to ask: "does
combining work for actual reasoning systems?", i.e., can existing tools for each component
logic be put together to obtain tools for combined logics? Obviously, the re-use of tools and
procedures is one of the key motivations underlying the field.
Unfortunately, one cannot put together proof procedures for two logics in a uniform way.
First, 'proving' can have different meanings in different logics: (semi-)deciding satisfiability
or validity, computing an instantiation, or generating a model. Second, it is not clear
where to "plug in" the proof procedure for a logic L 1
into that for a second logic L 2
; a proof
procedure may have different notions of valuations, or of proof goals.
So what can one do? One way out is to impose special conditions on the calculi that
one wants to combine (Beckert and Gabbay, 1998). Another possibility, in the case of
modal logics, is to use a translation-based approach to theorem proving, by mapping all
component logics into a common background logic (see below).
There are quite a few successful particular instances of combined logics where we have
no problems whatsoever in putting together tools; see (Aiello et al., 1999; Kurtonina and
de Rijke, 2000). By and large, however, we don't have a good understanding of how to
proceed. Further experiments are needed, both locally, and network based, so that at some
stage we will be able to plug together tools without having to be the designer or engineer
of the systems.
In the following sections we will consider the work that we are involved with concerning
the development of proof techniques for combined logics.
4.1. TABLEAUX BASED REASONING
Most commonly, reasoning methods for modal logics are presented as tableau-style proce-
dures. These semantically-based approaches are well suited to implementing proof procedures
for interacting modalities because the usually explicit presence of models in the
data-structures used by the algorithm helps the system to represent the interactions
between modalities. Thus, tableaux systems have the advantages that:
they have a (fairly) direct and intuitively obvious relationship with the Kripke structures
of the underlying logic;
algorithms are easy to design and extend;
the simplicity of the algorithms facilitates optimised implementation.
We have developed a range of tableaux-based systems for description logics, for example
(Horrocks, 1998a; Horrocks, 2000), and for combinations of linear-time temporal logic
with modal logics S5 or KD45 (Wooldridge et al., 1998).
4.2. RESOLUTION BASED REASONING
An alternative approach to reasoning in combined modal logics is to use direct resolution
techniques which should, in the long term have at least the performance of corresponding
tableaux-based systems.
Our work in this area has focused on extending the resolution methods developed for
linear-time temporal logics (Fisher, 1991; Fisher et al., 2001) to particular combinations
of the logics considered above. This clausal resolution method centres round three main
steps:
translation to a simple normal form (involving renaming of complex subformulae and
reduction to a core set of operators);
classical resolution between formulae that occur at the same moment in time; and
resolution between sets of formula that make  always true with constraints that
ensure  is false at some point in the future.
In (Dixon et al., 1998), we extended this method to linear-time temporal logic combined
with S5 modal logic. During translation to the normal form, temporal formulae are separated
out from modal (using renaming). Reasoning in the temporal and modal
components is then carried out separately and information is transferred between the two
components via classical propositional logic.
Other important direct resolution methods for modal logics include (Mints, 1990) (on
which the above approach was based) and our work on prefixed resolution (Areces et al.,
1999).
4.3. TRANSLATION BASED REASONING
Translation between different formal languages and different problem classes is one of the
most fundamental principles in computer science. For example, a compiler for a programming
language is just (the implementation of) a translation from one formal language into
another formal language. In the case of logical reasoning, such a translation approach is
based on the idea that given a (sound, complete, and possibly terminating) theorem prover
for a logic L 2 , inference in a logic L 1 can be carried out by translating formulae of L 1 into
. There are minimal requirements imposed on the translation from L 1
into
namely
that the translation preserves satisfiability equivalence and that it can be computed in
polynomial time.
In the case of modal logics, the most straightforward translation mapping, the relational
translation, is based on the Kripke semantics of modal logics (van Benthem, 1976). But
just as there are many compilers for a single programming language, there are a number
of alternative translation mappings from modal logics into subclasses of first order logic
which satisfy the mentioned minimal requirements. These include the functional translation
(Auffray and Enjalbert, 1992; Fari -
nas del Cerro and Herzig, 1988; Ohlbach, 1991)
the optimised functional translation (Ohlbach and Schmidt, 1997; Schmidt, 1997), and the
semi-functional translation (Nonnengart, 1995).
The advantages of the translation approach include the following. First, by enabling the
use of a variety of first-order and propositional theorem provers the translation approach
provides access to efficient, reliable and general methods of modal theorem proving. Sec-
ond, decision procedures can be obtained by suitably instantiating parameters in existing
theorem proving frameworks (Bachmair and Ganzinger, 1997). For the optimised functional
translation this has been demonstrated in (Schmidt, 1997; Schmidt, 1999), while
the relational and semi-functional translation have been considered in (Ganzinger et al.,
1999a; Hustadt, 1999; Hustadt and Schmidt, 1999b; Hustadt and Schmidt, 1998). Third,
there are general guidelines for choosing these parameters in the right way to enforce
termination and the hard part is to prove that termination is guaranteed.
The most common approach uses ordering refinements of resolution to ensure termi-
nation. Ordering refinements are very natural as they provide decision procedures for a
wide range of solvable first-order fragments
uller et al., 2000; Hustadt and Schmidt,
1999a).
An interesting alternative is selection refinements (Hustadt and Schmidt, 1998). Selection
refinements are closely related to hyper-resolution, a well-known and commonly used
refinement in first-order theorem provers. It can be shown that selection refinements plus
splitting are able to polynomially simulate proof search in standard tableaux calculi for
modal logic (Hustadt and Schmidt, 1999b; Hustadt and Schmidt, 2000). Another alternative
is based on the fact that the optimised functional translation can be used to translate
modal into a subclass of the Bernays-Sch- onfinkel class (Schmidt, 1997). The
number of ground instances of clauses obtained from formulae of the Bernays-Sch- onfinkel
class is always finite. Thus, it is possible to use propositional decision procedures to test
the satisfiability of the sets of ground clauses in this way.
While there are a number of other promising approaches, for example the use of equational
methods (e.g. rewriting), based on the algebraic interpretation of modal logics, or
constraint satisfaction techniques, it seems likely that many of the techniques developed
will share a broad similarity (Hustadt and Schmidt, 2000). In this sense, there are few
reasoning methods that are "inappropriate" (Ohlbach et al., 2000).
5. Interactions
Once we combine modal (and temporal) logics, we must decide whether we are going to
support interactions between the modal dimensions. Although there may be some cases of
combined modal logics without interactions that can be useful, to exploit the full power
of this combination technique, interactions must be handled. For example, interactions
typically involve commutative modalities - i.e., pairs of modalities,  and  satisfying
the schema
But this apparently simple schema is surprisingly hard to incorporate into modal reasoning
algorithms. Indeed, (Kracht, 1995) has shown that the logic containing three S5
modalities, each pair of which commutes, is undecidable, while it is well-known that S5
itself is NP-complete. See Section 8 later for further discussion of decidability issues.
In the following, we will re-examine some of the approaches considered in Section 4,
particularly concerning how they cope with such interactions.
5.1. DESCRIPTION LOGICS
In the context of description logics, interactions between different kinds of role (modality)
are an inherent and essential part of the work on expressive description logics. We can
think of basic description logics as a syntactic variant of the normal multi-modal logic K,
or even of a propositional dynamic logic. More expressive description logics are obtained
by adding new roles with specific properties - for example they may be transitive or
functional (deterministic); in this case, there is no interaction between modalities in the
combined logic. However, the interesting cases are when converse modalities, or implications
between modalities, e.g.,  ! , are introduced. The latter axiom schema in
a basic description logic combined with multi-modal S4 is important since it allows us to
encode the universal modality. As there are no description logics in which interactions such
as  $  are required, the above approach leads to practical reasoning systems for
quite complex description logics.
In the context of temporal description logics, interactions between temporal and non-temporal
modalities are usually bad. For example, the ability to define a global role - i.e.,
invariant over time - makes the logic undecidable. However, we have identified a special
case, still very useful in practice, where the combination of a basic description logic with a
temporal component is decidable (Artale and Franconi, 1998).
5.2. TEMPORAL LOGICS OF KNOWLEDGE
Particular interactions between temporal logics and modal logics of knowledge (S5) have
been analysed in (Halpern and Vardi, 1986; Halpern and Vardi, 1988b; Halpern and Vardi,
1988a; Halpern and Vardi, 1989). Notions such as perfect recall, no learning, unique initial
state and synchrony are defined. The basic temporal logics of knowledge are then restricted
to those where certain of the above notions hold. Fagin et al. (Fagin et al., 1996) consider
the complexity of the validity problem of these logics for one or more agents, linear or
branching-time temporal logic and with or without common knowledge. In general, the
complexity of the validity problem is higher where interactions are involved, with some
combinations of interactions leading to undecidability.
In (Dixon and Fisher, 2000), we consider resolution systems with synchrony and perfect
recall by adding extra clauses to the clause-set to account for the application of the
synchrony and perfect recall axiom to particular clauses. The former can be axiomatised
by the axioms of linear-time temporal logic, plus the axioms of the modal logic S5 (rep-
resented by the modal operator 'K') with the additional interaction axiom (Halpern and
Vardi, 1988b; Halpern et. al., 2000),
meaning informally that if an agent knows that in the next moment  will hold then in
the next moment the agent will know that  holds. Essentially, in systems with perfect
recall, the number of timelines (or possible futures) that an agent considers possible stays
the same or decreases over time. The axiom for synchrony and no learning is the converse
of the above axiom.
We are also interested in looking at what interactions are actually used in application
areas. For example the interaction (where [do i ()] is effectively a dynamic logic operator)
meaning informally if agent i knows that doing action  results in  then agent i doing
the action  results in agent i knowing , has been highlighted as desirable for the KARO
framework (van der Hoek et al., 1997). This is very similar to the synchrony and perfect
recall axiom noted above.
5.3. TRANSLATION
From the view of the translation approach, interactions between logics in some combination
of modal logics are no different from the more traditional axiom schemata which are
usually provided to characterise extensions of the basic modal logic K, for example, the
modal logics KD, S4 and S5. To accommodate these axiom schemata in the translation approach
we have to find a satisfiability equivalence preserving first-order characterisation
for them.
For example, consider a combination of two basic modal logics with modal operators
and . A very simple interaction between the two modal logics is given by the axiom
schema
Using the relational translation approach with predicate symbols R and R corresponding
to the accessibility relation for each logic, axiom schema (1) can be characterised by
the first-order formula
In some cases, the first-order formulae characterising interactions are already covered by
existing decidability results for subclasses of first-order logic corresponding to the modal
logics. For example, formula (2) belongs to the Skolem class, the class of DL-clauses
uller
et al., 2000), and various other classes. In these cases the translation approach provides us
with sound, complete, and terminating decision procedures for combinations of interacting
modal logics without any additional effort.
It is even possible to obtain general characterisations of the boundaries of decidability of
combinations of interacting modal logics in this way. For example, results from (Ganzinger
et al., 1999b) imply that if we have two modal logics which satisfy the 4 axiom, that is the
accessibility relations are transitive, and the modal logics are interacting, for example, by
the axiom schema (1), then the combined logic is undecidable.
6. General Frameworks
The considerations of previous sections were intended to highlight some of the potentials
of a representational framework based on combinations of modal logics. However, it was
also pointed out that providing such a representational framework together with the accompanying
tools is a non-trivial problem. It is therefore very likely that whatever our
first approach to this problem might be, it will have shortcomings which are too serious
to provide a workable solution. So, research in this direction will proceed by considering
a number of combinations of modal logics and assessing both their appropriateness and
usefulness.
Whether or not a particular combination of modal logics provides a suitable foundation
for a representational framework can only be decided if we are able to make practical
use of it, for example for the purpose of verifying and executing agents. Therefore,
the assessment necessarily requires the availability of implemented theorem provers for
combinations of modal logics.
It is, of course, possible to develop a suitable calculus from scratch, as we described in
Section 4, proving its soundness, completeness, and possibly its termination for the combination
2of logics under consideration, and finally to implement the calculus accompanied
with the required data structures, heuristic functions, and optimisation techniques in a
theorem prover. However, bearing in mind that we have to make this effort for a number
of different combinations of modal logics, it is necessary to find a more general approach.
Thus, we are interested in general principles and a general framework for combining
modal logics.
One approach is to use standard methods for modal logics. There are various levels at
which one could give a generalised account of combinations of modal logics. Semantically,
both the Kripke and Tarski style semantics generalise easily to combined modal systems.
Although algebraic semantics is more general and supports equational and constraint-based
methods, Kripke semantics is better known, more intuitive, and is well-suited to
developing tableau methods. The correspondences between these two semantic approaches
provide different perspectives on the interpretation, each of which has its own advantages;
see (Blackburn et al., 1999) for details on the correspondences.
The proof theory of modal logics was originally developed in terms of axiom schemata
(Hilbert systems). This approach can be applied equally well to combined modal systems.
Axiomatic presentations are concise and the meanings of the axioms are (if not too com-
plex) usually readily understandable. Within such a system, proofs can be carried out
simply by substituting formulae into the axiom schemata and applying the modus ponens
rule. However, these non-analytic rules do not provide practical inference systems. Rule-based
presentations seem to be better suited for the development of inference algorithms,
especially where they are purely analytic.
While the use of a traditional approach might be helpful in certain cases, there is
clearly a need for a framework specifically designed to handle the combination of modal
logics. Examples for such frameworks are fibring (Gabbay, 1999), the translation approach
(see above), and the SNF approach (Dixon et al., 1998). Briefly, the SNF approach involves
extending the normal form (called SNF) developed for representing temporal logics
(Fisher, 1997a) to other modal and temporal logics, such as branching-time temporal
logics (Bolotov and Fisher, 1999), modal logics (Dixon et al., 1998) and even -calculus
formulae (Fisher and Bolotov, 2000). The basic approach is to keep rules (clauses) separate
that deal with different logics, re-use proof rules for the relevant logics and to make sure
enough information is passed between each part (Dixon et al., 1998; Fisher and Ghidini,
1999).
An approach that we have been interested in more recently is itself a combination, namely,
a combination of the SNF and the translation approaches. For example, when combining a
temporal logic with a modal logic, the temporal aspects remain as SNF clauses, while the
modal clauses are translated to classical logic (Hustadt et al., 2000).
7. Tools
Given that combinations of modal logics are often quite complex, what are the prospects for
having practical tools that will allow us to reason about combined modal logics incorporating
One answer is that, for some particular instances of combined modal log-
ics, namely description logics, powerful and efficient systems already exist. Good examples
of these are FaCT (Horrocks, 1998a), iFaCT (Horrocks, 2000) and DLP (Patel-Schneider,
1998).
Implementation effort is also under way to support some of the reasoning methods
described in Section 4, for example clausal resolution based upon the SNF approach. Here,
a resolution based theorem prover for linear-time temporal logics plus S5 modal logic
based on (Dixon et al., 1998) is being developed. This is to be extended with work on
strategies for efficient application, and guidance, of proof rules (Dixon, 1996; Dixon, 1998;
Dixon, 1999) developed for temporal logics in order to help deal with interactions.
However, if combinations of modal logics are to function as practical vehicles for rea-
soning, we are likely to have to face the issues of complexity. There are various complexity
results counting both in favour and against the feasibility of combined modal reasoning. As
we have seen earlier, Kracht (Kracht, 1995) (amongst others) has shown that some simple
combinations of modalities together with very simple interaction axioms yield undecidable
systems; on the positive side, there are a number of examples of quite expressive fragments
of multi-modal languages, whose decision procedures are polynomial, for example (Renz
and Nebel, 1997). Thus, the viability of reasoning with combined modal logics depends
very much on the particular combination of modalities and interaction axioms.
An obvious way of reducing the complexity of a logical language is to restrict its syntax.
We consider such an approach, called layering (Finger and Gabbay, 1992), below.
7.1. LAYERED MODAL LOGICS
A layered modal logic is a special kind of combined modal logic in which restrictions are
placed on the nesting order of the different modalities in the language. A typical layering
restriction would be to require that temporal modalities lie outside the scope of spatial
modalities. This would allow one to represent tensed spatial constraints, but not specify
temporal constraints which vary over space. Whereas tensed spatial relations are very
common in natural language, the latter kind of constraint is not so common.
7.2. EXPRESSIVE POWER OF RESTRICTED FORMALISMS
One might expect that restricting combined modal formalisms to be layered would reduce
their expressive power to the extent that they would lose much of their usefulness. How-
ever, the S5(S4) hybrid described in Section 2.3 is strictly layered (which is one way to
account for its nice computational properties) and is also capable of representing a wide
range of topological relations.
In the case of a spatio-temporal language (as above) one might restrict temporal operators
to lie outside the scope of spatial operators. This would result in an intuitively natural
language of tensed spatial constraints, in which we could, for example, make statements
of the form "x will overlap y" but not of the form "every part of x will at some time satisfy
property ."
8. Decidability Problems
The result by (Ganzinger et al., 1999b) and related results by (Kracht, 1995) show that
undecidability of combinations of modal logics is imminent as soon as we allow interactions
between the logics. Consequently, one of the most attractive features of modal logics is lost
in these cases. Furthermore, one of the important arguments for the effort invested in the
development of tableaux-based theorem provers for modal logics is lost, namely, that they
provide rather straightforward decision procedures while the translation approach does
not ensure termination without the use of the appropriate refinements of resolution.
This raises several questions:
1. Should we concentrate our research on identifying combinations of interacting modal
logics which are still decidable? Or should we abandon the consideration of these
rather simple logics, since we have to expect that most combinations of modal logic
interesting for real-world applications will be undecidable?
2. If we acknowledge that we have to deal with undecidable combinations of modal logics,
does the use of modal logics still make sense? Is there still an advantage compared to
the use of first-order logic or some other logic for the tasks under consideration?
Note that the translation approach partly diminishes the importance of these questions as
far as the development of theorem provers is concerned. Refinements of resolution which
ensure termination on the translation of modal are still sound and complete
calculi for full first-order logic. Thus, in the translation approach we can always fall back
on full first-order logic whenever we have the feeling that combinations of modal logics are
too much of a strait-jacket.
In the work on description logics, the practical use of these formalisms has meant that
retaining decidability is essential. Thus, one of the key aspects of research in this area has
been the extension of expressive power while (just) retaining decidability.
In contrast, in the work on agent theories, there is research attempting to characterise
which interactions do lead to undecidability. For decidable cases, it is important to assess
how useful the interactions are in relevant application areas; if they are of use we can
study decision procedures for these interactions and one of the key strategies here has
been to structure information, and to separate the various reasoning tasks.
Finally, the development of heuristics and strategies to guide the proofs is essential
regardless of decidability as, even if decidable fragments exist, their complexity is likely
to be high if we include interactions.
9.

Summary

Does the idea of combining logics actually offer anything new? Some of the possible objections
can be justified. Logical combination is a relatively new idea: it has not yet been systematically
explored, and there is no established body of results or techniques. Nonethe-
less, there is a growing body of logic-oriented work in the field, and there are explorations
of their uses in AI, computational linguistics, automated deduction, and computer science.
An overly critical reaction seems misguided.
In order to receive more attention from the wider community of researchers interested
in knowledge representation and reasoning, the capabilities of combined modal logics
need to become more accessible; and their superiority over other formalisms (such as the
direct use of first-order logic) needs to be decisively demonstrated for some significant
applications. A survey of the expressive power, computational properties and potential
applications of a large class of combined modal logics would be very useful to AI system
designers.



--R

Spatial Reasoning for Image Retrieval.
Prefixed Resolution: A resolution method for modal and description logics.
A Temporal Description Logic for Reasoning about Actions and Plans.
Representing a Robotic Domain using Temporal Description Logics.
Temporal Entity-Relationship Modeling with Description Logics
A Survey of Temporal Extensions of Description Logics.
Temporal Description Logics.

A theory of resolution.
Transparent access to multiple bioinformatics information sources: an overview.
Fibring semantic tableaux.
Modal logics for qualitative spatial reasoning.
Logical Representations for Automated Reasoning about Spatial Relationships.
Modal Logic.

A Resolution Method for CTL Branching-Time Temporal Logic

Description Logic Framework for Information Integration.
Modal Logic
Tableaux and algorithms for propositional dynamic logic with converse.

Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall.
Resolution for Temporal Logics of Knowledge.
Search Strategies for Resolution in Temporal Logics.
Temporal Resolution using a Breadth-First Search Algorithm
Removing Irrelevant Information in Temporal Resolution Proofs.


Adding a Temporal Dimension to a Logic System.

uk/RESEARCH/LoCo/mures.
Clausal Temporal Resolution.
A Resolution Method for Temporal Logic.
A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution
Implementing BDI-like Systems by Direct Execution
Programming Resource-Bounded Deliberative Agents
Reasoning About Knowledge.
Fibring Logics
A resolution-based decision procedure for extensions of K4
The two-variable guarded fragment with transitive relations
IEEE Computer Society Press
The Complexity of Reasoning about Knowledge and Time: Extended Abstract.

Reasoning about Knowledge and Time in Asynchronous Systems.
The Complexity of Reasoning about Knowledge and Time: Synchronous Systems.
The Complexity of Reasoning about Knowledge and Time.
Journal of Computer and System Sciences
Complete axiomatizations for reasoning about knowledge and time (submitted).
A Propositional Modal Logic of Time Intervals.
Complexity transfer for modal logic.
The FaCT system.
Using an expressive description logic: FaCT or fiction?
FaCT and iFaCT.

Journal of Logic and Computation
Normal Forms and Proofs in Combined Modal and Temporal Logics.
Issues of decidability for description logics in the framework of resolution.
In Automated Deduction in Classical and Non-Classical Logics: Selected Papers
Using resolution for testing modal satisfiability and building models.

Maslov's class K revisited.
On the relation of resolution and tableaux proof systems for description logics.
Hybrid logics and linguistic inference.
Highway to the danger zone.
Simulation and transfer results in modal logic.
Formalising Motivational Attitudes of Agents: On Preferences

A Formal Theory of Knowledge and Action.
A Resolution-Based Calculus For Temporal Logics

Encoding two-valued non-classical logics in classical logic
Functional translation and second-order frame properties of modal logics
Journal of Logic and Computation
DLP system description.
Modeling Agents within a BDI-Architecture
Decision Procedures for Propositional Linear-Time Belief-Desire-Intention Logics
The GRAIL concept modelling language for medical terminology.

A concept language extended with different kinds of transitive roles.
Optimised Modal Translation and Resolution.
Decidability by resolution for propositional modal logics.
Combining Terminological Logics with Tense Logic.
Modal Correspondence Theory.
An integrated modal approach to rational agents.
Technical Report UU-CS-1997-06
Temporalizing Description Logics.
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
Intelligent agents: Theory and practice.

--TR
The complexity of reasoning about knowledge and time
Reasoning about knowledge and time in asynchronous systems
The complexity of reasoning about knowledge and time. I. lower bounds
Gentzen-type systems and resolution rules. Part I. Propositional logic
A propositional modal logic of time intervals
Reasoning about knowledge
On the decidability of query containment under constraints
Modal description logics
Clausal temporal resolution
Temporal resolution using a breadth-first search
A survey of temporal extensions of description logics
Decidability by Resolution for Propositional Modal Logics
Using Resolution for Testing Modal Satisfiability and Building Models
Combining Terminological Logics with Tense Logic
TAMBIS
Programming Resource-Bounded Deliberative Agents
On the Relation of Resolution and Tableaux Proof Systems for Description Logics
Normal Forms and Proofs in Combined Modal and Temporal Logics
Fibring Semantic Tableaux
The FaCT System
Temporal ER Modeling with Description Logics
A Concept Language Extended with Different Kinds of Transitive Roles
Issues of Decidability for Description Logics in the Framework of Resolution
Tableaux and Algorithms for Propositional Dynamic Logic with Converse
Maslov''s Class K Revisited
Prefixed Resolution
Search Strategies for Resolution in Temporal Logics
Encoding two-valued nonclassical logics in classical logic
Resolution decision procedures
The Two-Variable Guarded Fragment with Transitive Relations

--CTR
Daniel Oberle , Steffen Staab , Rudi Studer , Raphael Volz, Supporting application development in the semantic web, ACM Transactions on Internet Technology (TOIT), v.5 n.2, p.328-358, May 2005
Clare Dixon , Michael Fisher , Alexander Bolotov, Clausal resolution in a logic of rational agency, Artificial Intelligence, v.139 n.1, p.47-89, July 2002
modal logics;knowledge representation;logical reasoning