Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
1999
Edoardo Ardizzone and Mohand-Said Hacid.
A Semantic Modeling Approach for Video Retrieval by
Content.
In Proceedings of the IEEE International Conference on Multimedia Computing
and Systems, Florence, Italy, volume 2, pages 158–162. IEEE Computer
Society, June 1999.
Bibtex entry Paper (PS)
Abstract
A knowledge-based approach to model and retrieve video data by content is developed. Selected
objects of interest in a video sequence are described and stored in a database. This database
forms the object layer. On top of this layer, we define the schema layer used to capture the
structured abstractions of the objects stored in the object layer. We propose two abstract
languages on the basis of description logics: one for describing the contents of these layers,
and the other, more expressive, for making queries. The query language provides possibilities
for navigation of the schema through forward and backward traversal of links, sub-setting of
attributes, and constraints on links.
A. Artale and C. Lutz.
A Correspondance between Temporal Description Logics.
In Patrick Lambrix, Alex Borgida, Maurizio Lenzerini, Ralf Möller, and
Peter Patel-Schneider, editors, Proceedings of the International Workshop
on Description Logics (DL'99), number 22 in CEUR-WS, pages 145–149,
Linkoeping, Sweden, July 30 – August 1 1999. Linköping University.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/.
Bibtex entry Paper (PS)
Abstract
Description Logics (DLs) are formalisms for representing and reasoning about
conceptual knowledge. There exist several extensions of DLs for an
appropriate integration of temporal knowledge. This
paper investigates the relation between the two DLs
TL-ALCF and
ALCF(D). TL-ALCF is an interval-based, temporal DL
for reasoning about objects whose properties vary over time. ALCF(D) is a
logic for integrated reasoning about conceptual and so-called concrete
knowledge. If instantiated with a ``temporal'' concrete domain, ALCF(D) is
well-suited for reasoning about temporal objects, i.e., objects which have a
unique temporal extension. This paper is a first attempt to clarify the
relationship between this two formalisms. It is showed that satisfiability of
TL-ALCF concepts can be reduced to satisfiability of ALCF(D) concepts. This
allows to use the available ALCF(D) tableau calculus for reasoning with
TL-ALCF. Furthermore, it allows to settle the complexity of satisfiability of
TL-ALCF concepts, which was previously unknown.
F. Baader.
Logic-Based Knowledge Representation.
In M.J. Wooldridge and M. Veloso, editors, Artificial Intelligence Today,
Recent Trends and Developments, number 1600 in Lecture Notes in Computer
Science, pages 13–41. Springer Verlag, 1999.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
After a short analysis of the requirements that a knowledge representation
language must satisfy, we introduce Description Logics, Modal Logics, and
Nonmonotonic Logics as formalisms for representing terminological
knowledge, time-dependent or subjective knowledge, and incomplete knowledge
respectively.
At the end of each section, we briefly comment on the connection to
Logic Programming.
F. Baader and R. Küsters.
Matching in Description Logics with Existential Restrictions.
In P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, and P. Patel-Schneider,
editors, Proceedings of the International Workshop on Description Logics
1999 (DL'99), number 22 in CEUR-WS, Sweden, 1999. Linköping
University.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/.
Bibtex entry Paper (PS)
Abstract
Matching of concepts with variables (concept patterns) is a relatively
new operation that has been introduced in the context of description
logics, originally to help filter out unimportant aspects of large
concepts appearing in industrial-strength knowledge bases. Previous
work on this problem has produced polynomial-time matching algorithms
for sublanguages of the DL used in CLASSIC. Consequently, these algorithms
cannot handle existential restrictions. In this paper, we
consider matching in DLs allowing for existential restrictions.
We describe decision procedures that test solvability
of matching problems as well as algorithms for computing complete
sets of matchers. Unfortunately, these algorithms are no longer
polynomial-time, even for the small language EL, which
allows for the top concept, conjunction and existential restrictions.
F. Baader, R. Küsters, A. Borgida, and D. McGuinness.
Matching in Description Logics.
Journal of Logic and Computation, 9(3):411–447, 1999.
Bibtex entry Abstract
Abstract
Matching concepts against patterns (concepts with variables)
is a relatively new operation that has been introduced in the
context of concept description languages (description logics).
The original goal was to help filter out unimportant aspects of
complicated concepts appearing in large industrial knowledge bases.
We propose a new approach to performing matching, based on a
``concept-centered'' normal form, rather than the more standard
``structural subsumption'' normal form for concepts. As a result,
matching can be performed (in polynomial time) using arbitrary
concept patterns of the description language ALN, thus removing
restrictions from previous work. The paper also addresses the
question of matching problems with additional ``side conditions'',
which were motivated by practical needs.
F. Baader, R. Küsters, and R. Molitor.
Computing Least Common Subsumers in Description Logics with Existential
Restrictions.
In T. Dean, editor, Proceedings of the 16th International Joint Conference
on Artificial Intelligence (IJCAI'99), pages 96–101. Morgan Kaufmann,
1999.
Bibtex entry Abstract
Abstract
Computing the least common subsumer (lcs) is an inference task that can be
used to support the "bottom-up" construction of knowledge bases for KR
systems based on description logics. Previous work on how to compute the lcs
has concentrated on description logics that allow for universal value
restrictions, but not for existential restrictions. The main new contribution
of this paper is the treatment of description logics with existential
restrictions. Our approach for computing the lcs is based on an appropriate
representation of concept descriptions by certain trees, and a
characterization of subsumption by homomorphisms between these trees. The lcs
operation then corresponds to the product operation on trees.
F. Baader and R. Molitor.
Rewriting Concepts Using Terminologies.
In P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, and P. Patel-Schneider,
editors, Proceedings of the International Workshop on Description Logics
1999 (DL'99), number 22 in CEUR-WS, Sweden, 1999. Linköping
University.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/.
Bibtex entry Paper (PS)
Abstract
In this work we consider the inference problem of computing (minimal) rewritings
of concept descriptions using defined concepts from a terminology. We introduce
a general framework for this problem and instantiate it with the small
description logic FLo, which provides us with conjunction and value
restrictions. We show that the decision problem induced by the minimal rewriting
problem is NP-complete for FLo.
F. Baader, R. Molitor, and S. Tobies.
Tractable and Decidable Fragments of Conceptual Graphs.
In W. Cyre and W. Tepfenhart, editors, Proceedings of the Seventh
International Conference on Conceptual Structures (ICCS'99), number 1640
in Lecture Notes in Computer Science, pages 480–493. Springer Verlag, 1999.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
This paper is concerned with decidability and tractability of reasoning in
conceptual graphs (CGs). It is well-known that problems like validity and
subsumption of general CGs are undecidable, whereas subsumption is NP-complete
for simple conceptual graphs (SGs) and tractable for the fragment of SGs that
are trees. On the one hand, we will employ results on decidable fragments of
first-order logic to identify a natural and expressive fragment of CGs for
which validity and subsumption is decidable in deterministic exponential time.
On the other hand, we will extend existing work on the connection between SGs
and description logics (DLs) by identifying a DL that corresponds to the class
of SGs that are trees. This yields a previously unknown tractability result
for the DL in question. As a by-product, we will extend the tractability
results for trees to SGs that can be transformed into trees by ``cutting
cycles.''
F. Baader and U. Sattler.
Expressive Number Restrictions in Description Logics.
Journal of Logic and Computation, 9(3):319–350, 1999.
Bibtex entry Paper (PS)
Abstract
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.
F. Baader and C. Tinelli.
Deciding the Word Problem in the Union of Equational Theories Sharing
Constructors.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th
International Conference on Rewriting Techniques and Applications (RTA-99), volume 1631 of Lecture Notes in Computer Science, pages
175–189, Trento, Italy, 1999. Springer-Verlag.
Bibtex entry ©Springer-Verlag
Abstract
The main contribution of this paper is a new method for
combining decision procedures for the word problem in equational
theories sharing ``constructors.'' The notion of constructor
adopted in this paper has a nice algebraic definition and is more
general than a related notion introduced in previous work on the
combination problem.
Franz Baader and Cesare Tinelli.
Combining Equational Theories Sharing Non-Collapse-Free Constructors.
Technical Report 99-13, Department of Computer Science, University of Iowa,
October 1999.
Bibtex entry Paper (PS)
Abstract
In a previous work, we describe a method to combine decision procedures for the word problem for
theories sharing constructors. One of the requirements of our combination method is that the
constructors be collapse-free. This paper removes that requirement by modifying the
method so that it applies to non-collapse-free constructors as well. This broadens the scope of our
combination results considerably, for example in the direction of equational theories
corresponding to modal logics.
A. Borgida and R. Küsters.
What's not in a name? Initial Explorations of a Structural Approach to
Integrating Large Concept Knowledge-Bases.
Technical Report DCS-TR-391, Rutgers University, USA, 1999.
Bibtex entry Paper (PS)
Cyril Decleir, Mohand-Said Hacid, and Jacques Kouloumdjian.
A Database Approach for Modeling and Querying Video Data.
In Masaru Kitsuregawa, Leszek Maciaszek, and Mike Papazoglou, editors,
Proceedings of the 15th International Conference on Data Engineering, Sydney,
Australia, pages 6–13. IEEE Computer Society, March 1999.
Bibtex entry Paper (PS)
Abstract
Indexing video data is essential for providing content based access.
In this paper, we consider how database technology can offer an
integrated framework for modeling and querying video data. As many
concerns in video (e.g., modeling and querying) are also found in
databases, databases provide an interesting angle to attack many of the
problems. From a video applications perspective, database systems
provide a nice
basis for future video systems. More generally, database research
will provide solutions to many video issues even if these are partial or
fragmented. From a database perspective, video applications provide
beautiful challenges. Next generation database systems will need to
provide support for multimedia data (e.g., image, video, audio). These
data types require new techniques for their management (i.e., storing,
modeling, querying, etc.). Hence new solutions are significant.
This paper develops a data model and a rule-based query language for video
content based indexing and retrieval. The data model is designed around
the object and constraint paradigms. A video sequence is split into a set
of fragments. Each fragment can be analyzed to extract the information
(i.e., symbolic descriptions) of interest that can be put into a database.
This database can then be searched to find information of interest. Two types
of information are considered: (1) the entities (i.e., objects) of interest in the
domain of a video sequence, (2) video frames which contain these entities.
To represent these information, our data model allows facts as well as objects
and constraints. We present a declarative, rule-based, constraint query language
that can be used to infer relationships about information represented in the model.
The language has a clear declarative and operational semantics.
E. Franconi and U. Sattler.
A Data Warehouse Conceptual Data Model for Multidimensional
Aggregation.
In Workshop on Design and Management of Data Warehouses (DMDW'99),
Heidelberg, Germany, June 1999.
Bibtex entry Paper (PS)
E. Franconi and U. Sattler.
A Data Warehouse Conceptual Data Model for Multidimensional Aggregation: a
preliminary report.
Italian Association for Artificial Intelligence AI*IA Notizie, 1:9–21,
1999.
Bibtex entry Paper (PS)
V. Haarslev, C. Lutz, and R. Möller.
A Description Logic with Concrete Domains and Role-forming Predicates.
Journal of Logic and Computation, 9(3):351–384, 1999.
Bibtex entry Paper (PS)
Abstract
This article presents the description logic ALCRP(D) with concrete domains
and a role-forming predicate operator as its prominent aspects. We
demonstrate
the feasibility of ALCRP(D) for reasoning about spatial objects and their
qualitative spatial relationships and provide an appropriate concrete
domain for spatial
objects. The general significance of ALCRP(D) is demonstrated by adding
temporal reasoning to spatial and terminological reasoning using a combined
concrete domain. The theory is motivated as a basis for knowledge
representation and query processing in the domain of geographic information
systems. In
contrast to existing work in this domain, which mainly focuses either on
conceptual reasoning or on reasoning about qualitative spatial relations,
we integrate
reasoning about spatial information with terminological reasoning.
Mohand-Said Hacid and Christophe Rigotti.
Representing and Reasoning on Conceptual Queries Over Image
Databases.
In Zbigniew W. Ras and Andrzej Skowron, editors, Proceedings of the
Eleventh International Symposium on Methodologies for Intelligent Systems,
Warsaw, Poland, LNCS 1609, pages 340–348. Springer, June 1999.
Bibtex entry Paper (PS)
Abstract
The problem of content management of multimedia data types (e.g., image, video, graphics)
is becoming increasingly important with the development of advanced multimedia applications.
In this paper we develop a knowledge-based framework for modeling and retrieving image data.
To represent the various aspects of an image object's characteristics, we
propose a model which consists of three layers: (1) Feature and Content Layer, intended
to contain image visual features such as contours, shapes, etc.; (2) Object Layer, which provides the
(conceptual) content dimension of images; and (3) Schema Layer, which
contains the structured abstractions
of images.
We propose two abstract
languages on the basis of description logics: one for describing knowledge of the object and schema
layers,
and the other, more expressive, for making queries. Queries can refer to the form
dimension (i.e., information of the Feature and Content Layer) or to the content
dimension (i.e., information of the Object Layer).
As the amount of information contained in the previous layers may be huge and
operations performed at the Feature and Content Layer are time-consuming, resorting to
the use of materialized views to process and optimize queries may be extremely useful.
For that, we propose a formal framework for testing containment of a query in a view
expressed in our query language.
I. Horrocks and U. Sattler.
A Description Logic with Transitive and Inverse Roles and Role
Hierarchies.
Journal of Logic and Computation, 9(3):385–410, 1999.
Bibtex entry Abstract
Abstract
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 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.
Ian Horrocks, Ulrike Sattler, and Stephan Tobies.
Practical Reasoning for Description Logics with Functional Restrictions,
Inverse and Transitive Roles, and Role Hierarchies.
In Proceedings of the 1999 Workshop Methods for Modalities (M4M-1),
Amsterdam, 1999.
Bibtex entry Paper (PS)
Abstract
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 functional 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,
showing that relaxing the constraints placed on the kinds of roles used in
number restrictions leads to the undecidability of all inference problems.
Ian Horrocks, Ulrike Sattler, and Stephan Tobies.
Practical Reasoning for Expressive Description Logics.
In Harald Ganzinger, David McAllester, and Andrei Voronkov, editors,
Proceedings of the 6th International Conference on Logic for Programming and
Automated Reasoning (LPAR'99), number 1705 in Lecture Notes in
Artificial Intelligence, pages 161–180. Springer-Verlag, September 1999.
Bibtex entry Paper (PS)
Abstract
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.
Stephan Kepser and Jörn Richts.
Optimisation Techniques for Combining Constraint Solvers.
In Dov Gabbay and Maarten de Rijke, editors, Frontiers of Combining Systems
2, Papers presented at FroCoS'98, pages 193–210, Amsterdam, 1999.
Research Studies Press/Wiley.
Bibtex entry Paper (PS)
Abstract
In recent years, techniques that had been developed for the
combination of unification algorithms for equational theories were
extended to combining constraint solvers. These techniques
inherited an old deficit that was already present in the combination
of equational theories which makes them rather unsuitable for
practical use: The underlying combination algorithms are highly
non-deterministic. This paper is concerned with the practical
problem of how to optimise the combination method of Baader and
Schulz. We present an optimisation method, called the
deductive method, which uses specific algorithms for the
components to reach certain decisions deterministically. We also
give a strategy how to select an order of non-deterministic
decisions. Run time tests of our implementation indicate that the
optimised combination method yields combined decision procedures
that are efficient enough to be used in practice.
Stephan Kepser and Jörn Richts.
UniMoK: A System for Combining Equational Unification Algorithms.
In Rewriting Techniques and Applications, Proceedings RTA-99, volume
1631 of Lecture Notes in Computer Science, pages 248–251.
Springer-Verlag, 1999.
Bibtex entry
R. Küsters and A. Borgida.
What's in an Attribute? Consequences for the Least Common Subsumer.
Technical Report DCS-TR-404, Rutgers University, USA, 1999.
Bibtex entry Paper (PS)
Abstract
Functional relationships between objects, called ``attributes'', are of
considerable importance in knowledge representation languages, including
Description Logics (DLs). A study of the literature indicates that papers have
made, often implicitly, different assumptions about the nature of attributes:
whether they are always required to have a value, or whether they can be partial
functions. The work presented here is the first explicit study of this
difference for (sub-)classes of the CLASSIC DL, involving the same-as concept
constructor. It is shown that although determining subsumption between concept
descriptions has the same complexity (though requiring different algorithms),
the story is different in the case of determining the least common subsumer
(lcs). For attributes interpreted as partial functions, the lcs exists and can
be computed relatively easily; even in this case our results correct and extend
three previous papers about the lcs of DLs. In the case where attributes must
have a value, the lcs may not exist, and even if it exists it may be of
exponential size. Interestingly, it is possible to decide in polynomial time if
the lcs exists.
Ralf Küsters.
What's in a name? — First Steps Towards a Structural Approach to
Integrating Large Content-based Knowledge-Bases.
In S. Abiteboul, D. Florescu, A. Levy, and G. Moerkotte, editors,
Foundations for Information Integration, Dagstuhl-Seminar-Report 244,
1999.
ISSN 0940-1121.
Bibtex entry Abstract
Abstract
We address the problem of integrating two content-based knowledge bases. It is
well known that even the same slice of reality can be modeled in various ways.
This ranges from single morphological variants of identifiers to reification of
relationships. Hence, human intervention is required in order to set up some
kind of correspondence mapping between the knowledge bases. However, modern
real-life ontologies, such as the Galen medical ontology, are so large that it
seems not feasible for humans to perform this task without computer aid. We
therefore aim at exploiting the structural information to help find candidate
equivalent concepts from one ontology to the other.
To this end, we have set up a formal framework for correspondence mappings and
have investigated limitations of structural information to find such mappings.
Finally, first algorithmic and empirical results have been presented.
C. Lutz.
Complexity of Terminological Reasoning Revisited.
In Proceedings of the 6th International Conference on Logic for Programming
and Automated Reasoning LPAR'99, Lecture Notes in Artificial
Intelligence, pages 181–200. Springer-Verlag, September 6 – 10, 1999.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
TBoxes in their various forms are key components of knowledge representation
systems based on description logics (DLs) since they allow for a natural
representation of terminological knowledge. Largely due to a classical
result given by Nebel, complexity analyses for DLs have,
until now, mostly failed to take into account the most basic form of TBoxes,
so-called acyclic TBoxes. In this paper, we concentrate on DLs for
which reasoning without TBoxes is PSpace-complete, and show that there
exist logics for which the complexity of reasoning remains in PSpace if
acyclic TBoxes are added and also logics for which the complexity increases.
This demonstrates that it is necessary to take acyclic TBoxes into account
for complexity analyses.
C. Lutz.
Reasoning with Concrete Domains.
In Thomas Dean, editor, Proceedings of the Sixteenth International Joint
Conference on Artificial Intelligence IJCAI-99, pages 90–95, Stockholm,
Sweden, July 31 – August 6, 1999. Morgan-Kaufmann Publishers.
Bibtex entry Paper (PS)
Abstract
Description logics are formalisms for the representation of and reasoning
about conceptual knowledge on an abstract level. Concrete domains allow
the
integration of description logic reasoning with reasoning about concrete
objects such as numbers, time intervals, or spatial regions. The
importance
of this combined approach, especially for building real-world
applications,
is widely accepted. However, the complexity of reasoning with concrete
domains has never been formally analyzed and efficient algorithms have
not
been developed. This paper closes the gap by providing a tight bound for
the
complexity of reasoning with concrete domains and presenting optimal
algorithms.
C. Lutz, U. Sattler, and S. Tobies.
A Suggestion for an n-ary Description Logic.
In Patrick Lambrix, Alex Borgida, Maurizio Lenzerini, Ralf Möller, and
Peter Patel-Schneider, editors, Proceedings of the International Workshop
on Description Logics, number 22 in CEUR-WS, pages 81–85, Linkoeping,
Sweden, July 30 – August 1 1999. Linköping University.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/.
Bibtex entry Paper (PS)
Abstract
A restriction most Description Logics (DLs) have in common with most Modal
Logics is their restriction to unary and binary predicates. To our knowledge,
the only DLs that overcome these restrictions and allow for arbitrary n-ary
relations are n-ary Kandor and the very expressive DL DLR. In the field of Modal
Logics, there are two generalisations that allow for
n-ary predicates: Polyadic Modal Logics and the more
expressive Guarded Fragment, which was shown
to be ExpTime-complete and for which a resolution based decision
procedure exists. Unfortunately, when extended by operators
that are standard in DLs such as number restrictions, features, or transitive
roles, this logic becomes undecidable.
In this paper, we present a new DL, GF1-, that was designed to meet three goals:
1. It should allow for n-ary relations; 2. ``concept'' subsumption and satisfiability should be in PSpace; and 3., it should allow the extension with number restrictions and/or transitive
roles (without losing decidability).
S .Tobies.
A NExpTime-complete Description Logic Strictly Contained in C^2.
In J. Flum and M. Rodríguez-Artalejo, editors, Proceedings of the
Annual Conference of the European Association for Computer Science Logic
(CSL-99), LNCS 1683, pages 292–306. Springer-Verlag, 1999.
Bibtex entry Paper (PS) Extended technical report (PS)
Abstract
We examine the complexity and expressivity of the combination of the
Description Logic ALCQI with a terminological formalism based on cardinality
restrictions on concepts. This combination can naturally be embedded into
C^2, the two variable fragment of predicate logic with counting quantifiers.
We prove that ALCQI has the same complexity as C^2 but does not reach its
expressive power.
S. Tobies.
On the Complexity of Counting in Description Logics.
In P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, and P. Patel-Schneider,
editors, Proceedings of the International Workshop on Description Logics
1999 (DL'99), number 22 in CEUR-WS, Sweden, 1999. Linköping
University.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/.
Bibtex entry Paper (PS)
Abstract
Many Description Logics (DLs) allow for counting expressions of various forms
that are important in many applications, e.g., for reasoning with semantic
data models and for applications concerned with the configuration of technical
systems. We present two novel complexity results for DLs that contain counting
constructs:
(1) We prove that concept satisfiability for ALCQI is decidable in PSPACE even
if binary coding of numbers in the input is assumed. (2) We prove that TBox
consistency for ALCQI with cardinality restrictions is NEXPTIME-complete.
S. Tobies.
A PSpace Algorithm for Graded Modal Logic.
In H. Ganzinger, editor, Automated Deduction – CADE-16, 16th International
Conference on Automated Deduction, LNAI 1632, pages 52–66, Trento,
Italy, July 7–10, 1999. Springer-Verlag.
Bibtex entry Paper (PS)
Abstract
We present a PSPACE algorithm that decides satisfiability of the graded
logic Gr(K_R) - a natural extension of propositional modal logic K_R by counting
expressions -which plays an important role in the area of knowledge
representation. The algorithm employs a tableaux approach and is the first
known algorithm which meets the lower bound for the complexity of the problem.
Thus, we exactly fixe the complexity of the problem and refute a
EXPTIME-hardness conjecture. This establishes a kind of ``theoretical
benchmark'' that all algorithmic approaches can be measured with.
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.