The letters
O, I, and Q
are customary written in various orders, e.g.,
ALCQIO, but SHOIQ.
Here we do not reflect this tradition, but rather use a uniform naming scheme.
In literature, the letter F sometimes stands for
feature (dis)agreement constructor
(), rather than functionality
().
The presence of role intersection operator is sometimes indicated
by the letter R in literature, e.g.
ALCNR := ALCN(∩).
Transitive closure is usually denoted as R+.
The operators * and + are expressible in terms of each other via equalities:
R+ = R o R* and
R* = id(T) ∪ R+.
Note however that the former definition is not linearly bounded.
Therefore, any complexity result for a logic with + immediately implies
the same result for a logic with (*,o), but not vice versa.
In the selector "Allow/forbid complex roles in number restriction",
a role (expression) is called complex if it contains any role operations
other than inversion (i.e. inversion is harmless (with some rare exceptions,
which are pointed out in the comments to those cases)).
However, in literature it is usually hard or even impossible to determine whether
this assumption holds by looking at the name of a logic.
For instance, ALCQIreg usually abbreviates
a logic where only role names and their inverses are allowed in number restrictions; whereas
in the logic ALCN(o),
role composition is allowed in number restrictions.
To avoid this ambiguity, the selector was introduced here explicitly.
In Descripion Logics with unqualified number restrictions
(N), one can independently allow/forbid role operations
in value restrictions (∃R.C and ∀R.C)
and/or in number restrictions (≥nR).
Therefore, strictly speaking, the naming of logics should look like
ALC(∪,–)N(∪,o).
However, in our Navigator we are only able to display logics where role constructors
are either allowed in both value and number restrictions,
or in value restrictions only. What holds for the remaining case (if known)
is usually said in comments.
Note that this distinction is redundant for logics with qualified number
restrictions Q, since ∃R.C
can be expressed as ≥1R.C.
Recall that if C is a complexity class (e.g., PSpace or ExpTime), then a problem Q is said to be
inC if there is an algorithm that belongs to the class C
and solves the problem Q (so this is an upper bound for complexity). In particular, "decidable" is
an upper bound; here C is the class of all decidable problems.
A problem Q is called C-hard if all problems form the class C can be
polynomially reduced to the problem Q (so this is a lower bound;
in particular, the problem Q can be much harder, even undecidable!).
Finally, a problem Q is called C-complete if it is both
C-hard and in C. For more information on
Computational Complexity Theory see [].
The symbol
in the above table means that the author of this web page did not find
in the literature any results concerning the corresponding logic.
If you have any information about that logic, the author would be grateful
if you send
him a mail with a reference. Sometimes, you can find out the desired
complexity result using this tool by adding/removing some ingredients
from the logic you consider, since it is not guaranteed that whenever
this tool knows the complexity of two logics, and these complexities are the same,
then it knows the complexity of all logics in between.
As already pointed out, this tool is always
incomplete
and updated frequently.
Additional sources
Here
is the list of Description Logic reasoners,
together with a description of their capabilities and links to their web page.
Maintained by
Ulrike Sattler.
Here
you will find 6 diagrams depicting the complexity of
concept satisfiability and ABox consistency problems
for logics in between ALC and SHOIQ.
There are some gaps (open problems?) in those diagrams!
Here
you will find a description of how ABox can be eliminated
in presence of nominals (i.e., in extensions of ALCO)
and how TBox can be eliminated in extensions of ALCIO,
SH, and ALC(∪,*).
Proofs are missing (can be found in literature below).
Papers
|
all abstracts
|
long names of conferences
A road-map on complexity for hybrid logics
[ pdf |
]
@inproceedings{ArecesBlMarx1999,
author = {Carlos Areces and Patrick Blackburn and Maarten Marx},
title = {A road-map on complexity for hybrid logics},
pages = {307--321},
editor = {J{\"o}rg Flum and Mario Rodriguez-Artalejo},
booktitle = {Proc.\ of the 13th Int.\ Workshop on Computer Science Logic (CSL 2005),
8th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)},
series = {Lecture Notes in Computer Science},
volume = {1683},
publisher = {Springer},
year = {1999},
doi = {10.1007/3-540-48168-0_22},
ee = {http://dx.doi.org/10.1007/3-540-48168-0_22}
}
Hybrid languages are extended modal languages which can refer to (or even quantify over) states.
Such languages are better behaved proof theoretically than ordinary modal languages for
they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications,
including description logic and temporal reasoning. Thus it would be useful to have a map of their
complexity-theoretic properties, and this paper provides one.
Our work falls into two parts. We first examine the basic hybrid language and its multi-modal
and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages)
are no more complex than ordinary uni-modal logic: all have PSpace-complete K-satisfiability problems.
We then show that adding even one nominal to tense logic raises complexity from PSpace to ExpTime.
In the second part we turn to stronger hybrid languages in which it is possible to bind nominals.
We prove a general expressivity result showing that even the weak form of binding offered
by the ↓ operator easily leads to undecidability.
In
Jörg Flum and
Mario Rodrígues-Artalejo,
editors,
Proc. of
the 8th Annual Conference of the European Association for Computer Science Logic,CSL'99,Madrid, Spain, September 20-25, 1999,LNCS,
vol. 1683,
pp. 307–321,
Springer, 1999.
Augmenting concept languages by transitive closure of roles:
An alternative to terminological cycles
[ pdf |
]
@inproceedings{Baader1991,
author = {Franz Baader},
title = {Augmenting concept languages by transitive closure of roles:
{A}n alternative to terminological cycles},
pages = {446--451},
editor = {John Mylopoulos and Raymond Reiter},
booktitle = {Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI'91)},
publisher = {Morgan Kaufmann},
year = {1991}
}
In Baader (1990, 1990a), we have considered different types of semantics for terminological cycles
in the concept language TLQ which allows only conjunction of concepts and value-restrictions.
It turned out that greatest fixed-point semantics (gfp-semantics) seems to be most appropriate
for cycles in this language. In the present paper we shall show that the concept defining facilities
of FL0 with cyclic definitions and gfp-semantics can also be obtained
in a different way. One may replace cycles by role definitions involving union, composition,
and transitive closure of roles.
This proposes a way of retaining, in an extended language, the pleasant features
of gfp-semantics for FLQ with cyclic definitions without running into
the troubles caused by cycles in larger languages. Starting with the language ALC
of Schmidt-Schauß & Smolka (1988) – which allows negation, conjunction
and disjunction of concepts as well as value-restrictions and exists-in-restrictions –
we shall disallow cyclic concept definitions, but instead shall add the possibility
of role definitions involving union, composition, and transitive closure of roles.
In contrast to other terminological KR-systems which incorporate the transitive closure
operator for roles, we shall be able to give a sound and complete algorithm for concept subsumption.
Expressive number restrictions in Description Logics
[ pdf |
ps.zip |
]
@article{BaaderSattler1999,
author = {Franz Baader and Ulrike Sattler},
title = {Expressive number restrictions in Description Logics},
journal = {Journal of Logic and Computation},
volume = {9},
number = {3},
year = {1999},
pages = {319--350},
doi = {10.1093/logcom/9.3.319},
ee = {http://dx.doi.org/10.1093/logcom/9.3.319}
}
Number restrictions are concept constructors that are available in almost all implemented
Description Logic systems. However, they are mostly available only in a rather weak form,
which considerably restricts their expressive power.
On the one hand, the roles that may occur in number restrictions are usually of a very
restricted type, namely atomic roles or complex roles built using either intersection
or inversion. In the present paper, we increase the expressive power of Description Logics
by allowing for more complex roles in number restrictions. As role constructors,
we consider composition of roles (which will be present in all our logics) and intersection,
union, and inversion of roles in different combinations. We will present two decidability results
(for the basic logic that extends ALC by number restrictions on roles with composition,
and for one extension of this logic), and three undecidability results for three other
extensions of the basic logic.
On the other hand, with the rather weak form of number restrictions available in implemented systems,
the number of role successors of an individual can only be restricted by a fixed non-negative integer.
To overcome this lack of expressiveness, we allow for variables ranging over the non-negative integers
in place of the fixed numbers in number restrictions. The expressive power of this constructor
is increased even further by introducing explicit quantifiers for the numerical variables.
The Description Logic obtained this way turns out to have an undecidable satisfiability problem.
For a restricted logic we show that concept satisfiability is decidable.
Automata can show PSpace results for Description Logics
[ pdf |
]
@article{BaaderHlaPen2008,
author = {Franz Baader and Jan Hladik and Rafael Pe{\~n}aloza},
title = {Automata can show {PSpace} results for Description Logics},
pages = {1045--1056},
journal = {Information and Computation, Special issue: First Int.\ Conf.\ on
Language and Automata Theory and Applications (LATA 2007)},
volume = {206},
number = {9--10},
year = {2008},
doi = {10.1016/j.ic.2008.03.006},
ee = {http://dx.doi.org/10.1016/j.ic.2008.03.006}
}
In the area of Description Logic (DL), both tableau-based and automata-based algorithms
are frequently used to show decidability and complexity results for basic inference problems
such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case
optimal algorithms in the case of PSpace-complete logics, it is often very hard to design optimal
tableau-based algorithms for ExpTime-complete DLs. In contrast, the automata-based approach
is usually well-suited to prove ExpTime upper-bounds, but its direct application will usually
also yield an ExpTime-algorithm for a PSpace-complete logic since the (tree) automaton constructed
for a given concept is usually exponentially large. In the present paper, we formulate conditions
under which an on-the-fly construction of such an exponentially large automaton can be used
to obtain a PSpace-algorithm. We illustrate the usefulness of this approach by proving a new
PSpace upper-bound for satisfiability of concepts with respect to acyclic terminologies
in the DL SI, which extends the basic DL ALC with transitive and inverse roles.
Information and Computation,
Special Issue:
First Int. Conf. on Language and Automata Theory and Applications,LATA 2007,
Tarragona, Spain, March 29 – April 4, 2007,
206(9-10):1045-1056, 2008.
PSpace automata with blocking for Description Logics
[ pdf ]
LTCS-Report 06-04,
Chair for Automata Theory,
Institute for Theoretical Computer Science,
Dresden University of Technology,
Germany, 2006.
Integrating Description Logics and action formalisms for reasoning about web services
[ ps.zip |
]
@techreport{LTCSRep2004,
author = {Franz Baader and Maja Mili{\v{c}}i{\'c} and Carsten Lutz
and Ulrike Sattler and Frank Wolter},
title = {Integrating Description Logics and action
formalisms for reasoning about web services},
type = {LTCS-Report},
number = {05-02},
institution = {Chair for Automata Theory,
Institute for Theoretical Computer Science,
Dresden University of Technology},
address = {Dresden, Germany},
year = {2005}
}
Motivated by the need for semantically well-founded and algorithmically manageable formalisms
for describing the functionality of Web services, we introduce an action formalism that is
based on description logics (DLs), but is firmly grounded on research in the reasoning about
action community. Our main contribution is an analysis of how the choice of the DL influences
the complexity of standard reasoning tasks such as projection and executability,
which are important for Web service discovery and composition.
LTCS-Report 05-02,
Chair for Automata Theory,
Institute for Theoretical Computer Science,
Dresden University of Technology,
Germany, 2005.
A tableau calculus for multimodal logics and some (un)decidability results
[ pdf |
]
@inproceedings{BaldoniTableaux98,
author = {Matteo Baldoni and Laura Giordano and Alberto Martelli},
title = {A tableau calculus for multimodal logics and some (un)decidability results},
pages = {44--59},
editor = {Harrie de Swart},
booktitle = {Proc.\ of the Int.\ Conf.\ on Analytic Tableaux
and Related Methods ({TABLEAUX}'98)},
series = {Lecture Notes in Artificial Intelligence},
volume = {1397},
publisher = {Springer},
year = {1998},
doi = {10.1007/3-540-69778-0_13},
ee = {http://dx.doi.org/10.1007/3-540-69778-0_13}
}
In this paper we present a prefixed analytic tableau calculus for a class
of normal multimodal logics and we present some results about decidability
and undecidability of this class. The class is characterized by axioms of the form
[t1]...[tn] → [s1]...[sm]φ,
called inclusion axioms, where the ti's and sj's are constants.
This class of logics, called grammar logics, was introduced for the first time
by Fariñas del Cerro and Penttonen to simulate the behaviour of grammars in modal logics,
and includes some well-known modal systems. The prefixed tableau method is used to prove
the undecidability of modal systems based on unrestricted,
context sensitive, and context free grammars.
Moreover, we show that the class of modal logics, based on right-regular grammars,
are decidable by means of the filtration methods, by defining an extension
of the Fischer-Ladner closure.
In H. de Swart, editor,Proc. of
the Int. Conf. on Analytic Tableaux and Related Methods,TABLEAUX'98,Oisterwijk, The Netherlands, May 5-8, 1998.LNAI,
vol. 1397,
pp. 44–59.
Springer, 1998.
The undecidability of the dominoe problem
[ pdf |
]
@article{Berger1966,
author = {Robert Berger},
title = {The undecidability of the dominoe problem},
journal = {Memoirs of the American Mathematical Society},
volume = {66},
year = {1966},
pages = {1--72},
doi = {10.1090/memo/0066},
ee = {http://dx.doi.org/10.1090/memo/0066}
}
A domino set is a finite set of square plates, the dominoes
all of the same size, whose edges are marked with symbols, each plate in a different manner.
Assume we have an unlimites number of copies of each type of domino.
We see to assemble the copies (also called dominoes) on an infinite plane,
ruled into squares the size of one domino, according to the following rules:
• No dominoe may be rotated or reflected.
• A domino must be placed exactly over a ruled square.
• The symbols on adjacent domino edges must match.
• Every square must be covered with a domino.
The domino set is called solvable if and only if the dominoes can be so assembled.
The Domino Problem deals with the class of all domino sets.
It consists of deciding, for each domino set, whether or not it is solvable.
We say that the Domino Problem is decidable or undecidable
according to whether there exists or does not exist an algorithm which, given the specifications of
an arbitrary domino set, will decide whether or not the set is solvable.
This paper proves that the Domino Problem is undecidable.
On the undecidability of logics with converse, nominals, recursion and counting
[ pdf |
]
@article{BonattiPeron2004,
author = {Piero A. Bonatti and A.Peron},
title = {On the undecidability of logics with converse, nominals, recursion and counting},
journal = {Artificial Intelligence},
volume = {158},
number = {1},
year = {2004},
pages = {75--96},
doi = {10.1016/j.artint.2004.04.012},
ee = {http://dx.doi.org/10.1016/j.artint.2004.04.012}
}
The evolution of Description Logics (DLs) and Propositional Dynamic Logics produced
a hierarchy of decidable logics with multiple maximal elements. It would
be desirable to combine different maximal logics into one super-logic, but then inference
may turn out to be undecidable. Then it is important to characterize the
decidability threshold for these logics. In this perspective, an interesting open question
pointed out by Sattler and Vardi [IJCAR 2001]
is whether inference in a hybrid μ-calculus
with restricted forms of graded modalities is decidable, and which complexity class
it belongs to.
In this paper we improve a previous result [Bonatti, IJCAI 2003] and prove that this
calculus and the corresponding DL μALCIOfa are undecidable.
We show also that nested fixpoints are not necessary for undecidability.
@inproceedings{BonattiLutzICALP06,
author = {Piero A. Bonatti and Carsten Lutz and Aniello Murano and Moshe Y. Vardi},
title = {The complexity of enriched $\mu$-calculi},
pages = {540--551},
editor = {Michele Bugliesi and Bart Preneel and Vladimiro Sassone and Ingo Wegener},
booktitle = {Proc.\ of the 33rd Int.\ Colloquium on Automata,
Languages and Programming (ICALP~2006)},
series = {Lecture Notes in Computer Science},
volume = {4052},
publisher = {Springer},
year = {2006},
doi = {10.1007/11787006_46},
ee = {http://dx.doi.org/10.1007/11787006_46}
}
The fully enriched μ-calculus is the extension of the propositional
μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability
in several expressive fragments of the fully enriched μ-calculus is known
to be decidable and ExpTime-complete, it has recently been proved that the full
calculus is undecidable.
In this paper, we study the fragments of the fully enriched
μ-calculus that are obtained by dropping at least one of the additional constructs.
We show that, in all fragments obtained in this way, satisfiability is decidable
and ExpTime-complete. Thus, we identify a family of decidable logics that are
maximal (and incomparable) in expressive power.
Our results are obtained by
introducing two new automata models, showing that their emptiness problems
are ExpTime-complete, and then reducing satisfiability in the relevant logics to
this problem. The automata models we introduce are
two-way graded alternating parity automata over infinite trees (2GAPT) and
fully enriched automata (FEA)
over infinite forests. The former are a common generalization of two incomparable
automata models from the literature. The latter extend alternating automata in
a similar way as the fully enriched μ-calculus extends the standard μ-calculus.
In
Proc. of
the 33rd Int. Colloquium on Automata, Languages and Programming,ICALP 2006,Venice, Italy, July 9-16, 2006,LNCS,
vol. 4052,
pp. 540-551, Springer, 2006.
Decidable reasoning in terminological knowledge representation systems
[ pdf |
]
@article{Buchheit_etal_1993a,
author = {Martin Buchheit and Francesco M. Donini and Andrea Schaerf},
title = {Decidable reasoning in terminological knowledge representation systems},
journal = {Journal of Artificial Intelligence Research},
volume = {1},
year = {1993},
pages = {109--138},
doi = {10.1613/jair.21},
ee = {http://dx.doi.org/10.1613/jair.21}
}
Terminological knowledge representation systems (TKRSs) are tools for designing and
using knowledge bases that make use of terminological languages (or concept languages).
We analyze from a theoretical point of view a TKRS whose capabilities go beyond the
ones of presently available TKRSs. The new features studied, often required in practical
applications, can be summarized in three main points. First, we consider a highly expressive
terminological language, called ALCNR , including general complements of concepts,
number restrictions and role conjunction. Second, we allow to express inclusion statements
between general concepts, and terminological cycles as a particular case. Third, we
prove the decidability of a number of desirable TKRS-deduction services (like satisfiability,
subsumption and instance checking) through a sound, complete and terminating calculus
for reasoning in ALCNR -knowledge bases. Our calculus extends the general technique
of constraint systems. As a byproduct of the proof, we get also the result that inclusion
statements in ALCNR can be simulated by terminological cycles, if descriptive semantics
is adopted.
Research Report RR-93-10, Deutsches Forschungszentrum für Künstliche Intelligenz
(DFKI),
Saarbrucken (Germany), 1993.
An abridged version appeared in
Proc. of
the 13th Int. Joint Conf. on Artificial Intelligence,IJCAI'93,Chambéry, France, August 28 – September 3, 1993,pp. 704-709, Morgan Kaufmann, 1993.
Finite model reasoning in Description Logics
[ pdf |
]
@inproceedings{Calvanese1996a,
author = {Diego Calvanese},
title = {Finite model reasoning in Description Logics},
pages = {292--303},
editor = {Luigia Carlucci Aiello and Jon Doyle and Stuart C. Shapiro},
booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Principles
of Knowledge Representation and Reasoning (KR'96)},
publisher = {Morgan Kaufmann},
year = {1996}
}
For the basic Description Logics reasoning with respect to finite models amounts to reasoning
with respect to arbitrary ones, but finiteness of the domain needs to be considered
if expressivity is increased and the finite model property fails. Procedures for
reasoning with respect to arbitrary models in very expressive Description Logics have been
developed, but these are not directly applicable in the finite case. We first show that we
can nevertheless capture a restricted form of finiteness and represent finite modeling structures
such as lists and trees, while still reasoning with respect to arbitrary models. The
main result of this paper is a procedure to reason with respect to finite models in an
expressive Description Logic equipped with inverse roles, cardinality constraints, and in
which arbitrary inclusions between concepts can be specified without any restriction. This
provides the necessary expressivity to go beyond most semantic and object-oriented Database
models, and capture several useful extensions.
In
L.C.Aiello,
Jon Doyle,
and
Stuart C. Shapiro,
editors,
Proc. of
the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning,KR'96,Cambridge, Massachusetts, USA, November 5-8, 1996,pp. 292-303, Morgan Kaufmann, 1996.
Reasoning in expressive Description Logics with fixpoints based on automata on infinite trees
[ pdf |
]
@inproceedings{CalvaneseEtAl1999c,
author = {Diego Calvanese and Giuseppe De Giacomo and Maurizio Lenzerini},
title = {Reasoning in expressive Description Logics with fixpoints
based on automata on infinite trees},
pages = {84--89},
editor = {Thomas Dean},
booktitle = {Proc.\ of the 16th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI'99)},
publisher = {Morgan Kaufmann},
year = {1999}
}
In the last years, the investigation on Description Logics (DLs) has been driven by the goal of applying
them in several areas, such as software engineering, information systems, databases, information
integration, and intelligent access to the web. The modeling requirements arising in the above
areas have stimulated the need for very rich languages, including fixpoint constructs to represent
recursive structures. We study a DL comprising the most general form of fixpoint constructs on concepts,
all classical concept forming constructs, plus inverse roles, n-ary relations, qualified number restrictions,
and inclusion assertions. We establish the ExpTime decidability of such logic by presenting
a decision procedure based on a reduction to nonemptiness of alternating automata on infinite
trees. We observe that this is the first decidability result for a logic combining inverse roles, number
restrictions, and general fixpoints.
In
Proc. of
the 16th Int. Joint Conf. on Artificial Intelligence,IJCAI'99,Stockholm, Sweden, July 31 – August 6, 1999,pp. 84–89, Morgan Kaufmann, 1999.
Reasoning in expressive Description Logics
[ pdf |
]
@incollection{HandbookARCh23,
author = {Diego Calvanese and Giuseppe De Giacomo and
Maurizio Lenzerini and Daniele Nardi},
title = {Reasoning in expressive Description Logics},
chapter = {23},
pages = {1581--1634},
editor = {Alan Robinson and Andrei Voronkov},
booktitle = {Handbook of Automated Reasoning},
publisher = {Elsevier Science Publishers},
year = {2001}
}
In
Alan Robinson
and Andrei Voronkov,
editors,
Handbook of Automated Reasoning, pp. 1581–1634 (Chapter 23).
Elsevier Science Publishers, 2001.
Nondeterministic Propositional Dynamic Logic with intersection is decidable
[ pdf |
]
@inproceedings{Danecki1984,
author = {Ryszard Danecki},
title = {Nondeterministic Propositional Dynamic Logic with intersection is decidable},
pages = {34--53},
editor = {Andrzej Skowron},
booktitle = {Proc.\ of the 5th Symposium on Computation Theory},
series = {Lecture Notes in Computer Science},
volume = {208},
publisher = {Springer},
year = {1985},
doi = {10.1007/3-540-16066-3_5},
ee = {http://dx.doi.org/10.1007/3-540-16066-3_5}
}
Propositional Dynamic Logic (PDL) of [Fisher, Ladner, 1979] defines meaning of programs in terms
of binary input-output relations. Basic regular operations on programs are interpreted as superposition,
union, and reflexive-transitive closure of relations. The intersection, cf. [Harel 1983],
is a binary program forming functor a∩b with the meaning given by the set-theoretical
intersection of relations corresponding to programs a and b.
By adding intersection of programs to PDL we obtain a programming logic called PDL with intersection.
Harel [Harel 1983] has proved that the problem of whether or not a formula of
PDL with intersection has a deterministic model is highly undecidable (Σ11-hard).
The present paper shows that in the general case (nondeterministic models allowed)
the satisfiability problem for PDL with intersection is decidable in time double exponential
in the length of the formula tested. In comparison with PDL with strong loop predicate
[Danecki 1984], this is more powerful and interesting example of a logic which is decidable
in contrast to its deterministic case and despite the lack of finite and even tree model properties.
Boosting the correspondence between Description Logics and Propositional Dynamic Logics
[ pdf |
]
@inproceedings{DeGiacomoLenzerini1994a,
author = {Giuseppe De Giacomo and Maurizio Lenzerini},
title = {Boosting the correspondence between Description Logics
and Propositional Dynamic Logics},
pages = {205--212},
editor = {Barbara Hayes-Roth and Richard E. Korf},
booktitle = {Proc.\ of the 12th Nat.\ Conf.\ on Artificial Intelligence (AAAI~1994)},
volume = {1},
publisher = {AAAI Press / The MIT Press},
year = {1994},
ee = {http://www.aaai.org/Library/AAAI/1994/aaai94-032.php}
}
One of the main themes in the area of Terminological Reasoning has been to identify
description logics (DLs) that are both very expressive and decidable.
A recent paper by Schild showed that this issue can be profitably addressed
by relying on a correspondence between DLs and propositional dynamic logics (PDL).
However Schild left open three important problems, related to the translation
into PDLs of functional restrictions on roles (both direct and inverse),
number restrictions, and assertions on individuals.
The work reported in this paper presents a solution to these problems.
The results have a twofold significance. From the standpoint of DLs,
we derive decidability and complexity results for some of
the most expressive logics appeared in the literature,
and from the standpoint of PDLs, we derive a general methodology
for the representation of several forms of program determinism and
for the specification of partial computations.
In
Proc. of
the 12th Nat. Conf. on Artificial Intelligence,AAAI'94,Seattle, Washington, July 31 – August 4, 1994,pp. 205-212, AAAI Press / The MIT Press, 1994.
Eliminating “converse” from converse PDL
[ pdf |
]
@article{DeGiacomoLenzerini1996a,
author = {Giuseppe De Giacomo},
title = {Eliminating ``converse'' from converse {PDL}},
journal = {Journal of Logic, Language, and Information},
volume = {5},
number = {2},
year = {1996},
pages = {193--208},
doi = {10.1007/BF00173700},
ee = {http://dx.doi.org/10.1007/BF00173700}
}
In this paper we show that it is possible to eliminate the “converse” operator from
the propositional dynamic logic CPDL (Converse PDL), without compromising the soundness
and completeness of inference for it. Specifically we present an encoding of CPDL formulae
into PDL that eliminates the converse programs from a CPDL formula, but adds enough
information so as not to destroy its original meaning with respect to satisfiability,
validity, and logical implication. Notably, the resulting PDL formula is polynomially
related to the original one. This fact allows one to build inference procedures for CPDL,
by encoding CPDL formulae into PDL, and then running an inference procedure for PDL.
TBox and ABox reasoning in expressive Description Logics
[ pdf |
]
@inproceedings{DeGiacomoLenzerini1996,
author = {Giuseppe De Giacomo and Maurizio Lenzerini},
title = {{TB}ox and {AB}ox reasoning in expressive Description Logics},
pages = {316--327},
editor = {Luigia Carlucci Aiello and Jon Doyle and Stuart C. Shapiro},
booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Principles
of Knowledge Representation and Reasoning (KR'96)},
publisher = {Morgan Kaufmann},
year = {1996}
}
A Description Logic (DL) system is characterized by four fundamental aspects:
the set of constructs used in concept and role expressions,
the kind of assertions allowed in the TBox (assertions on concepts)
and the ABox (assertions on individuals), and the inference mechanisms
for reasoning on both the TBox and the ABox.
Most of the research done in the last decade made several simplifying assumptions on the above aspects.
However, the recent interest in DLs exhibited in many application areas (databases,
software engineering, intelligent access to the network, planning, etc.)
calls for investigating DL systems with full capabilities.
The work presented in this paper represents a step in this direction.
We present a sound, complete, and terminating (in worst-case ExpTime) inference procedure
that solves the problem of reasoning in a DL system with the following characteristics:
it comes equipped with a very expressive language, it allows the most general form of
TBox assertions, and it takes into account instance assertions on both concepts and roles in the ABox.
In
L.C.Aiello,
Jon Doyle,
and
Stuart C.Shapiro,
editors,
Proc. of
the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning,KR'96,Cambridge, Massachusetts, U.S.A., November 5-8, 1996.pp. 316-327. Morgan Kaufmann, 1996.
A uniform framework for concept definitions in Description Logics
[ pdf |
]
@article{DeGiacomoLenzerini1997,
author = {Giuseppe De Giacomo and Maurizio Lenzerini},
title = {A uniform framework for concept definitions in Description Logics},
journal = {Journal of Artificial Intelligence Research},
volume = {6},
year = {1997},
pages = {87--110},
doi = {10.1613/jair.334},
ee = {http://dx.doi.org/10.1613/jair.334}
}
Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain
are based on the notions of class (or concept) and relationship among classes. One interesting feature
of such formalisms is the possibility of defining a class, i.e., providing a set of properties that
precisely characterize the instances of the class. Many recent articles point out that there are several
ways of assigning a meaning to a class definition containing some sort of recursion.
In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results
by adopting a formalism that allows for different semantics to coexist. We demonstrate the feasibility
of our argument, by presenting a knowledge representation formalism, the description logic
μALCQ , with the above characteristics. In addition to the constructs for conjunction,
disjunction, negation, quantifiers, and qualified number restrictions, μALCQ includes
special fixpoint constructs to express (suitably interpreted) recursive definitions.
These constructs enable the usual frame-based descriptions to be combined with definitions of recursive
data structures such as directed acyclic graphs, lists, streams, etc. We establish several properties
of μALCQ , including the decidability and the computational complexity of reasoning,
by formulating a correspondence with a particular modal logic of programs called the modal μ-calculus.
The complexity of regularity in grammar logics and related modal logics
[ pdf |
]
@article{DemriJLC2001,
author = {Stéphane Demri},
title = {The complexity of regularity in grammar logics and related modal logics},
journal = {Journal of Logic and Computation},
volume = {11},
number = {6},
year = {2001},
pages = {933--960},
doi = {10.1093/logcom/11.6.933},
ee = {http://dx.doi.org/10.1093/logcom/11.6.933}
}
A modal reduction principle of the form
[i1]...[in]p → [j1]...[jn']p can be
viewed as a production rule
i1...in → j1...jn' in a formal grammar.
We study the extensions of the multimodal logic Km with m independent K
modal connectives by finite addition of axiom schemes of the above form such
that the associated finite set of production rules forms a regular grammar. We
show that given a regular grammar G and a modal formula φ, deciding whether
the formula is satisfiable in the extension of Km with axiom schemes from G
can be done in deterministic exponential-time in the size of G and φ, and this
problem is complete for this complexity class. Such an extension of Km is called
a regular grammar logic. The proof of the exponential-time upper bound is
extended to PDL-like extensions of Km and to global logical consequence and
global satisfiability problems. Using an equational characterization of context-free
languages, we show that by replacing the regular grammars by linear ones,
the above problem becomes undecidable. The last part of the paper presents
non-trivial classes of exponential time complete regular grammar logics.
@inproceedings{DingHaWiDL2007,
author = {Yu Ding and Volker Haarslev and Jiewen Wu},
title = {A new mapping from $\mathcal{ALCI}$ to $\mathcal{ALC}$},
editor = {Diego Calvanese and Enrico Franconi and
Volker Haarslev and Domenico Lembo and
Boris Motik and Anni-Yasmin Turhan and Sergio Tessaris},
booktitle = {Proc.\ of the 20th Int.\ Workshop on Description Logics (DL~2007)},
series = {CEUR Workshop Proceedings},
volume = {250},
publisher = {CEUR-WS.org},
year = {2007},
ee = {http://ceur-ws.org/Vol-250/paper_32.pdf}
}
It is well known that a correspondence theory for description logics (DLs), propositional
modal logics (MLs) and propositional dynamic logics (PDLs) was given
in [Schild 1991] and that an axiomatic system for a description logic with inverse roles
was presented in the same paper. Schild's paper covers what is to be discussed
in this paper although his paper did not mention nominals as well as expressive
roles explicitly. On the other hand, reductions to eliminate converse programs
(inverse roles in DLs) are known even for full PDL (ALCIreg);
the original reduction
from converse PDL to PDL was in [Giacomo 1996]. Moreover, a direct tableaux
method for converse PDL and further discussions on the elimination of converse
programs were given in [Giacomo, Massacci, 2000]. Besides graded modalities, it was pointed out in
[Giacomo 1996] that the previous reduction technique is also applicable to nominals.
This paper shares some viewpoints well made in [Giacomo 1996]. The proposed
mapping process here is based on the simple idea to capture possible back-propagation
caused by the use of inverse roles. This process consists of three
steps, tagging, recording, polarisation, which are introduced below.
Concept expressions / formulae are assumed to be in negation norm form (NNF). For simplicity,
existential restrictions and universal restrictions are called modal constraints
somewhere. We refer to [DL Handbook] for usual background knowledge on
description logics (DLs).
In
Proc. of
the 2007 Int. Workshop on Description Logics,DL 2007,Brixen-Bressanone, near Bozen-Bolzano, Italy, June 8-10, 2007,vol. 250 in CEUR,
pp. 267–274, 2007.
@article{DoniniMassacci2000,
author = {Francesco M. Donini and Fabio Massacci},
title = {ExpTime tableaux for $\mathcal{ALC}$},
journal = {Artificial Intelligence},
volume = {124},
number = {1},
year = {2000},
pages = {87--138},
doi = {10.1016/S0004-3702(00)00070-9},
ee = {http://dx.doi.org/10.1016/S0004-3702(00)00070-9}
}
The last years have seen two major advances in Knowledge Representation and Reasoning. First,
many interesting problems (ranging from Semi-structured Data to Linguistics) were shown to be
expressible in logics whose main deductive problems are ExpTime-complete. Second, experiments
in automated reasoning have substantially broadened the meaning of “practical tractability”.
Instances of realistic size for PSpace-complete problems are now within reach for implemented systems.
Still, there is a gap between the reasoning services needed by the expressive logics mentioned
above and those provided by the current systems. Indeed, the algorithms based on tree-automata,
which are used to prove ExpTime-completeness, require exponential time and space even in simple
cases. On the other hand, current algorithms based on tableau methods can take advantage of such
cases, but require double exponential time in the worst case.
We propose a tableau calculus for the description logic ALC for checking the satisfiability of a
concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based
decision procedure working in single exponential time.
To guarantee the ease of implementation, we also discuss the effects that optimizations
(propositional backjumping, simplification, semantic branching, etc.) might have on our complexity
result, and introduce a few optimizations ourselves.
Propositional Dynamic Logic of regular programs
[ pdf |
]
@article{FischerLadner1979,
author = {Michael J. Fischer and Richard E. Ladner},
title = {Propositional Dynamic Logic of regular programs},
journal = {Journal of Computer and System Science},
volume = {18},
number = {2},
year = {1979},
pages = {194--211},
doi = {10.1016/0022-0000(79)90046-1},
ee = {http://dx.doi.org/10.1016/0022-0000(79)90046-1}
}
We introduce a fundamental propositional logical system based on modal logic for
describing correctness, termination and equivalence of programs. We define a formal
syntax and semantics for the propositional dynamic logic of regular programs and give
several consequences of the definition. Principal conclusions are that deciding satisfiability
of length n formulas requires time dn/logn
for some d > 1, and that satisfiability can be
decided in nondeterministic time cn for some c.
We provide applications of the decision
procedure to regular expressions, Ianov schemes, and classical systems of modal logic.
Modal environment for Boolean speculations
[ pdf |
]
@incollection{Gargov_etal_1987,
author = {George Gargov and Solomon Passy and Tinko Tinchev},
title = {Modal environment for {B}oolean speculations},
pages = {253--263},
editor = {Dimiter G. Skordev},
booktitle = {Mathematical Logic and Its Applications},
publisher = {Plenum Press},
year = {1987},
doi = {10.1007/978-1-4613-0897-3_17},
ee = {http://dx.doi.org/10.1007/978-1-4613-0897-3_17}
}
The common form of a mathematical theorem consists in that "the truth of some properties for some objects is necessary and/or sufficient condition for other properties to hold for other objects". To formalize this, one happens to resort to Kripke modal logic K which, having in the syntax the notions of 'property' and 'necessity', appears to provide a reliable metamathematical fundament. In this paper we challenge this reliability. We propose two different approaches each claiming better formal treatment of the state of affairs. The first approach is in formalizing the notion of 'sufficiency' (which remains beyond the capacities of K), and consequently of 'sufficiency' and 'necessity' in a joint context. The second is our older idea to formalize the notion of 'object' in the same modal spirit. Having 'property, object, sufficiency, necessity', we establish some basic results and profess to properly formalize the everyday metamathematical reason.
In
Dimiter G. Skordev,
editor,
Mathematical Logic and its Applications,
Proc. of the Advanced International Summer School and Conference
dedicated to the 80th anniversary of Kurt Gödel's birth,
Druzhba near Varna, Bulgaria, September 24 – October 4, 1986,pp. 253-263, Plenum Press, New York, 1987.
PDL with intersection and converse is 2EXP-complete
[ pdf |
]
@inproceedings{GoLoLuICPDL2007,
author = {Stefan G{\"o}ller and Markus Lohrey and Carsten Lutz},
title = {{PDL} with intersection and converse is {2EXP}-complete},
pages = {198--212},
editor = {Helmut Seidl},
booktitle = {Proc.\ of the 10th Int.\ Conf.\ on Foundations of
Software Science and Computational Structures (FoSSaCS 2007)},
series = {Lecture Notes in Computer Science},
volume = {4423},
publisher = {Springer},
year = {2007},
doi = {10.1007/978-3-540-71389-0_15},
ee = {http://dx.doi.org/10.1007/978-3-540-71389-0_15}
}
We study the complexity of satisfiability in the expressive extension
ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and
converse as program operations. Our main result is containment in 2EXP, which
improves the previously known non-elementary upper bound and implies 2EXP-completeness
due to an existing lower bound for PDL with intersection. The proof
proceeds by showing that every satisfiable ICPDL formula has a model of tree-width
at most two and then giving a reduction to the (non-)emptiness problem for
alternating two-way automata on infinite trees. In this way, we also reprove in an
elegant way Danecki's difficult result that satisfiability for PDL with intersection
is in 2EXP.
Note: Here EXP means ExpTime, and 2EXP means ExpExpTime. (E.Z.)
In
Helmut Seidl, editor,
Proc. of
the 10th Int. Conf. on Foundations of Software Science and Computation Structures,FoSSaCS 2007,Braga, Portugal, 24 March – 1 April, 2007,LNCS,
vol. 4423,
pp. 198–212, Springer, 2007.
ExpTime tableaux with global caching for Description Logics with transitive roles, inverse roles and role hierarchies
[ pdf |
]
@inproceedings{Gore_Nguyen_2007,
author = {Rajeev Gor{\'e} and Linh Anh Nguyen},
title = {{ExpTime} tableaux with global caching for Description Logics
with transitive roles, inverse roles and role hierarchies},
pages = {133--148},
editor = {Nicola Olivetti},
booktitle = {Proc.\ of the 16th Int.\ Conf.\ on Automated Reasoning
with Analytic Tableaux and Related Methods (TABLEAUX 2007)},
series = {Lecture Notes in Computer Science},
volume = {4548},
publisher = {Springer},
year = {2007},
doi = {10.1007/978-3-540-73099-6_12},
ee = {http://dx.doi.org/10.1007/978-3-540-73099-6_12}
}
The description logic SHI extends the basic description logic
ALC with transitive roles, role hierarchies and inverse roles.
The known tableau-based decision procedure for SHI exhibit (at least) NExpTime
behaviour even though SHI is known to be ExpTime-complete.
The automata-based algorithms for SHI often yield optimal worst-case
complexity results, but do not behave well in practice since good optimisations
for them have yet to be found. We extend our method for global
caching in ALC to SHI by adding analytic cut rules, thereby giving the
first ExpTime tableau-based decision procedure for SHI , and showing
one way to incorporate global caching and inverse roles.
In
the Int. Conf. on Analytic Tableaux and Related Methods,TABLEAUX 2007,Aix en Provence, France, July 3-6, 2007.LNCS,
vol. 4548,
pp. 133–148, Springer, 2007.
Note: This logic is known as SHI .
Two-variable logic with counting is decidable
[ pdf |
ps.zip |
]
@inproceedings{Gradel_etal_1997b,
author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
title = {Two-variable logic with counting is decidable},
pages = {306--317},
editor = {Glynn Winskel},
booktitle = {Proc.\ of the 12th Annual IEEE Symposium
on Logic in Computer Science (LICS'97)},
publisher = {IEEE Computer Society Press},
year = {1997},
doi = {10.1109/LICS.1997.614957},
ee = {http://dx.doi.org/10.1109/LICS.1997.614957}
}
We prove that the satisfiability problem for C2 is decidable.
C2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers
∃≥m, m≥1.
It considerably extends L2, plain first-order with only two variables,
which is known to be decidable by a result of Mortimer.
Unlike L2, C2 does not have the finite model property.
As C2 extends L2 by expressive means for counting,
significant applications arise from the fact that C2 embeds
corresponding counting extensions of modal logics.
In
Proc. of
the 12th IEEE Symposium on Logic in Computer Science,LICS'97,Warsaw, Poland, June 29 – July 2, 1997,pp. 306-317, IEEE Computer Society Press, 1997.
On expressive number restrictions in Description Logics
[ pdf |
]
@inproceedings{GrandiDL2001,
author = {Fabio Grandi},
title = {On expressive number restrictions in Description Logics},
pages = {56--65},
editor = {Carole Goble and Deborah L. McGuinness and
Ralf M{\"o}ller and Peter F. Patel-Schneider},
booktitle = {Proc.\ of the 14th Int.\ Workshop on Description Logics (DL~2001)},
series = {CEUR Workshop Proceedings},
volume = {49},
publisher = {CEUR-WS.org},
year = {2001},
ee = {http://ceur-ws.org/Vol-49/Grandi-56start.ps}
}
We consider expressive Description Logics (ALCN ) allowing for number restrictions on complex roles
built with combinations of role constructors. In particular, we are mainly interested in Logics
(called ALCN ) allowing for the same kind
of complex roles both in number and in value restrictions, which represent
very expressive description languages and can be shown very useful for applications.
We investigate the computational properties of various ALCN extensions and slightly improve
the (un)decidability results following from the study published by Baader and Sattler in 1999.
In particular, we will show by reduction of a domino problem that
ALCN (+,∪) and
ALCN (+,∩) are undecidable.
In
Proc. of
the 2001 Int. Workshop on Description Logics,DL 2001,Stanford University, California, USA, August 1-3, 2001,vol. 49 in CEUR,
pp. 56–65, 2001.
On expressive Description Logics with composition of roles in number restrictions
[ pdf |
]
@inproceedings{GrandiLPAR2002,
author = {Fabio Grandi},
title = {On expressive Description Logics
with composition of roles in number restrictions},
pages = {202--215},
editor = {Matthias Baaz and Andrei Voronkov},
booktitle = {Proc.\ of the 9th Int.\ Conf.\ on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR~2002)},
series = {Lecture Notes in Computer Science},
volume = {2514},
publisher = {Springer},
year = {2002},
doi = {10.1007/3-540-36078-6_14},
ee = {http://dx.doi.org/10.1007/3-540-36078-6_14}
}
Description Logics are knowledge representation formalisms
which have been used in a wide range of application domains. Owing to
their appealing expressiveness, we consider in this paper extensions of the
well-known concept language ALC allowing for number restrictions on
complex role expressions. These have been first introduced by Baader and
Sattler as ALCN (M) languages, with the adoption of role constructors
M ⊆ {o,—,∪,∩}.
In particular, as far as languages equipped with role composition are
concerned, they showed in 1999 that, although ALCN(o) is decidable,
the addition of other operators may easily lead to undecidability: in fact,
ALCN (o,∩) and ALCN (o,—,∪)
were proved undecidable.
In this work, we further investigate the computational properties of the
ALCN family, aiming at narrowing the decidability gap left open by
Baader and Sattler's results. In particular, we will show that ALCN (o)
extended with inverse roles both in number and in value restrictions
becomes undecidable, whereas it can be safely extended with qualified
number restrictions without losing decidability of reasoning.
In
M. Baaz, A. Voronkov, editors,
Proc. of
the 9th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning,LPAR 2002,Tbilisi, Georgia, October 14-18, 2002.LNAI,
vol. 2514,
pp. 202–215, Springer, Berlin, 2002.
A tableau system for the Description Logic SHIO
[ ps.zip |
]
@inproceedings{HladikIJCAR2004,
author = {Jan Hladik},
title = {A tableau system for the Description Logic $\mathcal{SHIO}$},
pages = {21--25},
editor = {Ulrike Sattler},
booktitle = {Contributions to the Doctoral Programme of the 2nd Int.\
Joint Conf.\ on Automated Reasoning (IJCAR~2004)},
series = {CEUR Workshop Proceedings},
volume = {106},
publisher = {CEUR-WS.org},
year = {2004},
ee = {http://ceur-ws.org/Vol-106/05-hladik.ps}
}
For the satisfiability test of description logics (DLs), there are two prominent families of algorithms
with complementary advantages and disadvantages: firstly, automata-based algorithms,
which translate a DL expression φ into an automaton Aφ which accepts all
(abstractions of) models for φ, so that the satisfiability test for φ can be reduced to the emptiness
test of Aφ; and secondly, tableau algorithms, which incrementally create a
tree-shaped (pre-)model for φ using a set of rules labelling each tree node with the
appropriate subformulas of φ. In short, the advantages of automata algorithms are on the theoretical
side, because in many cases the proofs are very elegant and offer tight complexity bounds
(in particular for ExpTime-complete logics), whereas the advantages of tableau algorithms
are on the practical side, since they are well suited for implementation and optimisation.
In contrast, intuitive automata algorithms usually require exponential time also in the best case,
and thus an efficient implementation requires considerable modifications.
For this reason, an approach combining both advantages is highly desirable.
In [3], we introduced tableau systems (TS), a framework for tableau algorithms.
If a tableau algorithm can be described within this framework, the existence of
an automata algorithm (and thus the ExpTime upper bound) directly follows.
Moreover, only soundness and completeness of the tableau algorithm have to be proved;
termination and a practical procedure to ensure termination,
called a blocking test, also follows from the prerequisites of the framework.
As an example for the usefulness of this framework, we present in this paper
a TS for SHIO, an expressive DL whose computational properties to the best
of our knowledge have not been analysed so far. The purpose of this is two-fold:
firstly, we obtain that SHIO satisfiability is ExpTime-complete and
can be decided by a tableau algorithm. Secondly, the succinctness of the proofs
demonstrates how our framework simplifies the design of tableau algorithms.
[3] F.Baader, J.Hladik, C.Lutz, and F.Wolter.
From tableaux to automata for description logics.
Fundamenta Informaticae,
57:1-33, 2003.
In
Proc. of the Doctoral Programme of
the 2nd Int. Joint Conf. on Automated Reasoning,IJCAR 2004,Cork, Ireland, July 4-8, 2004.vol. 106 in CEUR,
pp. 21-25, 2004.
@inproceedings{HladikModelDL2004,
author = {Jan Hladik and J{\"o}rg Model},
title = {Tableau systems for $\mathcal{SHIO}$ and $\mathcal{SHIQ}$},
pages = {168--177},
editor = {Volker Haarslev and Ralf M{\"o}ller},
booktitle = {Proc.\ of the 17th Int.\ Workshop on Description Logics (DL~2004)},
series = {CEUR Workshop Proceedings},
volume = {104},
publisher = {CEUR-WS.org},
year = {2004},
ee = {http://ceur-ws.org/Vol-104/22Hladik-final.pdf}
}
Two prominent families of algorithms for the satisfiability test of Description Logics are
automata-based algorithms, which translate a concept C into an automaton
AC accepting all (abstractions of) models for C,
and tableau algorithms, which
incrementally create a tree-shaped (pre-)model for C using a set of completion rules.
In short, the advantages of automata algorithms are on the theoretical side, because in
many cases the proofs are very elegant and provide tight complexity bounds (in particular
for ExpTime-complete logics), whereas the advantages of tableau algorithms are
on the practical side, since they are well suited for implementation and optimisation.
Thus, an approach combining both advantages is highly desirable. In [1], we introduced
tableau systems (TS), a framework for tableau algorithms. From a TS for
a DL L, we can derive an automata algorithm deciding satisfiability of L inputs in
exponential time, and a tableau algorithm for L, including an appropriate blocking
condition which ensures termination. As an application of this framework, we present
in this paper tableau systems for two expressive DLs, the new DL SHIO and the well-known
SHIQ. Our main results are the following: firstly, we obtain that SHIO
satisfiability is ExpTime-complete and can be decided by a tableau algorithm. Secondly,
we will see that although these two logics share most of their constructs, they
lead to quite different TSs, which demonstrates how the capabilities of our framework
can be used to capture different language properties. Thirdly, the succinctness of the
proofs demonstrates how our framework simplifies the design of tableau algorithms.
In
Proc. of
the 2004 Int. Workshop on Description Logics,DL 2004,Whistler, British Columbia, Canada, June 6-8, 2004,vol. 104 in CEUR,
pp. 168–177, 2004.
@inproceedings{HladikPenalozaDL06,
author = {Jan Hladik and Rafael Pe{\~n}aloza},
title = {PSpace automata for Description Logics},
pages = {74--85},
editor = {Bijan Parsia and Ulrike Sattler and David Toman},
booktitle = {Proc.\ of the 19th Int.\ Workshop on Description Logics (DL~2006)},
series = {CEUR Workshop Proceedings},
volume = {189},
publisher = {CEUR-WS.org},
year = {2006},
ee = {http://ceur-ws.org/Vol-189/submission_22.pdf}
}
Tree automata are often used for satisfiability testing in the area of
description logics, which usually yields ExpTime complexity results. We
examine conditions under which this result can be improved, and we define two classes of automata,
called segmentable and weakly-segmentable,
for which emptiness can be decided using space logarithmic in the size of
the automaton (and thus polynomial in the size of the input). The usefulness
of segmentable automata is demonstrated by reproving the known
PSpace result for satisfiability of ALC concepts with respect to acyclic TBoxes.
In
Proc. of
the 2006 Int. Workshop on Description Logics,DL 2006,Windermere, Lake District, UK, May 30 – June 1, 2006vol. 189 in CEUR,
pp. 74–85, 2006.
@article{WvanderHoek1992,
author = {Wiebe van der Hoek},
title = {On the semantics of graded modalities},
journal = {Journal of Applied Non-Classical Logics},
volume = {2},
number = {1},
year = {1992},
pages = {81--123}
}
We enrich propositional modal logic with operators Mn (n ∈ N)
which are interpreted on Kripke structures as “there are more than n
accessible worlds for which...”, thus obtaining a basic graded logic GrK.
We show how some familiar concepts (such as subframes, p-morphisms, disjoint unions and filtrations)
and techniques from modal model theory can be used to obtain results about
expressiveness (like graded modal equivalence, correspondence and definability)
for this language. On the basis of the class of linear frames we demonstrate that the expressive
power of the language is considerably stronger than that of classical modal logic.
We give a class of formulas for which a first order equivalent can be systematically obtained,
but also show that the set of formulas for which such an equivalence exists is in some sense
a proper subset of the set of so called Sahlqvist formulas, a syntactically defined set of
modal formulas for which a corresponding formula is guaranteed to exist.
Finally, we show how, combining the technique of ‘filtration’ with a notion of ‘copying’
worlds – in view of the “more than n” interpretation,
one cannot simply collapse worlds – for some modal logics
(GrK, GrT, ...), the finite model property (and also decidability) is obtained.
Note: graded modal logics are in fact denoted in this paper as
K,
T, etc. (E.Z.)
@inproceedings{HorrKutzSattlerSRIQ,
author = {Ian Horrocks and Oliver Kutz and Ulrike Sattler},
title = {The irresistible $\mathcal{SRIQ}$},
pages = {108--117},
editor = {Bernardo Cuenca Grau and Ian Horrocks and
Bijan Parsia and Peter F. Patel-Schneider},
booktitle = {Proc.\ of the 1st Int.\ Workshop on OWL:
Experiences and Directions (OWLED~2005)},
series = {CEUR Workshop Proceedings},
volume = {188},
publisher = {CEUR-WS.org},
year = {2005},
ee = {http://ceur-ws.org/Vol-188/sub20.pdf}
}
Motivated primarily by medical terminology applications,
the prominent DL SHIQ has already been extended to a DL with complex
role inclusion axioms of the form
RoS ⊆ R
or
SoR ⊆ R,
called RIQ , and the SHIQ tableau algorithm has been extended to handle
such inclusions.
This paper further extends RIQ and its tableau algorithm with important
expressive means that are frequently requested in ontology applications,
namely with reflexive, symmetric, transitive, and irreflexive
roles, disjoint roles, and the construct ∃R.Self, allowing, for instance, the
definition of concepts such as a “narcissist”. Furthermore, we extend the algorithm
to cover ABox reasoning extended with negated role assertions.
The resulting logic is called SRIQ .
@inproceedings{HorrKutzSattlerSROIQ,
author = {Ian Horrocks and Oliver Kutz and Ulrike Sattler},
title = {The even more irresistible $\mathcal{SROIQ}$},
pages = {57--67},
editor = {Patrick Doherty and John Mylopoulos and Christopher A. Welty},
booktitle = {Proc.\ of the 10th Int.\ Conf.\ on the Principles of
Knowledge Representation and Reasoning (KR~2006)},
publisher = {AAAI Press},
year = {2006},
ee = {http://www.aaai.org/Library/KR/2006/kr06-009.php}
}
We describe an extension of the description logic underlying OWL-DL,
SHOIN , with a number of expressive means that we believe
will make it more useful in practice. Roughly speaking, we extend
SHOIN with all expressive means that were suggested to us by ontology
developers as useful additions to OWL-DL, and which, additionally,
do not affect its decidability. We consider complex role inclusion
axioms of the form
RoS ⊆ R
or
SoR ⊆ R,
to express propagation
of one property along another one, which have proven useful in medical
terminologies. Furthermore, we extend SHOIN with reflexive,
symmetric, transitive, and irreflexive roles, disjoint roles, a universal
role, and constructs ∃R.Self, allowing, for instance, the definition of
concepts such as a “narcissist”. Finally, we consider negated role assertions
in ABoxes and qualified number restrictions. The resulting logic
is called SROIQ .
We present a rather elegant tableau-based reasoning algorithm: it
combines the use of automata to keep track of universal value restrictions
with the techniques developed for SHOIQ . We believe that
SROIQ could serve as a logical basis for possible future extensions
of OWL-DL.
In
Proc. of
the 10th Int. Conf. on the Principles of Knowledge Representation and Reasoning,KR 2006,Lake District of the UK, June 2-5, 2006.
pp. 57-67,
AAAI Press,
2006.
A Description Logic with transitive and inverse roles and role hierarchies
[ pdf |
]
@article{HorrocksSattlerSHI1999,
author = {Ian Horrocks and Ulrike Sattler},
title = {A Description Logic with transitive and inverse roles and role hierarchies},
journal = {Journal of Logic and Computation},
volume = {9},
number = {3},
year = {1999},
pages = {385--410},
doi = {10.1093/logcom/9.3.385},
ee = {http://dx.doi.org/10.1093/logcom/9.3.385}
}
The combination of transitive and inverse roles is important in a range of applications,
and is crucial for the adequate representation of aggregated objects, allowing the simultaneous description
of parts by means of the whole to which they belong and of wholes by means of their constituent parts.
In this paper we present a tableaux algorithms for deciding concept satisfiability and subsumption in
Description Logics that extend ALC with both transitive and inverse roles, a role hierarchy,
and functional restrictions. In contrast to earlier algorithms for similar logics, those presented here
are well-suited for implementation purposes: using transitive roles and role hierarchies in place
of the transitive closure of roles enables sophisticated blocking techniques to be used in place
of the cut rule, a rule whose high degree of non-determinism strongly discourages its use in an implementation.
As well as promising superior computational behaviour, this new approach is shown to be sufficiently powerful
to allow subsumption and satisfiability with respect to a (possibly cyclic) knowledge base to be reduced
to concept subsumption and satisfiability, and to support reasoning in a Description Logic that no longer
has the finite model property.
Note: this Description Logic is now known as SHI .
Ontology reasoning in the SHOQ (D) Description Logic
[ pdf |
]
@inproceedings{HorrSattSHOQD,
author = {Ian Horrocks and Ulrike Sattler},
title = {Ontology reasoning in the $\mathcal{SHOQ}(D)$ Description Logic},
pages = {199--204},
editor = {Bernhard Nebel},
booktitle = {Proc.\ of the 17th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~2001)},
publisher = {Morgan Kaufmann},
year = {2001}
}
Ontologies are set to play a key rôle in the “Semantic Web” by providing
a source of shared and precisely defined terms that can be used in descriptions of web resources.
Reasoning over such descriptions will be essential if web resources
are to be more accessible to automated processes. SHOQ (D) is an expressive description
logic equipped with named individuals and concrete datatypes which has almost exactly the same
expressive power as the latest web ontology languages (e.g., OIL and DAML+OIL). We present
sound and complete reasoning services for this logic.
In
B. Nebel, editor,
Proc. of
the 17th Int. Joint Conf. on Artificial Intelligence,IJCAI 2001,Seattle, Washington, USA, August 4-10, 2001,pp. 199–204, Morgan Kaufmann, 2001.
Decidability of SHIQ with complex role inclusion axioms
[ pdf |
]
@article{HorrSattRIQ,
author = {Ian Horrocks and Ulrike Sattler},
title = {Decidability of $\mathcal{SHIQ}$ with complex role inclusion axioms},
journal = {Artificial Intelligence},
volume = {160},
number = {1--2},
pages = {79--104},
year = {2004},
doi = {10.1016/j.artint.2004.06.002},
ee = {http://dx.doi.org/10.1016/j.artint.2004.06.002}
}
Motivated by medical terminology applications, we investigate the decidability of an expressive
and prominent description logic (DL), SHIQ , extended with role inclusion axioms of the form
RoS ⊆ T.
It is well known that a naïve such extension leads to undecidability, and thus we restrict
our attention to axioms of the form
RoS ⊆ R
or
SoR ⊆ R,
which is the most important form of axioms in the applications that motivated this extension.
Surprisingly, this extension is still undecidable.
However, it turns out that by restricting our attention further to acyclic sets of such axioms, we regain
decidability. We present a tableau-based decision procedure for this DL and report on its implementation,
which promises to behave well in practice and provides important additional functionality in
a medical terminology application.
Proc. of
the 19th Int. Joint Conf. on Artificial Intelligence,IJCAI 2005,Edinburgh, Scotland, UK, July 30 – August 5, 2005,
pp. 448-453,
Professional Book Center, 2005.
A PSpace-algorithm for deciding ALCNIR+-satisfiability
[ ps.zip |
]
@techreport{HorrocksSattlerTobies1998,
author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies},
title = {A {PS}pace-algorithm for deciding $\mathcal{ALCNI}_{R^+}$-satisfiability},
institution = {LuFg Theoretical Computer Science, RWTH Aachen},
address = {Germany},
type = {LTCS-Report},
number = {98-08},
year = {1998}
}
ALCNIR+ —
ALCN augmented with transitive and inverse roles — is an expressive Description Logic
which is especially well-suited for the representation of complex, aggregated objects.
Despite its expressiveness, it has been conjectured that concept satisfiability for this logic could
be decided in a comparatively efficient way. In this paper we prove the correctness of this conjecture
by presenting a PSpace algorithm for deciding satisfiability and subsumption of
ALCNIR+-concepts.
The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution.
Note: this Description Logic is now known as SIN .
Practical reasoning for expressive Description Logics
[ pdf |
]
@inproceedings{HorrocksSattlerPract1999,
author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies},
title = {Practical reasoning for expressive Description Logics},
pages = {161--180},
editor = {Harald Ganzinger and David A. McAllester and Andrei Voronkov},
booktitle = {Proc.\ of the 6th Int.\ Conf.\ on Logic for Programming
and Automated Reasoning (LPAR'99)},
series = {Lecture Notes in Computer Science},
volume = {1705},
publisher = {Springer},
year = {1999},
doi = {10.1007/3-540-48242-3_11},
ee = {http://dx.doi.org/10.1007/3-540-48242-3_11}
}
Description Logics (DLs) are a family of knowledge representation
formalisms mainly characterised by constructors to build complex
concepts and roles from atomic ones. Expressive role constructors are
important in many applications, but can be computationally problematical.
We present an algorithm that decides satisfiability of the DL ALC
extended with transitive and inverse roles, role hierarchies, and qualifying
number restrictions. Early experiments indicate that this algorithm
is well-suited for implementation. Additionally, we show that ALC extended
with just transitive and inverse roles is still in PSpace. Finally,
we investigate the limits of decidability for this family of DLs.
E.Z.: In short: SHIQ is decidable; SI is in PSpace;
unrestricted SHN is undecidable.
Practical reasoning for very expressive Description Logics
[ pdf |
]
@article{HorrocksSattlerPract2000,
author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies},
title = {Practical reasoning for very expressive Description Logics},
journal = {Logic Journal of the IGPL},
volume = {8},
number = {3},
year = {2000},
pages = {239--263},
doi = {10.1093/jigpal/8.3.239},
ee = {http://dx.doi.org/10.1093/jigpal/8.3.239}
}
Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised
by constructors to build complex concepts and roles from atomic ones. Expressive role constructors
are important in many applications, but can be computationally problematical.
We present an algorithm that decides satisfiability of the DL ALC extended with transitive and
inverse roles and functional restrictions with respect to general concept inclusion axioms and role
hierarchies; early experiments indicate that this algorithm is well-suited for implementation. Additionally,
we show that ALC extended with just transitive and inverse roles is still in PSpace. We
investigate the limits of decidability for this family of DLs, showing that relaxing the constraints
placed on the kinds of roles used in number restrictions leads to the undecidability of all inference
problems. Finally, we describe a number of optimisation techniques that are crucial in obtaining
implementations of the decision procedures, which, despite the hight worst-case complexity of the
problem, exhibit good performance with real-life problems.
E.Z.: In short: SHIQ is decidable; SI is in PSpace;
unrestricted SHN is undecidable.
How many legs do I have? Non-simple roles in number restrictions revisited
[ pdf |
]
@inproceedings{KazSatZolin2007,
author = {Yevgeny Kazakov and Ulrike Sattler and Evgeny Zolin},
title = {How many legs do {I} have? {N}on-simple roles
in number restrictions revisited},
pages = {303--317},
editor = {Nachum Dershowitz and Andrei Voronkov},
booktitle = {Proc.\ of the 14th Int.\ Conf.\ on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR~2007)},
series = {Lecture Notes in Computer Science},
volume = {4790},
publisher = {Springer},
year = {2007},
doi = {10.1007/978-3-540-75560-9_23}
ee = {http://dx.doi.org/10.1007/978-3-540-75560-9_23}
}
The Description Logics underpinning OWL impose a well-known syntactic
restriction in order to preserve decidability: they do not allow to use non-simple
roles – that is, transitive roles or their super-roles – in number restrictions.
When modeling composite objects, for example in bio-medical ontologies, this
restriction can pose problems.
Therefore, we take a closer look at the problem of counting over non-simple
roles. On the one hand, we sharpen the known undecidability results and demonstrate
that: (i) for DLs with inverse roles, counting over non-simple roles leads
to undecidability even when there is only one role in the language; (ii) for DLs
without inverses, two transitive and an arbitrary role are sufficient for undecidability.
On the other hand, we demonstrate that counting over non-simple roles
does not compromise decidability in the absence of inverse roles provided that
certain restrictions on role inclusion axioms are satisfied.
E.Z.: In short:
• unrestricted SIQ and even SIN with TBoxes
with even one role are undecidable;
• unrestricted SHQ and even SHN with TBoxes
with just three roles (and a special RBox) are undecidable;
• SHQ with TBoxes is decidable for a large family of RBoxes.
So the question is: In your ontology, do you use a “safe” RBox,
i.e., which does not destroy decidability?
In
Nachum Dershowitz and Andrei Voronkov, editors,
Proc. of
the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning,LPAR 2007,Yerevan, Armenia, October 15-19, 2007.LNAI,
vol. 4790,
pp. 303-317, Springer, 2007.
@article{Kozen1983,
author = {Dexter Kozen},
title = {Results on the propositional $\mu$-calculus},
journal = {Theoretical Computer Science, Special Issue:
9th Int.\ Colloquium on Automata, Languages and Programming (ICALP'82)},
volume = {27},
number = {3},
year = {1983},
pages = {333--354},
doi = {10.1016/0304-3975(82)90125-6},
ee = {http://dx.doi.org/10.1016/0304-3975(82)90125-6}
}
In this paper we define and study a propositional μ-calculus Lμ,
which consists essentially of propositional modal logic with a least fixpoint operator.
Lμ is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL).
For a restricted version we give an exponential-time decision procedure, small model property,
and complete deductive system, thereby subsuming the corresponding results for PDL.
Theoretical Computer Science,
Special Issue:
9th Int. Colloquium on Automata, Languages and Programming,ICALP'82,
Aarhus, Denmark, July 12 – 16, 1982,
27(3):333–354, 1983.
A finite model theorem for the propositional μ-calculus
[ pdf |
]
@article{Kozen1988,
author = {Dexter Kozen},
title = {A finite model theorem for the propositional $\mu$-calculus},
journal = {Studia Logica},
volume = {47},
number = {3},
year = {1988},
pages = {233--241},
doi = {10.1007/BF00370554},
ee = {http://dx.doi.org/10.1007/BF00370554}
}
We prove a finite model theorem and infinitary completeness result for
the propositional μ-calculus. The construction establishes a link between finite
model theorems for propositional program logics and the theory of well-quasi-orders.
@inproceedings{KupfSatVardi2002,
author = {Orna Kupferman and Ulrike Sattler and Moshe Y. Vardi},
title = {The complexity of the graded $\mu$-calculus},
pages = {423--437},
editor = {Andrei Voronkov},
booktitle = {Proc.\ of the 18th Int.\ Conf.\ on Automated Deduction (CADE-18)},
series = {Lecture Notes in Computer Science},
volume = {2392},
publisher = {Springer},
year = {2002},
doi = {10.1007/3-540-45620-1_34},
ee = {http://dx.doi.org/10.1007/3-540-45620-1_34}
}
In classical logic, existential and universal quantifiers express that there
exists at least one individual satisfying a formula, or that all individuals satisfy a formula.
In many logics, these quantifiers have been generalized to express that, for a
non-negative integer n, at least n individuals or all but n individuals satisfy a formula.
In modal logics, graded modalities generalize standard existential and universal
modalities in that they express, e.g., that there exist at least n accessible worlds
satisfying a certain formula. Graded modalities are useful expressive means in knowledge
representation; they are present in a variety of other knowledge representation
formalisms closely related to modal logic.
A natural question that arises is how the generalization of the existential and universal
modalities affects the decidability problem for the logic and its computational
complexity, especially when the numbers in the graded modalities are coded in binary.
In this paper we study the graded μ-calculus, which extends graded modal
logic with fixed-point operators, or, equivalently, extends classical μ-calculus with
graded modalities. We prove that the decidability problem for graded μ-calculus is
ExpTime-complete – not harder than the decidability problem for μ-calculus, even
when the numbers in the graded modalities are coded in binary.
E.Z.: In short, graded μ-calculus is ExpTime-complete, hence so is μALCQ .
A lower complexity bound for Propositional Dynamic Logic with intersection
[ pdf |
ps.zip |
]
@inproceedings{LangeEXPSPACE,
author = {Martin Lange},
title = {A lower complexity bound for Propositional Dynamic Logic with intersection},
pages = {133--147},
editor = {Renate A. Schmidt and Ian Pratt-Hartmann and
Mark Reynolds and Heinrich Wansing},
booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Advances in Modal Logic (AiML 2004)},
publisher = {King's College Publications},
year = {2005},
ee = {http://www.aiml.net/volumes/volume5/Lange.ps}
}
This paper shows that satisfiability for Propositional Dynamic Logic
with intersection is ExpSpace-hard. The proof uses a reduction from
the word problem for alternating, exponential time bounded Turing machines.
In
Renate Schmidt,
Ian Pratt-Hartmann,
Mark Reynolds, and
Heinrich Wansing, editors,
Proc. of
Advances in Modal Logic, Volume 5,AiML 2004,University of Manchester, UK, September 9-11, 2004.
pp. 133–147, King's College Publications, 2005.
2-ExpTime lower bounds for Propositional Dynamic Logics with intersection
[ ps.zip |
]
@article{LangeLutz2005,
author = {Martin Lange and Carsten Lutz},
title = {{2-ExpTime} lower bounds for Propositional Dynamic Logics with intersection},
journal = {Journal of Symbolic Logic},
volume = {70},
number = {4},
year = {2005},
pages = {1072--1086},
doi = {10.2178/jsl/1129642115},
ee = {http://dx.doi.org/10.2178/jsl/1129642115}
}
In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL)
extended with an intersection operator on programs, is decidable in deterministic double exponential time.
Since then, the exact complexity of IPDL has remained an open problem: the best known lower
bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness.
In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete.
We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted
on tree structures.
E.Z.: In short, IPDL and hence ALC (∩,∪,o,*,id) is 2ExpTime-complete.
An improved NExpTime-hardness result for description logic ALC
extended with inverse roles, nominals, and counting
[ ps.zip |
]
@techreport{LutzImproved2004,
author = {Carsten Lutz},
title = {An improved {NExpTime}-hardness result for description logic
$\mathcal{ALC}$ extended with inverse roles, nominals, and counting},
type = {LTCS-Report},
number = {05-05},
institution = {Chair for Automata Theory, Institute for Theoretical Computer Science,
Dresden University of Technology},
address = {Dresden, Germany},
year = {2005}
}
The Description Logic (DL) ALCIO extends the basic propositionally closed DL ALC
with inverse roles and nominals. Reasoning with ALCIO concept descriptions is ExpTime-complete,
and the same holds for reasoning in ALCIO with general TBoxes (aka GCIs)
since TBoxes can be “internalized”:
reasoning with general TBoxes can be polynomially reduced to reasoning with concept descriptions.
It is well-known that the complexity of reasoning increases if ALCIO is extended with
counting constructors: Tobies considers ALCIO extended with a concept constructor
(≤ 1 r) and proves that reasoning in the resulting DL is NExpTime-complete, both with concept descriptions
and with general TBoxes. For his reduction, it is crucial that the constructor (≤ 1 r) can be applied
both to atomic roles and to inverse roles. In this paper, we strengthen Tobies' result by proving NExpTime-hardness
of reasoning in the description logic ALCFIO , which is obtained from ALCIO by adding
an additional sort of roles which are interpreted as partial functions. Thus, in our formalism we can only count
on roles “in one direction”, while Tobies' proof requires counting in both direction.
Just as in Tobies' case, our proof is by reduction of a NExpTime-complete variant of the domino problem.
However, our reduction strategy is quite different from the one used by Tobies.
E.Z.: In short, ALCFIO is NExpTime-complete, even with numbers coded in binary,
and even with inverse roles not used in number restrictions.
LTCS-Report 04-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology,
Germany, 2004.
PDL with intersection and converse is decidable
[ ps.zip |
]
@inproceedings{LutzICPDL2005,
author = {Carsten Lutz},
title = {{PDL} with intersection and converse is decidable},
pages = {413--427},
editor = {C.-H. Luke Ong},
booktitle = {Proc.\ of the 19th Int.\ Workshop on Computer Science Logic (CSL 2005),
14th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)},
series = {Lecture Notes in Computer Science},
volume = {3634},
publisher = {Springer},
year = {2005},
doi = {10.1007/11538363_29},
ee = {http://dx.doi.org/10.1007/11538363_29}
}
In its many guises and variations, propositional dynamic logic (PDL) plays an important rôle
in various areas of computer science such as databases, artificial intelligence, and computer linguistics.
One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse.
However, although ICPDL has several interesting applications, its computational properties have never
been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the
monadic second order logic of infinite trees. Our result has applications in information logic,
description logic, and epistemic logic. In particular, we solve a long-standing open problem in
information logic. Another virtue of our approach is that it provides a decidability proof that
is more transparent than existing ones for PDL with intersection (but without converse).
E.Z.: In short, ICPDL and hence ALCI (∩,∪,o,*,id) is decidable.
In
Proc. of
the 14th Annual Conference of the European Association for Computer Science Logic,CSL 2005,Oxford, UK, August 22-25, 2005,LNCS.
vol. 3634,
pp. 413-427, Springer, 2005.
@article{LutzArecHorSat2004,
author = {Carsten Lutz and Carlos Areces and Ian Horrocks and Ulrike Sattler},
title = {Keys, nominals, and concrete domains},
journal = {Journal of Artificial Intelligence Research},
volume = {23},
year = {2004},
pages = {667--726},
doi = {10.1613/jair.1542},
ee = {http://dx.doi.org/10.1613/jair.1542}
}
Many description logics (DLs) combine knowledge representation on an abstract, logical
level with an interface to “concrete” domains like numbers and strings with built-in predicates
such as <, +, and prefix-of. These hybrid DLs have turned out to be useful in
several application areas, such as providing the basis for expressive ontology languages.
We propose to further extend such DLs with key constraints that allow the expression of
statements like “US citizens are uniquely identified by their social security number”.
Based on this idea, we introduce a number of natural description logics and perform a detailed
analysis of their decidability and computational complexity. It turns out that naïve extensions
with key constraints easily lead to undecidability, whereas more careful extensions
yield NExpTime-complete DLs for a variety of useful concrete domains.
LTCS-Report 02-04,
Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology,
Germany, 2002.
The complexity of reasoning with Boolean modal logics
[ ps.zip |
]
@inproceedings{LutzSattler2001,
author = {Carsten Lutz and Ulrike Sattler},
title = {The complexity of reasoning with {B}oolean modal logics},
pages = {329--348},
editor = {Frank Wolter and Heinrich Wansing and
Maarten de Rijke and Michael Zakharyaschev},
booktitle = {Proc.\ of the 3rd Int.\ Conf.\ on Advances in Modal Logic (AiML~2000)},
publisher = {World Scientific},
year = {2002}
}
In this paper, we investigate the complexity of reasoning with various Boolean Modal Logics.
The main results are that
(i) adding negation of modal parameters to (multi-modal) K makes reasoning ExpTime-complete
and
(ii) adding atomic negation and conjunction to K even yields a NExpTime-complete logic.
The last result is relativized by the fact that it depends on an infinite
number of modal parameters to be available. If the number of modal parameters is bounded,
full Boolean Modal Logic becomes ExpTime-complete.
The complexity of finite model reasoning in Description Logics
[ pdf |
]
@article{LutzSattlerTendera2005,
author = {Carsten Lutz and Ulrike Sattler and Lidia Tendera},
title = {The complexity of finite model reasoning in Description Logics},
journal = {Information and Computation},
volume = {199},
number = {1--2},
year = {2005},
pages = {132--171},
doi = {10.1016/j.ic.2004.11.002},
ee = {http://dx.doi.org/10.1016/j.ic.2004.11.002}
}
We analyse the complexity of finite model reasoning in the description logic ALCQI ,
i.e., ALC augmented
with qualifying number restrictions, inverse roles, and general TBoxes. It turns out that all relevant reasoning
tasks such as concept satisfiability and ABox consistency are ExpTime-complete, regardless of whether the
numbers in number restrictions are coded unarily or binarily.
Thus, finite model reasoning with ALCQI is
not harder than standard reasoning with ALCQI .
Modal Logic and the two-variable fragment
[ pdf |
]
@inproceedings{LutzSattlerWolter2001,
author = {Carsten Lutz and Ulrike Sattler and Frank Wolter},
title = {Modal Logic and the two-variable fragment},
pages = {247--261},
editor = {Laurent Fribourg},
booktitle = {Proc.\ of the 15th Int.\ Workshop on Computer Science Logic (CSL 2001),
10th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)},
series = {Lecture Notes in Computer Science},
volume = {2142},
publisher = {Springer},
year = {2001},
doi = {10.1007/3-540-44802-0_18},
ee = {http://dx.doi.org/10.1007/3-540-44802-0_18}
}
We introduce a modal language L which is obtained from standard modal logic by adding the Boolean operators
on accessibility relations, the identity relation, and the converse of relations.
It is proved that L has the same expressive power as the two-variable fragment
FO2 of first-order logic, but speaks less succinctly about relational structures:
if the number of relations is bounded, then L-satisfiability is ExpTime-complete
but FO2 satisfiability is NExpTime-complete.
We indicate that the relation between L and FO2 provides
a general framework for comparing modal and temporal languages with first-order languages.
E.Z.: In short, ALCI (∩,∪,¬,id)
is ExpTime-complete (and as expressive as FO2).
Proc. of
the 10th Annual Conference of the European Association for Computer Science Logic,CSL 2001,Paris, France, September 10-13, 2001.LNCS,
vol. 2142,
pp.247-261, Springer, 2001.
@article{LutzWalther2004,
author = {Carsten Lutz and Dirk Walther},
title = {{PDL} with negation of atomic programs},
journal = {Journal of Applied Non-Classical Logics},
volume = {15},
number = {2},
year = {2005},
pages = {189--214},
doi = {10.3166/jancl.15.189-213},
ee = {http://dx.doi.org/10.3166/jancl.15.189-213}
}
Propositional dynamic logic (PDL) is one of the most successful variants of modal logic.
To make it even more useful for applications, many extensions of PDL have been considered in the literature.
A very natural and useful such extension is with negation of programs. Unfortunately, as long-known,
reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL
with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context
of Description Logics, and prove that satisfiability is decidable and ExpTime-complete using an approach
based on Büchi tree automata.
In
Proc. of
the 2nd Int. Joint Conf. on Automated Reasoning,IJCAR 2004,Cork, Ireland, July 4-8, 2004.LNAI,
vol. 3097,
pp. 259–273, Springer, 2004.
Decision procedures for expressive Description Logics with intersection,
composition, converse of roles and role identity
[ pdf |
]
@inproceedings{Massacci2001,
author = {Fabio Massacci},
title = {Decision procedures for expressive Description Logics with intersection,
composition, converse of roles and role identity},
pages = {193--198},
editor = {Bernhard Nebel},
booktitle = {Proc.\ of the 17th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~2001)},
publisher = {Morgan Kaufmann},
year = {2001}
}
In the quest for expressive description logics for real-world applications, a powerful combination of
constructs has so far eluded practical decision procedures: intersection and composition of roles.
We propose tableau-based decision procedures for the satisfiability of logics extending ALC with the
intersection, composition, union, converse of roles and role identity. We show that
1. the satisfiability of ALC (∩,∪,o), for which a
2-ExpTime upper bound was given by tree-automata techniques, is PSpace-complete;
2. the satisfiability of ALCI (∩,∪,o,id), an
open problem so far, is in NExpTime.
In
Proc. of
the 17th Int. Joint Conf. on Artificial Intelligence,IJCAI 2001,Seattle, Washington, USA, August 4-10, 2001,pp. 193-198, Morgan Kaufmann, 2001.
Complexity results for first-order two-variable logic with counting
[ pdf |
ps.zip |
]
@article{Pacholski_etal_2000,
author = {Leszek Pacholski and Wieslaw Szwast and Lidia Tendera},
title = {Complexity results for first-order two-variable logic with counting},
journal = {SIAM Journal on Computing},
volume = {29},
year = {2002},
pages = {1083--1117},
doi = {10.1137/S0097539797323005},
ee = {http://dx.doi.org/10.1137/S0097539797323005}
}
Let Cp2 denote the class of first-order sentences with two variables
and with additional quantifiers “there exists exactly (at most, at least) i”,
for i≤p, and let C2 be the union of
Cp2 taken over all integers p.
We prove that the satisfiability problem for C12
sentences is NExpTime-complete.
This strengthens the results by Grädel, Kolaitis, and Vardi [15],
who showed that the satisfiability problem for the first-order two-variable logic
L2 is NExpTime-complete and by Grädel, Otto, and Rosen [16],
who proved the decidability of C2.
Our result easily implies that the satisfiability problem for C2 is
in nondeterministic, doubly exponential time.
It is interesting that C12 is in NExpTime in spite of the fact that
there are sentences whose minimal (and only) models are of doubly exponential size.
It is worth noticing that by a recent result of
E. Grädel, M. Otto, and E. Rosen [17], extensions of two-variable logic
L2 by a weak access to cardinalities through the
Härtig (or equicardinality) quantifier is undecidable.
The same is true for extensions of L2 by very weak forms of recursion.
The satisfiability problem for logics with a bounded number of variables has applications in artificial intelligence,
notably in modal logics, where counting comes in the context of graded modalities,
and in description logics, where counting can be used to express so-called number restrictions.
[15] E. Grädel, Ph. Kolaitis, and M. Vardi,
On the decision problem for two-variable first-order logic.
Bull. Symbolic Logic, 3 (1997), pp. 53–69.
[16] E. Grädel, M. Otto, and E. Rosen,
Two-variable logic with counting is decidable.
Proc. of the 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 306–317.
[17] E. Grädel, M. Otto, and E. Rosen,
Undecidability results on two-variables logics.
Proc. of the 14th Annual Symposium on Theoretical Aspects of Computer Science,
LNCS, vol. 1200, Springer, Berlin, 1997.
SIAM Journal on Computing
(SICOMP),
vol. 29, pp. 1083-1117, 2000.
Its Section 4 was presented at the conference:
Complexity of two-variable logic with counting
[ pdf ]
In
Proc. of
the 12th IEEE Symposium on Logic in Computer Science,LICS'97,Warsaw, Poland, June 29 – July 2, 1997,pp.318-327, IEEE Computer Society Press, 1997.
Reasoning in the SHOQ (Dn) Description Logic
[ pdf |
]
@inproceedings{PanHorrSHOQDn,
author = {Jeff Z. Pan and Ian Horrocks},
title = {Reasoning in the $\mathcal{SHOQ}(D_n)$ Description Logic},
pages = {53--62},
editor = {Ian Horrocks and Sergio Tessaris},
booktitle = {Proc.\ of the 15th Int.\ Workshop on Description Logics (DL~2002)},
series = {CEUR Workshop Proceedings},
volume = {53},
publisher = {CEUR-WS.org},
year = {2002},
ee = {http://ceur-ws.org/Vol-53/Pan-Horrocks-shoqdn-2002.ps}
}
Description Logics (DLs) are of crucial importance to the development of the Semantic Web,
where their rôle is to provide formal underpinnings and automated reasoning
services for Semantic Web ontology languages such as DAML+OIL. In this paper we
show how the description logic
SHOQ (D),
which has been designed to provide such
services, can be extended with n-ary datatype predicates as well as datatype number restrictions,
to give SHOQ (Dn),
and we present an algorithm for deciding the satisfiability
of SHOQ (Dn) concepts,
along with a proof of its soundness and completeness. The work
is motivated by the requirement for n-ary datatype predicates in relation to
“real world”
properties such as size, weight and duration, in the Semantic Web applications.
@inproceedings{Pratt1979,
author = {Vaughan R. Pratt},
title = {Models of program logics},
pages = {115--122},
booktitle = {Proc.\ of the 20th Annual Symposium on
Foundations of Computer Science (FoCS~'79)},
publisher = {IEEE Computer Society},
year = {1979},
doi = {10.1109/SFCS.1979.24},
ee = {http://dx.doi.org/10.1109/SFCS.1979.24}
}
We briefly survey the major proposals for models of programs and show that
they all lead to the same propositional theory of programs.
Methods of algebraic logic dominate in the proofs.
One of the connections made between the models,
that involving language models, is quite counterintuitive.
The common theory has already been shown to be complete in deterministic exponential time;
we give here a simpler proof of the upper bound.
Complexity of the two-variable fragment with counting quantifiers
[ pdf |
]
@article{PrattHartmann_2005,
author = {Ian Pratt-Hartmann},
title = {Complexity of the two-variable fragment with counting quantifiers},
journal = {Journal of Logic, Language, and Information},
volume = {14},
number = {3},
year = {2005},
pages = {369--395},
doi = {10.1007/s10849-005-5791-1},
ee = {http://dx.doi.org/10.1007/s10849-005-5791-1}
}
The satisfiability and finite satisfiability problems for the two-variable fragment of first-order
logic with counting quantifiers are both in NExpTime, even when counting quantifiers are coded succinctly.
@article{MdeRijke2000Graded,
author = {Maarten de Rijke},
title = {A note on graded modal logic},
journal = {Studia Logica},
volume = {64},
number = {2},
year = {2000},
pages = {271--283},
doi = {10.1007/s10849-005-5791-1},
ee = {http://dx.doi.org/10.1007/s10849-005-5791-1}
}
We introduce a notion of bisimulation for graded modal logic.
Using these bisimulations the model theory of graded modal logic can be developed in a uniform manner.
We illustrate this by establishing the finite model property, and proving invariance and definability results.
Undecidability and nonperiodicity of tilings on the plane
[ pdf |
]
@article{Robinson1971,
author = {Raphael Robinson},
title = {Undecidability and nonperiodicity of tilings on the plane},
journal = {Inventiones Mathematicae},
volume = {12},
number = {3},
year = {1971},
pages = {177--209},
doi = {10.1007/BF01418780},
ee = {http://dx.doi.org/10.1007/BF01418780}
}
The three main objectives of the paper, and the relevant sections, are as follows.
(a) Proof that the six polygonal tiles shown on Fig. 1 allow only nonperiodic tilings of the plane.
The same result is obtained for the closely related set of ten tiles.
(b) Proof that there is a set of 36 square tiles with colored edges for
which the completion problem is undecidable, translation only being used.
By the completion problem is meant the problem of deciding whether
an arbitrary finite partial tiling of the plane can be completed.
(c) Simplified proof of Berger's theorem that the plane tiling problem is undecidable.
@inproceedings{SattlerVardi2001,
author = {Ulrike Sattler and Moshe Y. Vardi},
title = {The hybrid $\mu$-calculus},
pages = {76--91},
editor = {Rajeev Gor{\'e} and Alexander Leitsch and Tobias Nipkow},
booktitle = {Proc.\ of the 1st Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2001)},
series = {Lecture Notes in Computer Science},
volume = {2083},
publisher = {Springer},
year = {2001},
doi = {10.1007/3-540-45744-5_7},
ee = {http://dx.doi.org/10.1007/3-540-45744-5_7}
}
We present an ExpTime decision procedure for the full μ-calculus
(including converse programs) extended with nominals and a
universal program, thus devising a new, highly expressive ExpTime logic.
The decision procedure is based on tree automata, and makes explicit the
problems caused by nominals and how to overcome them. Roughly speaking,
we show how to reason in a logic lacking the tree model property
using techniques for logics with the tree model property. The contribution
of the paper is two-fold: we extend the family of ExpTime logics,
and we present a technique to reason in the presence of nominals.
E.Z.: In short,
μ-calculus with converse programs, universal program and nominals is in ExpTime,
and hence ExpTime-complete (since μ-calculus is ExpTime-hard).
Hence, concept satisfiability in μALCIO is ExpTime-complete
(even with general TBoxes, which are internalizable in presence of μ).
In
R. Gore, A. Leitsch, and T. Nipkow, editors,
Proc. of
the 1st Int. Joint Conf. on Automated Reasoning,IJCAR 2001,Siena, Italy, June 18-23, 2001.LNAI,
vol. 2083,
pp. 76–91, Springer, 2001.
Reasoning with individuals in concept languages
[ pdf |
ps.zip |
]
@article{Schaerf1994b,
author = {Andrea Schaerf},
title = {Reasoning with individuals in concept languages},
journal = {Data and Knowledge Engineering},
volume = {13},
number = {2},
year = {1994},
pages = {141--176},
doi = {10.1016/0169-023X(94)90002-7},
ee = {http://dx.doi.org/10.1016/0169-023X(94)90002-7}
}
One of the main characteristics of knowledge representation systems based on the description of concepts
is the clear distinction between terminological and assertional knowledge. Although this characteristic
leads to several computational and representational advantages, it usually limits the expressive power
of the system. For this reason, some attempts have been done, allowing for a limited form of
amalgamation between the two components and a more complex interaction between them.
In particular, one of these attempts is based on letting the individuals to be referenced
in the concept expressions. This is generally performed by admitting a constructor for building
a concept from a set of enumerated individuals.
In this paper we investigate on the consequences of introducing constructors of this type in
the concept description language. We also provide a complete reasoning procedure to deal
with these constructors and we obtain some complexity results on it.
A correspondence theory for terminological logics: Preliminary report
[ pdf |
ps.zip |
]
@inproceedings{Schild1991,
author = {Klaus Schild},
title = {A correspondence theory for terminological logics: {P}reliminary report},
pages = {466--471},
editor = {John Mylopoulos and Raymond Reiter},
booktitle = {Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~1991)},
publisher = {Morgan Kaufmann},
year = {1991}
}
We show that the terminological logic ALC comprising Boolean operations
on concepts and value restrictions is a notational variant of the propositional
modal logic K(m).
To demonstrate the utility of the correspondence, we give
two of its immediate by-products. Namely, we axiomatize ALC and give a
simple proof that subsumption in ALC is PSpace-complete, replacing the
original six-page one.
Furthermore, we consider an extension of ALC additionally containing
both the identity role and the composition, union, transitive-reflexive closure,
range restriction, and inverse of roles. It turns out that this language, called
TSL , is a notational variant of the propositional dynamic logic converse-PDL.
Using this correspondence, we prove that it suffices to consider finite
TSL -models, show that TSL -subsumption is decidable,
and obtain an axiomatization of TSL .
By discovering that features correspond to deterministic programs in dynamic logic,
we show that adding them to TSL preserves decidability, although violates
its finite model property. Additionally, we describe an algorithm for deciding
the coherence of inverse-free TSL -concepts with features.
Finally, we prove that universal implications can be expressed within TSL .
E.Z.: Note that TSL is now known as ALCIreg. In short,
• ALC ≅ K(m),
• ALCIreg ≅ converse-PDL,
• ALCIFreg ≅ deterministic converse-PDL,
• ALCIreg has FMP,
• ALCIFreg lacks FMP.
@techreport{Schild1989,
author = {Klaus Schild},
title = {Towards a theory of frames and rules},
type = {KIT-Report},
number = {76},
institution = {Fachbereich Informatik, Technische Universit{\"a}t Berlin},
address = {Berlin, Germany},
year = {1989}
}
A term definition language very similar to the terminological part of BACK
is enriched with Horn-like rules and disjointness restrictions built up from
arbitrary concepts possibly involving syntactic or semantic cycles.
The resulting hybrid language is given a weak semantics which captures
the inferences expected intuitively and allows for representing some kind of procedural knowledge.
The weak semantics used is based on model theoretic grounds and, even more important,
allows to prove properties of the language very easily.
Moreover an algorithm is developed which is sound and and complete
with respect to the weak semantics and can be characterized
to be polynomially time bound for non-pathological cases.
@inproceedings{SchmidtSchauBKLONE89,
author = {Manfred Schmidt-Schau{\ss}},
title = {Subsumption in {KL-ONE} is undecidable},
pages = {421--431},
editor = {Ronald J. Brachman and Hector J. Levesque and Raymond Reiter},
booktitle = {Proc.\ of the 1st Int.\ Conf.\ on the Principles of
Knowledge Representation and Reasoning (KR'89)},
publisher = {Morgan Kaufmann},
year = {1989}
}
It is shown that in the frame-based language KL-ONE it is
undecidable whether one concept is subsumed by another concept. In
fact a rather small sublanguage of KL-ONE called ALR is used which
has only the concept forming operators conjunction, value restriction,
and role value maps using only “=”. In particular, number restrictions
are not used. The language ALR can be viewed as an extension of feature
terms without complements and unions, where features have sets
as values instead of elements. Our result shows that there is a basic
difference between feature terms and KL-ONE, since the complexity of
subsumption switches from quasi-linear to undecidable if the restriction
is dropped that roles are functional.
In
Proc. of
the 1st Int. Conf. on the Principles of Knowledge Representation and Reasoning,KR'89,Toronto, Ontario, Canada, May 15-18, 1989.pp. 421–431, Morgan Kaufmann, 1989.
Attributive concept descriptions with complements
[ pdf |
]
@article{SchmidtSchauBSmolka1991,
author = {Manfred Schmidt-Schau\ss and Gert Smolka},
title = {Attributive concept descriptions with complements},
journal = {Artificial Intelligence},
volume = {48},
number = {1},
year = {1991},
pages = {1--26},
doi = {10.1016/0004-3702(91)90078-X},
ee = {http://dx.doi.org/10.1016/0004-3702(91)90078-X}
}
We investigate the consequences of adding unions and complements to attributive concept
descriptions employed in terminological knowledge representation languages. It is shown
that deciding coherence and subsumption of such descriptions are PSpace-complete
problems that can be decided with linear space.
An automata theoretic decision procedure for the propositional μ-calculus
[ pdf |
]
@article{StreettEmerson1989,
author = {Robert S. Streett and E. Allen Emerson},
title = {An automata theoretic decision procedure for the propositional $\mu$-calculus},
journal = {Information and Computation},
volume = {81},
number = {3},
year = {1989},
pages = {249--264},
doi = {10.1016/0890-5401(89)90031-X},
ee = {http://dx.doi.org/10.1016/0890-5401(89)90031-X}
}
The propositional μ-calculus is a propositional
logic of programs which incorporates a least fixpoint
operator and subsumes the Propositional Dynamic Logic of
Fischer and Ladner, the infinite looping construct of
Streett, and the Game Logic of Parikh. We give an elementary
time decision procedure, using a reduction to the emptiness
problem for automata on infinite trees. A small model
theorem is obtained as a corollary.
Proc. of
the 11th Int. Colloquium on Automata, Languages and Programming,ICALP'84,Antwerp, Belgium, July 16-20, 1984.LNCS,
vol. 172,
pp. 465–472, Springer, 1984.
The complexity of reasoning with cardinality restrictions and nominals in expressive Description Logics
[ pdf |
]
@article{Tobies2000,
author = {Stephan Tobies},
title = {The complexity of reasoning with cardinality restrictions
and nominals in expressive Description Logics},
journal = {Journal of Artificial Intelligence Research},
volume = {12},
year = {2000},
pages = {199--217},
doi = {10.1613/jair.705},
ee = {http://dx.doi.org/10.1613/jair.705}
}
We study the complexity of the combination of the Description Logics
ALCQ and ALCQI
with a terminological formalism based on cardinality restrictions on concepts. These
combinations can naturally be embedded into C2,
the two variable fragment of predicate logic with counting quantifiers,
which yields decidability in NExpTime. We show that this approach leads
to an optimal solution for ALCQI , as ALCQI
with cardinality restrictions has the same complexity as
C2 (NExpTime-complete). In contrast, we show that for ALCQ ,
the problem can be solved in ExpTime. This result is obtained by a reduction of
reasoning with cardinality restrictions to reasoning with the (in general weaker) terminological
formalism of general axioms for ALCQ extended with nominals.
Using the same reduction, we show that, for the extension of ALCQI with nominals,
reasoning with general axioms is a NExpTime-complete problem.
Finally, we sharpen this result and show that pure concept satisfiability for
ALCQI with nominals is NExpTime-complete. Without nominals,
this problem is known to be PSpace-complete.
The taming of converse: Reasoning about two-way computations
[ pdf |
]
@inproceedings{Vardi1985,
author = {Moshe Y. Vardi},
title = {The taming of converse: {R}easoning about two-way computations},
pages = {413--424},
editor = {Rohit Parikh},
booktitle = {Proc.\ of the 5th Workshop on Logics of Programs},
series = {Lecture Notes in Computer Science},
volume = {193},
publisher = {Springer},
year = {1985},
doi = {10.1007/3-540-15648-8_31},
ee = {http://dx.doi.org/10.1007/3-540-15648-8_31}
}
We consider variants of propositional dynamic logic (PDL) augmented with the converse construct.
Intuitively, the converse α— of a program α
is a programs whose semantics is to run a backwards.
While PDL consists of assertions about weakest preconditions, the converse construct
enable us to make assertions about strongest postconditions. We investigate the interaction
of converse with two constructs that deal with infinite computations: loop and repeat.
We show that converse-loop-PDL is decidable in exponential time, and converse-repeat-PDL is
decidable in nondeterministic exponential time.
Reasoning about the past with two-way automata
[ pdf |
]
@inproceedings{Vardi1998,
author = {Moshe Y. Vardi},
title = {Reasoning about the past with two-way automata},
pages = {628--641},
editor = {Kim G. Larsen and Sven Skyum and Glynn Winskel},
booktitle = {Proc.\ of the 25th Int.\ Colloquium on Automata,
Languages and Programming (ICALP'98)},
series = {Lecture Notes in Computer Science},
volume = {1443},
publisher = {Springer},
year = {1998},
doi = {10.1007/BFb0055090},
ee = {http://dx.doi.org/10.1007/BFb0055090}
}
The μ-calculus can be viewed as essentially the “ultimate”
program logic, as it expressively subsumes all propositional program logics,
including dynamic logics, process logics, and temporal logics. It is
known that the satisfiability problem for the μ-calculus is ExpTime-complete.
This upper bound, however, is known for a version of the logic
that has only forward modalities, which express weakest preconditions,
but not backward modalities, which express strongest postconditions.
Our main result in this paper is an exponential time upper bound for the
satisfiability problem of the μ-calculus with both forward and backward
modalities. To get this result we develop a theory of two-way alternating
automata on infinite trees.
E.Z.: In short: the converse μ-calculus is ExpTime-complete.
Hence, so is concept satisfiability in μALCI.
In
Proc. of
the 25th Int. Colloquium on Automata, Languages and Programming,ICALP'98,Aalborg, Denmark, July 13-17, 1998.LNCS,
vol. 1443,
pp. 628–641, Springer, 1998.
Obstacles on the way to qualitative spatial reasoning with Description Logics: some undecidability results
[ pdf |
]
@inproceedings{WesselDL2001,
author = {Michael Wessel},
title = {Obstacles on the way to qualitative spatial reasoning with
Description Logics: {S}ome undecidability results},
pages = {122--131},
editor = {Carole Goble and Deborah L. McGuinness and
Ralf M{\"o}ller and Peter F. Patel-Schneider},
booktitle = {Proc.\ of the 14th Int.\ Workshop on Description Logics (DL~2001)},
series = {CEUR Workshop Proceedings},
volume = {49},
publisher = {CEUR-WS.org},
year = {2001},
ee = {http://ceur-ws.org/Vol-49/Wessel-122start.ps}
}
We summarize the results we obtained on the extensions of ALC
with composition-based role inclusion axioms of the form
SoT ⊆ R1∪...∪Rn.
A set of these role axioms is called a role box.
The original motivation for this work was to develop a description logic suitable for
qualitative spatial reasoning problems. We quickly define and discuss the DLs
ALCRA ,
ALCRA(–),
ALCRASG ,
and
ALCNRASG .
All but
ALCRASG
are shown to be undecidable, and
ALCRASG
is of limited utility, even though it is still
as expressive as
ALCR+ .
ALCRASG
has shown to be ExpTime-complete,
due to associativity of role boxes,
which is an important requirement.
In
Proc. of
the 2001 Int. Workshop on Description Logics,DL 2001,Stanford University, California, USA, August 1-3, 2001,vol. 49 in CEUR,
pp. 122–131, 2001.
There are three accompanying technical reports:
Obstacles on the way to spatial reasoning with Description Logics:
undecidability of ALCRA(–)
[ pdf ]
Technical Report FBI-HH-M-297/00, University of Hamburg, Computer Science Department,
October 2000.
Decidable and undecidable extensions of ALC with composition-based role inclusion axioms
[ pdf ]
Technical Report FBI-HH-M-301/01, University of Hamburg, Computer Science Department,
December 2000.