Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Publications

2007

A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalising Tractable Description Logics. In Proceedings of the Fourteenth International Symposium on Temporal Representation and Reasoning. IEEE Computer Society Press, 2007.
Bibtex entry Paper (PDF)

Abstract

It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of "weak" description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable.

Alessandro Artale, Carsten Lutz, and David Toman. A Description Logic of Change. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 218–223. AAAI Press, 2007.
Bibtex entry Paper (PDF)

Abstract

We combine the modal logic S5 with the description logic (DL) ALCQI. The resulting multi-dimensional DL S5-ALCQI supports reasoning about change by allowing to express that concepts and roles change over time. It cannot, however, discriminate between changes in the past and in the future. Our main technical result is that satisfiability of S5-ALCQI concepts with respect to general TBoxes (including GCIs) is decidable and 2-ExpTime-complete. In contrast, reasoning in temporal DLs that are able to discriminate between past and future is inherently undecidable. We argue that our logic is sufficient for reasoning about temporal conceptual models with time-stamping constraints.

F. Baader, editor. 18th International Conference on Rewriting Techniques and Applications (RTA 2007), volume 4533 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
Bibtex entry Abstract

Abstract

This volume contains the papers presented at the 18th International Conference on Rewriting Techniques and Applications (RTA'07), which was held on June 26--28, 2007, on the Paris campus of the Conservatoire National des Arts et Metiers (CNAM) in Paris, France.

F. Baader and S. Ghilardi. Connecting Many-Sorted Theories. The Journal of Symbolic Logic, 72(2):535–583, 2007.
Bibtex entry Paper (PDF)

Abstract

Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme. Our results can be seen as a generalization of the so-called E-connection approach for combining modal logics to an algebraic setting.

F. Baader, J. Hladik, and R. Peñaloza. Blocking Automata for PSPACE DLs. In D. Calvanese, E. Franconi, and S. Tessaris, editors, Proceedings of the 2007 International Workshop on Description Logics, CEUR-WS, 2007.
Bibtex entry Paper (PDF)

Abstract

In Description Logics (DLs), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as concept satisfiability. 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 w.r.t. acyclic terminologies in the DL SI.

F. Baader, J. Hladik, and R. Peñaloza. SI! Automata Can Show PSPACE Results for Description Logics. In C. Martin-Vide, editor, Proceedings of the First International Conference on Language and Automata Theory and Applications (LATA'07), 2007.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

In Description Logics (DLs), 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 w.r.t. acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles.

F. Baader, I. Horrocks, and U. Sattler. Description Logics. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, pages 135–179. Elsevier, 2007.
Bibtex entry Abstract

Abstract

In this chapter we will introduce description logics, a family of logic-based knowledge representation languages that can be used to represent the terminological knowledge of an application domain in a structured way. We will first review their provenance and history, and show how the field has developed. We will then introduce the basic description logic ALC in some detail, including definitions of syntax, semantics and basic reasoning services, and describe important extensions such as inverse roles, number restrictions, and concrete domains. Next, we will discuss the relationship between description logics and other formalisms, in particular first order and modal logics; the most commonly used reasoning techniques, in particular tableaux, resolution and automata based techniques; and the computational complexity of basic reasoning problems. After reviewing some of the most prominent applications of description logics, in particular ontology language applications, we will conclude with an overview of other aspects of description logic research, and with pointers to the relevant literature.

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya. Completing Description Logic Knowledge Bases using Formal Concept Analysis. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07). AAAI Press, 2007.
Bibtex entry Paper (PDF)

Abstract

We propose an approach for extending both the terminological and the assertional part of a Description Logic knowledge base by using information provided by the knowledge base and by a domain expert. The use of techniques from Formal Concept Analysis ensures that, on the one hand, the interaction with the expert is kept to a minimum, and, on the other hand, we can show that the extended knowledge base is complete in a certain, well-defined sense.

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya. Completing Description Logic Knowledge Bases using Formal Concept Analysis. In Christine Golbreich, Aditya Kalyanpur, and Bijan Parsia, editors, Proceedings of the Third International Workshop OWL: Experiences and Directions (OWLED 2007), volume 258. CEUR-WS, 2007.
Bibtex entry Paper (PDF)

Abstract

Franz Baader, Carsten Lutz, and Boontawee Suntisrivaraporn. Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?. In Journal of Logic, Language and Information, Special Issue on Method for Modality (M4M), 2007. To appear.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

Extensions of the description logic EL have recently been proposed as lightweight ontology languages. The most important feature of these extensions is that, despite including powerful expressive means such as general concept inclusion axioms, reasoning can be carried out in polynomial time. In this paper, we consider one of these extensions, EL+, and introduce a refinement of the known polynomial-time classification algorithm for this logic. This refined algorithm was implemented in our CEL reasoner. We describe the results of several experiments with CEL on large ontologies from practice, which show that even a relatively straightforward implementation of the described algorithm outperforms highly optimized, state-of-the-art tableau reasoners for expressive description logics.

Franz Baader and Rafael Peñaloza. Axiom Pinpointing in General Tableaux. In N. Olivetti, editor, Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2007, volume 4548 of Lecture Notes in Computer Science, pages 11–27, Aix-en-Provence, France, 2007. Springer-Verlag.
Bibtex entry Paper (PDF) ©Springer-Verlag

Abstract

Axiom pinpointing has been introduced in description logics to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of "tableaux algorithms," which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn. Pinpointing in the Description Logic EL. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007.
Bibtex entry Paper (PDF)

Abstract

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question. Until now, the pinpointing approach has only been applied to the DL ALC and some of its extensions. This paper considers axiom pinpointing in the DL EL, for which subsumption can be decided in polynomial time. We describe an extension of the subsumption algorithm for EL that can be used to compute all minimal subsets of a given TBox that imply a certain subsumption relationship. We also show that an EL TBox may have exponentially many such minimal subsets and that even finding out whether there is such a minimal subset within a given cardinality bound is an NP-complete problem. In contrast to these negative results, we also show that one such minimal set can be computed in polynomial time. Finally, we provide some encouraging experimental results regarding the performance of a practical algorithm that computes one (not necessarily minimal) set that has a given subsumption relation as consequence.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn. Pinpointing in the Description Logic EL. In Proceedings of the 30th German Conference on Artificial Intelligence (KI2007), volume 4667 of Lecture Notes in Artificial Intelligence, pages 52–67, Osnabrück, Germany, 2007. Springer-Verlag.
Bibtex entry Paper (PDF) ©Springer-Verlag

Abstract

Axiom pinpointing has been introduced in description logics (DLs) to help the user understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question. Until now, the pinpointing approach has only been applied to the DL ALC and some of its extensions. This paper considers axiom pinpointing in the less expressive DL EL+, for which subsumption can be decided in polynomial time. More precisely, we consider an extension of the pinpointing problem where the knowledge base is divided into a static part, which is always present, and a refutable part, of which subsets are taken. We describe an extension of the subsumption algorithm for EL+ that can be used to compute all minimal subsets of (the refutable part of) a given TBox that imply a certain subsumption relationship. The worst-case complexity of this algorithm turns out to be exponential. This is not surprising since we can show that a given TBox may have exponentially many such minimal subsets. However, we can also show that the problem is not even output polynomial, i.e., unless P=NP, there cannot be an algorithm computing all such minimal sets that is polynomial in the size of its input and output. In addition, we show that finding out whether there is such a minimal subset within a given cardinality bound is an NP-complete problem. In contrast to these negative results, we also show that one such minimal subset can be computed in polynomial time. Finally, we provide some encouraging experimental results regarding the performance of a practical algorithm that computes one (small, but not necessarily minimal) subset that has a given subsumption relation as consequence.

Franz Baader, Baris Sertkaya, and Anni-Yasmin Turhan. Computing the Least Common Subsumer w.r.t. a Background Terminology. Journal of Applied Logic, 5(3):392–420, 2007.
Bibtex entry Paper (PS) Paper (PDF) ©Journal of Applied Logic

Abstract

Methods for computing the least common subsumer (lcs) are usually restricted to rather inexpressive Description Logics (DLs) whereas existing knowledge bases are written in very expressive DLs. In order to allow the user to re-use concepts defined in such terminologies and still support the definition of new concepts by computing the lcs, we extend the notion of the lcs of concept descriptions to the notion of the lcs w.r.t. a background terminology. We will show both theoretical results on the existence of the least common subsumer in this setting, and describe a practical approach—based on a method from formal concept analysis—for computing good common subsumers, which may, however, not be the least ones. We will also describe results obtained in a first evaluation of this practical approach.

Birte Glimm, Carsten Lutz, Ian Horrocks, and Ulrike Sattler. Answering conjunctive queries in the SHIQ description logic. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 299–404. AAAI Press, 2007.
Bibtex entry Paper (PDF)

Abstract

Conjunctive queries play an important role as an expressive query language for Description Logics (DLs). Although modern DLs usually provide for transitive roles, it was an open problem whether conjunctive query answering over DL knowledge bases is decidable if transitive roles are admitted in the query. In this paper, we consider conjunctive queries over knowledge bases formulated in the popular DL SHIQ and allow transitive roles in both the query and the knowledge base. We show that query answering is decidable and establish the following complexity bounds: regarding combined complexity, we devise a deterministic algorithm for query answering that needs time single exponential in the size of the KB and double exponential in the size of the query. Regarding data complexity, we prove co-NP-completeness.

Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with Intersection and Converse is 2EXP-complete. In Helmut Seidl, editor, Proceedings of the Tenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'07), volume 4423 of Lecture Notes in Computer Science, pages 198–212. Springer-Verlag, 2007.
Bibtex entry Paper (PDF)

Abstract

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.

A. Krisnadhi and C. Lutz. Data Complexity in the EL family of DLs. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007. To appear.
Bibtex entry Paper (PDF)

Abstract

We study the data complexity of instance checking and conjunctive query answering in the EL family of DLs, with a particular emphasis on the boundary of tractability. We identify a large number of intractable extensions of EL, but also show that in ELIf, the extension of EL with inverse roles and global functionality, conjunctive query answering is tractable regarding data complexity. In contrast, instance checking in EL extended with only inverse roles or global functionality is ExpTime-complete regarding combined complexity.

Adila Krisnadhi and Carsten Lutz. Data Complexity in the EL family of Description Logics. In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR2007), volume 4790 of Lecture Notes in Artificial Intelligence, pages 333–347. Springer-Verlag, 2007.
Bibtex entry Paper (PDF)

Abstract

We study the data complexity of instance checking and conjunctive query answering in the EL family of description logics, with a particular emphasis on the boundary of tractability. We identify a large number of intractable extensions of EL, but also show that in ELI^f, the extension of EL with inverse roles and global functionality, conjunctive query answering is tractable regarding data complexity. In contrast, already instance checking in EL extended with only inverse roles or global functionality is ExpTime-complete regarding combined complexity.

C. Löding, C. Lutz, and O. Serre. Propositional Dynamic Logic with Recursive Programs. Journal of Logic and Algebraic Programming, 73:51–69, 2007.
Bibtex entry Paper (PDF)

Abstract

We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs. Our decision procedure establishes a 2- ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with non-regular programs. Thus, we also show that such extensions tend to be more complex than standard PDL.

C. Lutz. Inverse Roles Make Conjunctive Queries Hard. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007. To appear.
Bibtex entry Paper (PDF)

Abstract

Conjunctive query answering is an important DL reasoning task. Although this task is by now quite well-understood, tight complexity bounds for conjunctive query answering in expressive DLs have never been obtained: all known algorithms run in deterministic double exponential time, but the existing lower bound is only an ExpTime one. In this paper, we prove that conjunctive query answering in ALCI is 2-ExpTime-hard (and thus complete), and that it becomes NExpTime-complete under some reasonable assumptions.

C. Lutz and M. Milicic. A Tableau Algorithm for DLs with Concrete Domains and GCIs. Journal of Automated Reasoning, 38(1–3):227–259, 2007.
Bibtex entry Paper (PDF)

Abstract

To use description logics (DLs) in an application, it is crucial to identify a DL that is sufficiently expressive to represent the relevant notions of the application domain, but for which reasoning is still decidable. Two means of expressivity that are required by many modern applications of DLs are concrete domains and general TBoxes. The former are used for decidablening concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. The purpose of the latter is to capture background knowledge by stating that the extension of a concept is included in the extension of another concept. Unfortunately, it is wellknown that combining concrete domains with general TBoxes often leads to DLs for which reasoning is undecidable. In this paper, we identify a general property of concrete domains that is sucient for proving decidability of DLs with both concrete domains and general TBoxes. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with concrete domains and general TBoxes.

Carsten Lutz, Dirk Walther, and Frank Wolter. Conservative Extensions in Expressive Description Logics. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 453–458. AAAI Press, 2007.
Bibtex entry Paper (PDF)

Abstract

The notion of a conservative extension plays a central role in ontology design and integration: it can be used to formalize ontology refinements, safe mergings of two ontologies, and independent modules inside an ontology. Regarding reasoning support, the most basic task is to decide whether one ontology is a conservative extension of another. It has recently been proved that this problem is decidable and 2ExpTime-complete if ontologies are formulated in the basic description logic ALC. We consider more expressive description logics and begin to map out the boundary between logics for which conservativity is decidable and those for which it is not. We prove that conservative extensions are 2ExpTime-complete in ALCQI, but undecidable in ALCQIO. We also show that if conservative extensions are defined model-theoretically rather than in terms of the consequence relation, they are undecidable already in ALC.

Carsten Lutz and Frank Wolter. Conservative Extensions in the Lightweight Description Logic EL. In Frank Pfenning, editor, Proceedings of the 21th Conference on Automated Deduction (CADE-21), volume 4603 of Lecture Notes in Artificial Intelligence, pages 84–99. Springer-Verlag, 2007.
Bibtex entry Paper (PDF) ©Springer-Verlag

Abstract

We bring together two recent trends in description logic (DL): lightweight DLs in which the subsumption problem is tractable and conservative extensions as a central tool for formalizing notions of ontology design such as refinement and modularity. Our aim is to investigate conservative extensions as an automated reasoning problem for the basic tractable DL EL. The main result is that deciding (deductive) conservative extensions is ExpTime-complete, thus more difficult than subsumption in EL, but not more difficult than subsumption in expressive DLs. We also show that if conservative extensions are defined model-theoretically, the associated decision problem for EL is undecidable.

Maja Milicic. Complexity of Planning in Action Formalisms Based on Description Logics. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2007), Lecture Notes in Artificial Intelligence. Springer-Verlag, 2007.
Bibtex entry Paper (PDF)

Abstract

In this paper, we continue the recently started work on integrating action formalisms with description logics (DLs), by investigating planning in the context of DLs. We prove that the plan existence problem is decidable for actions described in fragments of ALCQIO. More precisely, we show that its computational complexity coincides with the one of projection for DLs between ALC and ALCQIO if operators contain only unconditional post-conditions. If we allow for conditional post-conditions, the plan existence problem is shown to be in 2-ExpSpace.

Maja Milicic. Planning in Action Formalisms based on DLs: First Results. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007.
Bibtex entry Paper (PDF)

Abstract

In this paper, we continue the recently started work on integrating action formalisms with description logics (DLs), by investigating planning in the context of DLs. We prove that the plan existence problem is decidable for actions described in fragments of ALCQIO. More precisely, we show that, if post-conditions of operators are unconditional, its computational complexity coincides with the one of projection for DLs between ALC and ALCQIO.

Stefan Schulz, Boontawee Suntisrivaraporn, and Franz Baader. SNOMED CT's Problem List: Ontologists' and Logicians' Therapy Suggestions. In Proceedings of The Medinfo 2007 Congress, Studies in Health Technology and Informatics (SHTI-series). IOS Press, 2007.
Bibtex entry Paper (PDF)

Abstract

After a critical review of the present architecture of SNOMED CT, addressing both logical and ontological issues, we present a roadmap towards an overall improvement of this terminology. In particular, we recommend the following actions: Upper level categories should be re-arranged according to a standard upper level ontology. Meta-class like concepts should be identified and removed from the taxonomy. SNOMED concepts denoting (non instantiable) individual entities (e.g. geographical regions) should be kept separate from those concepts that denote (instantiable) types. SNOMED binary relations should be reduced to a set of canonical ones, following existing recommendations. Taxonomies should be cleansed and split into disjoint partitions. The number of full definitions should be increased. Finally, we propose a new approach to modeling part-whole hierarchies, as well as the integration of qualifier relations into the description logic framework.

Boontawee Suntisrivaraporn, Franz Baader, Stefan Schulz, and Kent Spackman. Replacing SEP-Triplets in SNOMED CT using Tractable Description Logic Operators. In Jim Hunter Riccardo Bellazzi, Ameen Abu-Hanna, editor, Proceedings of the 11th Conference on Artificial Intelligence in Medicine (AIME'07), Lecture Notes in Computer Science. Springer-Verlag, 2007.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

Reification of parthood relations according to the SEP-triplet encoding pattern has been employed in the clinical terminology SNOMED CT to simulate transitivity of the part-of relation via transitivity of the is-a relation and to inherit properties along part-of links. In this paper we argue that using a more expressive representation language, which allows for a direct representation of the relevant properties of the part-of relation, makes modelling less error prone while having no adverse effect on the efficiency of reasoning.

Balder ten Cate and Carsten Lutz. Query Containment in Very Expressive XPath dialects. In Leonid Libkin, editor, 26th ACM Symposium on Principles of Database Systems (PODS'07), pages 73–82. ACM Press, 2007.
Bibtex entry Paper (PDF)

Abstract

Query containment has been studied extensively for fragments of XPath 1.0. For instance, the problem is known to be EXPTIMEcomplete for CoreXPath, the navigational core of XPath 1.0. Much less is known about query containment in (fragments of) the richer language XPath 2.0. In this paper, we consider extensions of CoreXPath with the following operators, which are all part of XPath 2.0 (except the last): path intersection, path equality, path complementation, for-loops, and transitive closure. For each combination of these operators, we determine the complexity of query containment, both with and without DTDs. It turns out to range from EXPTIME (for extensions with path equality) and 2-EXPTIME (for extensions with path intersection) to non-elementary (for extensions with path complementation or for-loops). In almost all cases, adding transitive closure on top has no further impact on the complexity. We also investigate the effect of dropping the upward and/or sibling axes, and show that this sometimes leads to a reduction in complexity. Since the languages we study include negation and conjunction in filters, our complexity results can equivalently be stated in terms of satisfiability. We also analyze the above languages in terms of succinctness.

A.-Y. Turhan and Y. Bong. Speeding up Approximation with Nicer Concepts. In D. Calvanese, E. Franconi, V. Haarslev, D. Lembo, B. Motik, S. Tessaris, and A.-Y. Turhan, editors, Proc. of the 2007 Description Logic Workshop (DL 2007), 2007.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

Concept approximation is an inference service for Description Logics that provides ``translations'' of concept descriptions from one DL to a less expressive DL. In [4] a method for optimizing the computation of ALC-ALE-approximations of ALC-concept descriptions was introduced. The idea is to characterize a certain class of concept descriptions for which conjuncts can be approximated independently. In this paper we provide relaxed conditions for this class of ALC-concept descriptions, extend this notion to number restrictions and report on a first implementation of this method for ALCN-ALEN-approximation.

Back to the homepage of the Chair for Automata Theory.

Generated at Sat Feb 4 10:56:31 CET 2012.