Technische Berichte

Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL EL is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

@techreport{ BaFe-LTCS-24-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}},
  doi = {https://doi.org/10.25368/2024.34},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {24-01},
  title = {Unification in the Description Logic {$\mathcal{ELH}_{\mathcal{R}^+}$} without the Top Concept modulo Cycle-Restricted Ontologies (Extended Version)},
  type = {LTCS-Report},
  year = {2024},
}

Errors in knowledge bases (KBs) written in a Description Logic (DL) are usually detected when reasoning derives an inconsistency or a consequence that does not hold in the application domain modelled by the KB. Whereas classical repair approaches produce maximal subsets of the KB not implying the inconsistency or unwanted consequence, optimal repairs maximize the consequence sets. In this paper, we extend previous results on how to compute optimal repairs from the DL \(\mathcal{EL}\) to its extension \(\mathcal{EL}^{\bot}\), which in contrast to \(\mathcal{EL}\) can express inconsistency. The problem of how to deal with inconsistency in the context of optimal repairs was addressed previously, but in a setting where the (fixed) terminological part of the KB must satisfy a restriction on cyclic dependencies. Here, we consider a setting where this restriction is not required. We also show how the notion of optimal repairs obtained this way can be used in inconsistency- and error-tolerant reasoning.

@techreport{ BaKrNu-LTCS-24-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah}},
  doi = {https://doi.org/10.25368/2024.6},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {24-02},
  title = {Inconsistency- and Error-Tolerant Reasoning w.r.t.\ Optimal Repairs of $\mathcal{EL}^{\bot}$ Ontologies (Extended Version)},
  type = {LTCS-Report},
  year = {2024},
}

Removing unwanted consequences from a knowledge base has been investigated in belief change under the name contraction and is called repair in ontology engineering. Simple repair and contraction approaches based on removing statements from the knowledge base (respectively called belief base contractions and classical repairs) have the disadvantage that they are syntax-dependent and may remove more consequences than necessary. Belief set contractions do not have these problems, but may result in belief sets that have no finite representation if one works with logics that are not fragments of propositional logic. Similarly, optimal repairs, which are syntax-independent and maximize the retained consequences, may not exist. In this paper, we want to leverage advances in characterizing and computing optimal repairs of ontologies based on the description logics EL to obtain contraction operations that combine the advantages of belief set and belief base contractions. The basic idea is to employ, in the partial meet contraction approach, optimal repairs instead of optimal classical repairs as remainders. We introduce this new approach in a very general setting, and prove a characterization theorem that relates the obtained contractions with well-known postulates. Then, we consider several interesting instances, not only in the standard repair/contraction setting where one wants to get rid of a consequence, but also in other settings such as variants of forgetting in propositional and description logic. We also show that classical belief set contraction is an instance of our approach.

@techreport{ BaWa-LTCS-24-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Renata {Wassermann}},
  doi = {https://doi.org/10.25368/2024.122},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {24-03},
  title = {Contractions Based on Optimal Repairs (Extended Version)},
  type = {LTCS-Report},
  year = {2024},
}

This volume contains the contributions presented at the 38th International Workshop on Unification (UNIF 2024). UNIF 2024 was a satellite event of the Conference on Automated Deduction (CADE), affiliated with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024). It took place on July 2, 2024, in Nancy, France.

@techreport{ EsFe-LTCS-24-04,
  address = {Dresden, Germany},
  author = {Santiago {Escobar} and Oliver {Fern{\'a}ndez Gil}},
  doi = {https://doi.org/10.25368/2024.121},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {24-04},
  title = {{Informal Proceedings of The 38th International Workshop on Unification, UNIF 2024}},
  type = {LTCS-Report},
  year = {2024},
}

We present an FCA-based axiomatization method that produces a complete \(\mathcal{EL}\) TBox (the terminological part of an OWL 2 EL ontology) from a graph dataset in at most exponential time. We describe technical details that allow for efficient implementation as well as variations that dispense with the computation of extremely large axioms, thereby rendering the approach applicable albeit some completeness is lost. Moreover, we evaluate the prototype on real-world datasets.

@techreport{ Kr-LTCS-23-01,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2023.214},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {23-01},
  title = {Efficient Axiomatization of OWL 2 EL Ontologies from Data by means of Formal Concept Analysis (Extended Version)},
  type = {LTCS-Report},
  year = {2023},
}

Concrete domains have been introduced in Description Logic (DL) to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. The primary research goal in this context was to find restrictions on the concrete domain such that its integration into certain DLs preserves decidability or tractability. In this paper, we investigate the abstract expressive power of logics extended with concrete domains, namely which classes of first-order interpretations can be expressed using these logics. In the first part of the paper, we show that, under natural conditions on the concrete domain \(\mathfrak{D}\) (which also play a role for decidability), extensions of first-order logic (\(\texttt{FOL}\)) or \(\mathcal{ALC}\) with \(\mathfrak{D}\) share important formal properties with \(\texttt{FOL}\), such as the compactness and the Löwenheim-Skolem property. Nevertheless, their abstract expressive power need not be contained in that of \(\texttt{FOL}\). In the second part of the paper, we investigate whether finitely bounded homogeneous structures, which preserve decidability if employed as concrete domains, can be used to express certain universal first-order sentences, which then could be added to DL knowledge bases without destroying decidability. We show that this requires rather strong conditions on said sentences or an extended scheme for integrating the concrete domain that leads to undecidability.

@techreport{ BaBo-LTCS-23-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Filippo {De Bortoli}},
  doi = {https://doi.org/10.25368/2024.240},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaBo-LTCS-23-02}},
  number = {23-02},
  title = {{On the Abstract Expressive Power of Description Logics with Concrete Domains (Extended Version)}},
  type = {LTCS-Report},
  year = {2023},
}

Ontologies based on Description Logics may contain errors, which are usually detected when reasoning produces consequences that follow from the ontology, but do not hold in the modelled application domain. In previous work, we have introduced repair approaches for \(\mathcal{EL}\) ontologies that are optimal in the sense that they preserve a maximal amount of consequences. In this paper, we will, on the one hand, review these approaches, but with an emphasis on motivation rather than on technical details. On the other hand, we will describe new results that address the problems that optimal repairs may become very large or need not even exist unless strong restrictions on the terminological part of the ontology apply. We will show how one can deal with these problems by introducing concise representations of optimal repairs.

@techreport{ BaKoKr-LTCS-23-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Patrick {Koopmann} and Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2023.121},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {23-03},
  title = {Optimal Repairs in the Description Logic $\mathcal{EL}$ Revisited (Extended Version)},
  type = {LTCS-Report},
  year = {2023},
}

We introduce an extension of the Description Logic FL0 that allows us to define concepts in an approximate way. More precisely, we extend FL0 with a threshold concept constructor of the form C@t for @ in <,<=,>,>=, whose semantics is given by using a membership distance function (mdf). A membership distance function m assigns to each domain element and concept a distance value expressing how ``close'' is such element to being an instance of the concept. Based on this, a threshold concept C@t is interpreted as the set of all domain elements that have a distance s from C such that s @ t. We provide a framework to obtain membership distance functions based on functions that compare tuples of languages, and we show how weighted looping tree automata over a semiring can be used to define membership distance functions for FL0 concepts.

@techreport{ FeMa-LTCS-23-04,
  address = {Dresden, Germany},
  author = {Oliver {Fern{\'a}ndez Gil} and Pavlos {Marantidis}},
  doi = {https://doi.org/10.25368/2024.241},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {23-04},
  title = {Towards Extending the Description Logic FL0 with Threshold Concepts Using Weighted Tree Automata},
  type = {LTCS-Report},
  year = {2023},
}

Errors in Description Logic (DL) ontologies are often detected when a reasoner computes unwanted consequences. The question is then how to repair the ontology such that the unwanted consequences no longer follow, but as many of the other consequences as possible are preserved. The problem of computing such optimal repairs was addressed in our previous work in the setting where the data (expressed by an ABox) may contain errors, but the schema (expressed by an \(\mathcal{EL}\) TBox) is assumed to be correct. Actually, we consider a generalization of ABoxes called quantified ABoxes (qABoxes) both as input for and as result of the repair process. Using qABoxes for repair allows us to retain more information, but the disadvantage is that standard DL systems do not accept qABoxes as input. This raises the question, investigated in the present paper, whether and how one can obtain optimal repairs if one restricts the output of the repair process to being ABoxes. In general, such optimal ABox repairs need not exist. Our main contribution is that we show how to decide the existence of optimal ABox repairs in exponential time, and how to compute all such repairs in case they exist.

@techreport{ BaKoKrNu-LTCS-22-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Patrick {Koopmann} and Francesco {Kriegel} and Adrian {Nuradiansyah}},
  doi = {https://doi.org/10.25368/2022.65},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {22-01},
  title = {Optimal ABox Repair w.r.t.\ Static {$\mathcal{EL}$} TBoxes: from Quantified ABoxes back to ABoxes (Extended Version)},
  type = {LTCS-Report},
  year = {2022},
}

Ontologies based on Description Logic (DL) represent general background knowledge in a terminology (TBox) and the actual data in an ABox. DL systems can then be used to compute consequences (such as answers to certain queries) from an ontology consisting of a TBox and an ABox. Since both human-made and machine-learned data sets may contain errors, which manifest themselves as unintuitive or obviously incorrect consequences, repairing DL-based ontologies in the sense of removing such unwanted consequences is an important topic in DL research. Most of the repair approaches described in the literature produce repairs that are not optimal, in the sense that they do not guarantee that only a minimal set of consequences is removed. In a series of papers, we have developed an approach for computing optimal repairs, starting with the restricted setting of an \(\mathcal{EL}\) instance store, extending this to the more general setting of a quantified ABox (where some individuals may be anonymous), and then adding a static \(\mathcal{EL}\) TBox.

Here, we extend the expressivity of the underlying DL considerably, by adding nominals, inverse roles, regular role inclusions and the bottom concept to \(\mathcal{EL}\), which yields a fragment of the well-known DL Horn-\(\mathcal{SROIQ}\). The ideas underlying our repair approach still apply to this DL, though several non-trivial extensions are needed to deal with the new constructors and axioms. The developed repair approach can also be used to treat unwanted consequences expressed by certain conjunctive queries or regular path queries, and to handle Horn-\(\mathcal{ALCOI}\) TBoxes with regular role inclusions.

@techreport{ BaKr-LTCS-22-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.131},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {22-02},
  title = {Pushing Optimal ABox Repair from {$\mathcal{EL}$} Towards More Expressive Horn-DLs (Extended Version)},
  type = {LTCS-Report},
  year = {2022},
}

Reasoners can be used to derive implicit consequences from an ontology. Sometimes unwanted consequences are revealed, indicating errors or privacy-sensitive information, and the ontology needs to be appropriately repaired. The classical approach is to remove just enough axioms such that the unwanted consequences vanish. However, this is often too rough since mere axiom deletion also erases many other consequences that might actually be desired. The goal should not be to remove a minimal number of axioms but to modify the ontology such that only a minimal number of consequences is removed, including the unwanted ones. Specifically, a repair should rather be logically entailed by the input ontology, instead of being a subset. To this end, we introduce a framework for computing fixed-premise repairs of \(\mathcal{EL}\) TBoxes. In the first variant the conclusions must be generalizations of those in the input TBox, while in the second variant no such restriction is imposed. In both variants, every repair is entailed by an optimal one and, up to equivalence, the set of all optimal repairs can be computed in exponential time. A prototypical implementation is provided. In addition, we show new complexity results regarding gentle repairs.

@techreport{ Kr-LTCS-22-04,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.321},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {22-04},
  title = {Optimal Fixed-Premise Repairs of {$\mathcal{EL}$} TBoxes (Extended Version)},
  type = {LTCS-Report},
  year = {2022},
}

The application of automated reasoning approaches to Description Logic (DL) ontologies may produce certain consequences that either are deemed to be wrong or should be hidden for privacy reasons. The question is then how to repair the ontology such that the unwanted consequences can no longer be deduced. An optimal repair is one where the least amount of other consequences is removed. Most of the previous approaches to ontology repair are of a syntactic nature in that they remove or weaken the axioms explicitly present in the ontology, and thus cannot achieve semantic optimality. In previous work, we have addressed the problem of computing optimal repairs of (quantified) ABoxes, where the unwanted consequences are described by concept assertions of the light-weight DL \(\mathcal{EL}\). In the present paper, we improve on the results achieved so far in two ways. First, we allow for the presence of terminological knowledge in the form of an \(\mathcal{EL}\) TBox. This TBox is assumed to be static in the sense that it cannot be changed in the repair process. Second, the construction of optimal repairs described in our previous work is best case exponential. We introduce an optimized construction that is exponential only in the worst case. First experimental results indicate that this reduces the size of the computed optimal repairs considerably.

@techreport{ BaKoKrNu-LTCS-21-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Patrick {Koopmann} and Francesco {Kriegel} and Adrian {Nuradiansyah}},
  doi = {https://doi.org/10.25368/2022.64},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {21-01},
  title = {Computing Optimal Repairs of Quantified ABoxes w.r.t. Static {$\mathcal{EL}$} TBoxes (Extended Version)},
  type = {LTCS-Report},
  year = {2021},
}

Unification in the Description Logic (DL) FL0 is known to be ExpTime-complete, and of unification type zero. We investigate in this paper whether a lower complexity of the unification problem can be achieved by either syntactically restricting the role depth of concepts or semantically restricting the length of role paths in interpretations. We show that the answer to this question depends on whether the number formulating such a restriction is encoded in unary or binary: for unary coding, the complexity drops from ExpTime to PSpace. As an auxiliary result, which is however also of interest in its own right, we prove a PSpace-completeness result for a depth-restricted version of the intersection emptiness problem for deterministic root-to-frontier tree automata. Finally, we show that the unification type of FL0 improves from type zero to unitary (finitary) for unification without (with) constants in the restricted setting.

@techreport{ BaGiRo21,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern\'andez Gil} and Maryam {Rostamigiv}},
  doi = {https://doi.org/10.25368/2022.266},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {21-02},
  title = {Restricted Unification in the {DL} {$\mathcal{FL}_0$} (Extended Version)},
  type = {LTCS-Report},
  year = {2021},
}

We discuss two ways of using abduction to explain missing entailments from description logic knowledge bases, one more common, one more unusual, and then have a closer look at how current results/implementations on abduction could be used towards generating such explanations, and what still needs to be done.

@techreport{ Ko-LTCS-21-03,
  author = {Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.267},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {21-03},
  title = {Two Ways of Explaining Negative Entailments in Description Logics Using Abduction (Extended Version)},
  type = {LTCS-Report},
  year = {2021},
}

We review our recent work on how to compute optimal repairs, optimal compliant anonymizations, and optimal safe anonymizations of ABoxes containing possibly anonymized individuals. The results can be used both to remove erroneous consequences from a knowledge base and to hide secret information before publication of the knowledge base, while keeping as much as possible of the original information.

@techreport{ BaKoKrNuPe-LTCS-21-04,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Patrick {Koopmann} and Francesco {Kriegel} and Adrian {Nuradiansyah} and Rafael {Pe\~{n}aloza}},
  doi = {https://doi.org/10.25368/2022.268},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {21-04},
  title = {{Privacy-Preserving Ontology Publishing: The Case of Quantified ABoxes w.r.t.\ a Static Cycle-Restricted $\mathcal{EL}$ TBox (Extended Version)}},
  type = {LTCS-Report},
  year = {2021},
}

We discuss explanations in Description Logics (DLs), a family of logics used for knowledge representation. Initial work on explaining consequences for DLs had focused on justifications, which are minimal subsets of axioms that entail the consequence. More recently, it was proposed that proofs can provide more detailed information about why a consequence follows. Moreover, several measures have been proposed to estimate the comprehensibility of justifications and proofs, for example, their size or the complexity of logical expressions. In this paper, we analyze the connection between these measures, e.g. whether small justifications necessarily give rise to small proofs. We use a dataset of DL proofs that was constructed last year based on the ontologies of the OWL Reasoner Evaluation 2015. We find that, in general, less complex justifications indeed correspond to less complex proofs, and discuss some exceptions to this rule.

@techreport{ Borg-LTCS-21-05,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt}},
  doi = {https://doi.org/10.25368/2023.225},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {21-05},
  title = {Concise Justifications Versus Detailed Proofs for Description Logic Entailments},
  type = {LTCS-Report},
  year = {2021},
}

Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called omega-admissiblity, need to be imposed on the concrete domain. On the one hand, we generalize the notion of omega-admissiblity from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissiblity to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory.

@techreport{ BaRy-LTCS-20-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Jakub {Rydval}},
  doi = {https://doi.org/10.25368/2022.259},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-01},
  title = {Using Model-Theory to Find $\omega$-Admissible Concrete Domains},
  type = {LTCS-Report},
  year = {2020},
}

The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we add the assumption that certain function symbols f are extensional in the sense that f(s₁,...,s_n) = f(t₁,...,t_n) implies s₁ = t₁,...,s_n = t_n. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.

@techreport{ BaKa-LTCS-20-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Deepak {Kapur}},
  doi = {https://doi.org/10.25368/2022.260},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-02},
  title = {Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols},
  type = {LTCS-Report},
  year = {2020},
}

@techreport{ BoPaRy-LTCS-20-04,
  address = {Dresden, Germany},
  author = {Manuel {Bodirsky} and Wied {Pakusa} and Jakub {Rydval}},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-04},
  title = {Temporal Constraint Satisfaction Problems in Fixed-Point Logic},
  type = {LTCS-Report},
  year = {2020},
}

Classical regular path queries (RPQs) can be too restrictive for some applications and answering such queries under approximate semantics to relax the query is desirable. While for answering regular path queries over graph databases under approximate semantics algorithms are available, such algorithms are scarce for the ontology-mediated setting. In this paper we extend an approach for answering RPQs over graph databases that uses weighted transducers to approximate paths from the query in two ways. The first extension is to answering approximate conjunctive 2-way regular path queries (C2RPQs) over graph databases and the second is to answering C2RPQs such queries over ELH and DL-LiteR ontologies. We provide results on the computational complexity of the underlying reasoning problems and devise approximate query answering algorithms.

@techreport{ FeAt-LTCS-20-05,
  address = {Dresden, Germany},
  author = {Oliver {Fern{\'a}ndez Gil} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.261},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {20-05},
  title = {Answering Regular Path Queries Under Approximate Semantics in Lightweight Description Logics},
  type = {LTCS-Report},
  year = {2020},
}

In deductive module extraction, we determine a small subset of an ontology for a given vocabulary that preserves all logical entailments that can be expressed in that vocabulary. While in the literature stronger module notions have been discussed, we argue that for applications in ontology analysis and ontology reuse, deductive modules, which are decidable and potentially smaller, are often sufficient. We present methods based on uniform interpolation for extracting different variants of deductive modules, satisfying properties such as completeness, minimality and robustness under replacements, the latter being particularly relevant for ontology reuse. An evaluation of our implementation shows that the modules computed by our method are often significantly smaller than those computed by existing methods.

@techreport{ KoCh-LTCS-20-06,
  author = {Patrick {Koopmann} and Jieying {Chen}},
  doi = {https://doi.org/10.25368/2022.262},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {20-06},
  title = {Deductive Module Extraction for Expressive Description Logics (Extended Version)},
  type = {LTCS-Report},
  year = {2020},
}

We adapt existing approaches for privacy-preserving publishing of linked data to a setting where the data are given as Description Logic (DL) ABoxes with possibly anonymised (formally: existentially quantified) individuals and the privacy policies are expressed using sets of concepts of the DL \(\mathcal{E\!L}\). We provide a chacterization of compliance of such ABoxes w.r.t. \(\mathcal{E\!L}\) policies, and show how optimal compliant anonymisations of ABoxes that are non-compliant can be computed. This work extends previous work on privacy-preserving ontology publishing, in which a very restricted form of ABoxes, called instance stores, had been considered, but restricts the attention to compliance. The approach developed here can easily be adapted to the problem of computing optimal repairs of quantified ABoxes.

@techreport{ BaKrNuPe-LTCS-20-08,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah} and Rafael {Pe\~{n}aloza}},
  doi = {https://doi.org/10.25368/2022.263},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-08},
  title = {Computing Compliant Anonymisations of Quantified ABoxes w.r.t. $\mathcal{E\!L}$ Policies (Extended Version)},
  type = {LTCS-Report},
  year = {2020},
}

In recent work, we have shown how to compute compliant anonymizations of quantified ABoxes w.r.t. \(\mathcal{E\!L}\) policies. In this setting, quantified ABoxes can be used to publish information about individuals, some of which are anonymized. The policy is given by concepts of the Description Logic (DL) \(\mathcal{E\!L}\), and compliance means that one cannot derive from the ABox that some non-anonymized individual is an instance of a policy concept. If one assumes that a possible attacker could have additional knowledge about some of the involved non-anonymized individuals, then compliance with a policy is not sufficient. One wants to ensure that the quantified ABox is safe in the sense that none of the secret instance information is revealed, even if the attacker has additional compliant knowledge. In the present paper, we show that safety can be decided in polynomial time, and that the unique optimal safe anonymization of a non-safe quantified ABox can be computed in exponential time, provided that the policy consists of a single \(\mathcal{E\!L}\) concept.

@techreport{ BaKrNuPe-LTCS-20-09,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah} and Rafael {Pe\~{n}aloza}},
  doi = {https://doi.org/10.25368/2022.264},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-09},
  title = {Computing Safe Anonymisations of Quantified ABoxes w.r.t.\ $\mathcal{E\!L}$ Policies (Extended Version)},
  type = {LTCS-Report},
  year = {2020},
}

Concrete domains have been introduced in Description Logics (DLs) to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. To retain decidability when integrating a concrete domain into a decidable DL, the domain must satisfy quite strong restrictions. In previous work, we have analyzed the most prominent such condition, called omega-admissibility, from an algebraic point of view. This provided us with useful algebraic tools for proving omega-admissibility, which allowed us to find new examples for concrete domains whose integration leaves the prototypical expressive DL ALC decidable. When integrating concrete domains into lightweight DLs of the EL family, achieving decidability is not enough. One wants reasoning in the resulting DL to be tractable. This can be achieved by using so-called p-admissible concrete domains and restricting the interaction between the DL and the concrete domain. In the present paper, we investigate p-admissibility from an algebraic point of view. Again, this yields strong algebraic tools for demonstrating p-admissibility. In particular, we obtain an expressive numerical p-admissible concrete domain based on the rational numbers. Although omega-admissibility and p-admissibility are orthogonal conditions that are almost exclusive, our algebraic characterizations of these two properties allow us to locate an infinite class of p-admissible concrete domains whose integration into ALC yields decidable DLs.

@techreport{ BaRy-LTCS-20-10,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Jakub {Rydval}},
  doi = {https://doi.org/10.25368/2022.265},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-10},
  title = {An Algebraic View on p-Admissible Concrete Domains for Lightweight Description Logics (Extended Version)},
  type = {LTCS-Report},
  year = {2020},
}

We make a first step towards adapting an existing approach for privacy-preserving publishing of linked data to Description Logic (DL) ontologies. We consider the case where both the knowledge about individuals and the privacy policies are expressed using concepts of the DL \(\mathcal{EL}\), which corresponds to the setting where the ontology is an \(\mathcal{EL}\) instance store. We introduce the notions of compliance of a concept with a policy and of safety of a concept for a policy, and show how optimal compliant (safe) generalizations of a given \(\mathcal{EL}\) concept can be computed. In addition, we investigate the complexity of the optimality problem.

@techreport{ BaKrNu-LTCS-19-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah}},
  doi = {https://doi.org/10.25368/2022.250},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaKrNu-LTCS-19-01}},
  number = {19-01},
  title = {{Privacy-Preserving Ontology Publishing for $\mathcal{EL}$ Instance Stores (Extended Version)}},
  type = {LTCS-Report},
  year = {2019},
}

A joining implication is a restricted form of an implication where it is explicitly specified which attributes may occur in the premise and in the conclusion, respectively. A technique for sound and complete axiomatization of joining implications valid in a given formal context is provided. In particular, a canonical base for the joining implications valid in a given formal context is proposed, which enjoys the property of being of minimal cardinality among all such bases. Background knowledge in form of a set of valid joining implications can be incorporated. Furthermore, an application to inductive learning in a Horn description logic is proposed, that is, a procedure for sound and complete axiomatization of \(\textsf{Horn-}\mathcal{M}\) concept inclusions from a given interpretation is developed. A complexity analysis shows that this procedure runs in deterministic exponential time.

@techreport{ Kr-LTCS-19-02,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.251},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-19-02}},
  number = {19-02},
  title = {{Joining Implications in Formal Contexts and Inductive Learning in a Horn Description Logic (Extended Version)}},
  type = {LTCS-Report},
  year = {2019},
}

We present some initial results on ontology-based query answering with description logic ontologies that may employ temporal and probabilistic operators on concepts and axioms. Specifically, we consider description logics extended with operators from linear temporal logic (LTL), as well as subjective probability operators, and an extended query language in which conjunctive queries can be combined using these operators. We first show some complexity results for the setting in which either only temporal operators or only probabilistic operators may be used, both in the ontology and in the query, and then show a lower bound for the setting in which both types of operators can be used together.

@techreport{ Ko-LTCS-19-03,
  address = {Dresden, Germany},
  author = {Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.252},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {19-03},
  title = {Maybe Eventually? Towards Combining Temporal and Probabilistic Description Logics and Queries (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Projection is the problem of checking whether the execution of a given sequence of actions will achieve its goal starting from some initial state. In this paper, we study a setting where we combine a two-dimensional Description Logic of context (ConDL) with an action formalism. We choose a well-studied ConDL where both: the possible states of a dynamical system itself (object level) and also different context-dependent views on this system state (context level) are organised in relational structures and can be described using usual DL constructs. To represent how such a system and its views evolve we introduce a suitable action formalism. It allows one to describe change on both levels. Furthermore, the observable changes on the object level due to an action execution can also be context- dependent. We show that the formalism is well-behaved in the sense that projection has the same complexity as standard reasoning tasks in case ALCO is the underlying DL.

@techreport{ TiZa-LTCS-19-04,
  address = {Dresden, Germany},
  author = {Satyadharma {Tirtarasa} and Benjamin {Zarrie{\ss}}},
  doi = {https://doi.org/10.25368/2022.253},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {19-04},
  title = {Projection in a Description Logic of Context with Actions (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. On the other hand, description logics (DLs) provide a well-suited formalism to describe and reason about static knowledge, used in many areas to specify domain knowledge in an ontology. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.

@techreport{ DuKoTu-LTCS-19-05,
  address = {Dresden, Germany},
  author = {Clemens {Dubslaff} and Patrick {Koopmann} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.254},
  institution = {TU Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {19-05},
  title = {Ontology-Mediated Probabilistic Model Checking (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

%!TEX root = ./paper.tex [1]blue#1 We present a method for answering ontology-mediated queries for DL-Lite extended with a concrete domain, where we allow concrete domain predicates to be used in the query as well. Our method is based on query rewriting, a well-known technique for ontology-based query answering (OBQA), where the knowledge provided by the ontology is compiled into the query so that the rewritten query can be evaluated directly over a database. This technique reduces the problem of query answering w.r.t. an ontology to query evaluation over a database instance. Specifically, we consider members of the DL-Lite family extended with unary and binary concrete domain predicates over the real numbers. While approaches for query rewriting DL-Lite with these concrete domain have been investigated theoretically, these approaches use a combined approach in which also the data is processed, and require the concrete domain values occurring in the data to be known in advance, which makes the procedure data-dependent. In contrast, we show how rewritings can be computed in a data-independent fashion.

@techreport{ AlKoTu-LTCS-19-06,
  address = {Dresden, Germany},
  author = {Christian {Alrabbaa} and Patrick {Koopmann} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.255},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {19-06},
  title = {Practical Query Rewriting for \textit{DL-Lite} with Numerical Predicates (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Finite Herbrand models are Herbrand models of first-order theories where each predicate is interpreted by a finite set of atoms. We consider first-order clauses with the signature restricted to unary predicate and function symbols and one variable. Deciding the existence of a finite Herbrand model for a set of such clauses is known to be ExpTime-hard even when clauses are restricted to an anti-Horn form. Here we present an ExpTime algorithm to decide if a finite Herbrand model exists in the more general case of arbitrary clauses. Moreover, we describe a way to generate finite Herbrand models, if they exist. Since there can be infinitely many minimal finite Herbrand models, we propose a new notion of acyclic Herbrand models. If there is a finite Herbrand model for a set of restricted clauses, then there are finitely many (at most triple-exponentially many) acyclic Herbrand models. We show how to generate all of them.

@techreport{ BoMo-LTCS-19-07,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.256},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports/#BoMo-LTCS-19-07}},
  number = {19-07},
  title = {Finite {H}erbrand Models for Restricted First-Order Clauses},
  type = {LTCS-Report},
  year = {2019},
}

We investigate the impact that general concept inclusions and role-value maps have on the complexity and decidability of reasoning in the Description Logic FL0. On the one hand, we give a more direct proof for ExpTime-hardness of subsumption w.r.t. general concept inclusions in FL0. On the other hand, we determine restrictions on role-value maps that ensure decidability of subsumption, but we also show undecidability for the cases where these restrictions are not satisfied.

@techreport{ BaTh-LTCS-19-08,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Cl\'ement {Th\'eron}},
  doi = {https://doi.org/10.25368/2022.257},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaTh-LTCS-19-08}},
  number = {19-08},
  title = {Role-Value Maps and General Concept Inclusions in the Description Logic {$\mathcal{FL}_0$}},
  type = {LTCS-Report},
  year = {2019},
}

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades under the respective names of number restrictions and cardinality restrictions on concepts. Recently, we have considerably extended the expressivity of such quantifiers by allowing to impose set and cardinality constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) on sets of role successors and concepts, respectively. We were able to prove that this extension does not increase the complexity of reasoning. In the present paper, we investigate the expressive power of the DLs obtained this way, using appropriate bisimulation characterizations and 0–1 laws as tools for distinguishing the expressiveness of different logics. In particular, we show that, in contrast to most classical DLs, these logics are no longer expressible in first-order predicate logic (FOL), and we characterize their first-order fragments. In most of our previous work on DLs with QFBAPA-based set and cardinality constraints we have employed finiteness restrictions on interpretations to ensure that the obtained sets are finite. Here we dispense with these restrictions to make the comparison with classical DLs, where one usually considers arbitrary models rather than finite ones, easier. It turns out that doing so does not change the complexity of reasoning.

@techreport{ BaBo-LTCS-19-09,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Filippo {De Bortoli}},
  doi = {https://doi.org/10.25368/2022.258},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaBo-LTCS-19-09}},
  number = {19-09},
  title = {{On the Complexity and Expressiveness of Description Logics with Counting}},
  type = {LTCS-Report},
  year = {2019},
}

Large-scale knowledge bases are at the heart of modern information systems. Their knowledge is inherently uncertain, and hence they are often materialized as probabilistic databases. However, probabilistic database management systems typically lack the capability to incorporate implicit background knowledge and, consequently, fail to capture some intuitive query answers. Ontology-mediated query answering is a popular paradigm for encoding commonsense knowledge, which can provide more complete answers to user queries. We propose a new data model that integrates the paradigm of ontology-mediated query answering with probabilistic databases, employing a log-linear probability model. We compare our approach to existing proposals, and provide supporting computational results.

@techreport{ BoCL-LTCS-19-10,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Ismail Ilkan {Ceylan} and Thomas {Lukasiewicz}},
  doi = {https://doi.org/10.25368/2023.221},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {19-10},
  title = {Ontology-Mediated Query Answering over Log-Linear Probabilistic Data (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. We propose a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic \(\mathcal{ELH}_\bot\), which is based on the minimal canonical model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity.

@techreport{ BoFo-LTCS-19-11,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Walter {Forkel}},
  doi = {https://doi.org/10.25368/2023.222},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {19-11},
  title = {Closed-World Semantics for Conjunctive Queries with Negation over {$\mathcal{ELH}_\bot$} Ontologies (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Lightweight temporal ontology languages have become a very active field of research in recent years. Many real-world applications, like processing electronic health records (EHRs), inherently contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. In this paper, we introduce a temporal extension of the tractable language \(\mathcal{ELH}_\bot\), which features a new class of convex diamond operators that can be used to bridge temporal gaps. We develop a completion algorithm for our logic, which shows that entailment remains tractable. Based on this, we develop a minimal-world semantics for answering metric temporal conjunctive queries with negation. We show that query answering is combined first-order rewritable, and hence in polynomial time in data complexity.

@techreport{ BoFK-LTCS-19-12,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Walter {Forkel} and Alisa {Kovtunova}},
  doi = {https://doi.org/10.25368/2023.223},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {19-12},
  title = {Finding New Diamonds: {T}emporal Minimal-World Query Answering over Sparse {AB}oxes (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

Selecting patients for clinical trials is very labor-intensive. Our goal is to develop an automated system that can support doctors in this task. This paper describes a major step towards such a system: the automatic translation of clinical trial eligibility criteria from natural language into formal, logic-based queries. First, we develop a semantic annotation process that can capture many types of clinical trial criteria. Then, we map the annotated criteria to the formal query language. We have built a prototype system based on state-of-the-art NLP tools such as Word2Vec, Stanford NLP tools, and the MetaMap Tagger, and have evaluated the quality of the produced queries on a number of criteria from clinicaltrials.gov. Finally, we discuss some criteria that were hard to translate, and give suggestions for how to formulate eligibility criteria to make them easier to translate automatically.

@techreport{ XFBBZ-LTCS-19-13,
  address = {Dresden, Germany},
  author = {Chao {Xu} and Walter {Forkel} and Stefan {Borgwardt} and Franz {Baader} and Beihai {Zhou}},
  doi = {https://doi.org/10.25368/2023.224},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {19-13},
  title = {Automatic Translation of Clinical Trial Eligibility Criteria into Formal Queries (Extended Version)},
  type = {LTCS-Report},
  year = {2019},
}

The classical approach for repairing a Description Logic ontology \(\mathfrak{O}\) in the sense of removing an unwanted consequence \(\alpha\) is to delete a minimal number of axioms from \(\mathfrak{O}\) such that the resulting ontology \(\mathfrak{O}'\) does not have the consequence \(\alpha\). However, the complete deletion of axioms may be too rough, in the sense that it may also remove consequences that are actually wanted. To alleviate this problem, we propose a more gentle way of repair in which axioms are not necessarily deleted, but only weakened. On the one hand, we investigate general properties of this gentle repair method. On the other hand, we propose and analyze concrete approaches for weakening axioms expressed in the Description Logic \(\mathcal{E\mkern-1.618mu L}\).

@techreport{ BaKrNuPe-LTCS-18-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah} and Rafael {Pe\~{n}aloza}},
  doi = {https://doi.org/10.25368/2022.238},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaKrNuPe-LTCS-18-01}},
  number = {18-01},
  title = {{Repairing Description Logic Ontologies by Weakening Axioms}},
  type = {LTCS-Report},
  year = {2018},
}

For a probabilistic extension of the description logic \(\mathcal{E\mkern-1.618mu L}^{\bot}\), we consider the task of automatic acquisition of terminological knowledge from a given probabilistic interpretation. Basically, such a probabilistic interpretation is a family of directed graphs the vertices and edges of which are labeled, and where a discrete probability measure on this graph family is present. The goal is to derive so-called concept inclusions which are expressible in the considered probabilistic description logic and which hold true in the given probabilistic interpretation. A procedure for an appropriate axiomatization of such graph families is proposed and its soundness and completeness is justified.

@techreport{ Kr-LTCS-18-03,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.239},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-18-03}},
  number = {18-03},
  title = {{Terminological Knowledge Acquisition in Probabilistic Description Logic}},
  type = {LTCS-Report},
  year = {2018},
}

Although being quite inexpressive, the description logic (DL) FL0, which provides only conjunction, value restriction and the top concept as concept constructors, has an intractable subsumption problem in the presence of terminologies (TBoxes): subsumption reasoning w.r.t. acyclic FL0 TBoxes is coNP-complete, and becomes even ExpTime-complete in case general TBoxes are used. In the present paper, we use automata working on infinite trees to solve both standard and non-standard inferences in FL0 w.r.t. general TBoxes. First, we give an alternative proof of the ExpTime upper bound for subsumption in FL0 w.r.t. general TBoxes based on the use of looping tree automata. Second, we employ parity tree automata to tackle non-standard inference problems such as computing the least common subsumer and the difference of FL0 concepts w.r.t. general TBoxes.

@techreport{ BaFePe-LTCS-18-04,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil} and Maximilian {Pensel}},
  doi = {https://doi.org/10.25368/2022.240},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {18-04},
  title = {Standard and Non-Standard Inferences in the Description Logic $\mathcal{FL}_0$ Using Tree Automata},
  type = {LTCS-Report},
  year = {2018},
}

Golog programs allow to model complex behaviour of agents by combining primitive actions defined in a Situation Calculus theory using imperative and non-deterministic programming language constructs. In general, verifying temporal properties of Golog programs is undecidable. One way to establish decidability is to restrict the logic used by the program to a Description Logic (DL), for which recently some complexity upper bounds for verification problem have been established. However, so far it was open whether these results are tight, and lightweight DLs such as EL have not been studied at all. Furthermore, these results only apply to a setting where actions do not consume time, and the properties to be verified only refer to the timeline in a qualitative way. In a lot of applications, this is an unrealistic assumption. In this work, we study the verification problem for timed Golog programs, in which actions can be assigned differing durations, and temporal properties are specified in a metric branching time logic. This allows to annotate temporal properties with time intervals over which they are evaluated, to specify for example that some property should hold for at least n time units, or should become specified within some specified time window. We establish tight complexity bounds of the verification problem for both expressive and lightweight DLs. Our lower bounds already apply to a very limited fragment of the verification problem, and close open complexity bounds for the non-metrical cases studied before.

@techreport{ KoZa-LTCS-18-06,
  address = {Dresden, Germany},
  author = {Patrick {Koopmann} and Benjamin {Zarrie{\ss}}},
  doi = {https://doi.org/10.25368/2022.241},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-06},
  title = {On the Complexity of Verifying Timed {Golog} Programs over Description Logic Actions (Extended Version)},
  type = {LTCS-Report},
  year = {2018},
}

Especially in the field of stream reasoning, there is an increased interest in reasoning about temporal data in order to detect situations of interest or complex events. Ontologies have been proved a useful way to infer missing information from incomplete data, or simply to allow for a higher order vocabulary to be used in the event descriptions. Motivated by this, ontology-based temporal query answering has been proposed as a means for the recognition of situations and complex events. But often, the data to be processed do not only contain temporal information, but also probabilistic information, for example because of uncertain sensor measurements. While there has been a plethora of research on ontology-based temporal query answering, only little is known so far about querying temporal probabilistic data using ontologies. This work addresses this problem by introducing a temporal query language that extends a well-investigated temporal query language with probability operators, and investigating the complexity of answering queries using this query language together with ontologies formulated in the description logic EL.

@techreport{ Ko-LTCS-18-07,
  address = {Dresden, Germany},
  author = {Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.242},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-07},
  title = {Ontology-Mediated Query Answering for Probabilistic Temporal Data with {$\mathcal{EL}$} Ontologies (Extended Version)},
  type = {LTCS-Report},
  year = {2018},
}

Description Logic actions specify adaptations of description logic interpretations based on some preconditions defined using a description logic. We consider DL actions in which preconditions can be specified using DL axioms as well as using conjunctive queries, and combinatiosn thereof. We investigate complexity bounds for the executability and the projection problem for these actions, which respectively ask whether an action can be executed on models of an interpretation, and which entailments are satisfied after an action has been executed on this model. In addition, we consider a set of new reasoning tasks concerned with conflicts and interactions that may arise if two action are executed at the same time. Since these problems have not been investigated before for Description Logic actions, we investigate the complexity of these tasks both for actions with conjunctive queries and without those. Finally, we consider the verification problem for Golog programs formulated over our famility of actions. Our complexity analysis considers several expressive DLs, and we provide tight complexity bounds for those for which the exact complexity of conjunctive query entailment is known.

@techreport{ Ko-LTCS-18-08,
  address = {Dresden, Germany},
  author = {Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.243},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-08},
  title = {Actions with Conjunctive Queries: Projection, Conflict Detection and Verification},
  type = {LTCS-Report},
  year = {2018},
}

Modeling context-dependent systems for their analysis is challenging as verification tools usually rely on an input language close to imperative programming languages which need not support description of contexts well. We introduce the concept of contextualized programs where operational behaviors and context knowledge are modeled separately using domain-specific formalisms. For behaviors specified in stochastic guarded-command language and contextual knowledge given by OWL description logic ontologies, we develop a technique to eficiently incorporate contextual information into behavioral descriptions by reasoning about the ontology. We show how our presented concepts support and facilitate the quantitative analysis of context-dependent systems using probabilistic model checking. For this, we evaluate our implementation on a case study issuing a multi-server system.

@techreport{ DuKoTu-LTCS-18-09,
  address = {Dresden, Germany},
  author = {Clemens {Dubslaff} and Patrick {Koopmann} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.244},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-09},
  title = {Contextualized Programs for Ontology-Mediated Probabilistic System Analysis},
  type = {LTCS-Report},
  year = {2018},
}

For the description logic \(\mathcal{E\mkern-1.618mu L}\), we consider the neighborhood relation which is induced by the subsumption order, and we show that the corresponding lattice of \(\mathcal{E\mkern-1.618mu L}\) concept descriptions is distributive, modular, graded, and metric. In particular, this implies the existence of a rank function as well as the existence of a distance function.

@techreport{ Kr-LTCS-18-10,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.245},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-18-10}},
  number = {18-10},
  title = {{The Distributive, Graded Lattice of $\mathcal{E\mkern-1.618mu L}$ Concept Descriptions and its Neighborhood Relation (Extended Version)}},
  type = {LTCS-Report},
  year = {2018},
}

The notion of a most specific consequence with respect to some terminological box is introduced, conditions for its existence in the description logic \(\mathcal{E\mkern-1.618mu L}\) and its variants are provided, and means for its computation are developed. Algebraic properties of most specific consequences are explored. Furthermore, several applications that make use of this new notion are proposed and, in particular, it is shown how given terminological knowledge can be incorporated in existing approaches for the axiomatization of observations. For instance, a procedure for an incremental learning of concept inclusions from sequences of interpretations is developed.

@techreport{ Kr-LTCS-18-11,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.246},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-18-11}, accepted for publication in {Discrete Applied Mathematics}},
  number = {18-11},
  title = {{Most Specific Consequences in the Description Logic $\mathcal{E\mkern-1.618mu L}$}},
  type = {LTCS-Report},
  year = {2018},
}

Description logics in their standard setting only allow for representing and reasoning with crisp knowledge without any degree of uncertainty. Of course, this is a serious shortcoming for use cases where it is impossible to perfectly determine the truth of a statement. For resolving this expressivity restriction, probabilistic variants of description logics have been introduced. Their model-theoretic semantics is built upon so-called probabilistic interpretations, that is, families of directed graphs the vertices and edges of which are labeled and for which there exists a probability measure on this graph family.

Results of scientific experiments, e.g., in medicine, psychology, or biology, that are repeated several times can induce probabilistic interpretations in a natural way. In this document, we shall develop a suitable axiomatization technique for deducing terminological knowledge from the assertional data given in such probabilistic interpretations. More specifically, we consider a probabilistic variant of the description logic \(\mathcal{E\mkern-1.618mu L}^{\!\bot}\), and provide a method for constructing a set of rules, so-called concept inclusions, from probabilistic interpretations in a sound and complete manner.

@techreport{ Kr-LTCS-18-12,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.247},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-18-12}},
  number = {18-12},
  title = {{Learning Description Logic Axioms from Discrete Probability Distributions over Description Graphs (Extended Version)}},
  type = {LTCS-Report},
  year = {2018},
}

We investigate ontology-based query answering for data that are both temporal and probabilistic, which might occur in contexts such as stream reasoning or situation recognition with uncertain data. We present a framework that allows to represent temporal probabilistic data, and introduce a query language with which complex temporal and probabilistic patterns can be described. Specifically, this language combines conjunctive queries with operators from linear time logic as well as probability operators. We analyse the complexities of evaluating queries in this language in various settings. While in some cases, combining the temporal and the probabilistic dimension in such a way comes at the cost of increased complexity, we also determine cases for which this increase can be avoided.

@techreport{ Koopmann18tr,
  address = {Dresden, Germany},
  author = {Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.248},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-13},
  title = {Ontology-Based Query Answering for Probabilistic Temporal Data (Extended Version)},
  type = {LTCS-Report},
  year = {2018},
}

Ontology-based access to large data-sets has recently gained a lot of attention. To access data efficiently, one approach is to rewrite the ontology into Datalog, and then use powerful Datalog engines to compute implicit entailments. Existing rewriting techniques support Description Logics (DLs) from \(\mathcal{ELH}\) to Horn-\(\mathcal{SHIQ}\). We go one step further and present one such data-independent rewriting technique for Horn-\(\mathcal{SRIQ}_\sqcap\), the extension of Horn-\(\mathcal{SHIQ}\) that supports role chain axioms, an expressive feature prominently used in many real-world ontologies. We evaluated our rewriting technique on a large known corpus of ontologies. Our experiments show that the resulting rewritings are of moderate size, and that our approach is more efficient than state-of-the-art DL reasoners when reasoning with data-intensive ontologies.

@techreport{ CaGoKo-18-14,
  author = {David {Carral} and Larry {Gonz\'alez} and Patrick {Koopmann}},
  doi = {https://doi.org/10.25368/2022.249},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {18-14},
  title = {From {Horn}-{$\mathcal{SRIQ}$} to {Datalog}: A Data-Independent Transformation that Preserves Assertion Entailment (Extended Version)},
  type = {LTCS-Report},
  year = {2018},
}

Defeasible Description Logics (DDLs) extend Description Logics with defeasible concept inclusions. Reasoning in DDLs often employs rational or relevant closure according to the (propositional) KLM postulates. If in DDLs with quantification a defeasible subsumption relationship holds between concepts, this relationship might also hold if these concepts appear in existential restrictions. Such nested defeasible subsumption relationships were not detected by earlier reasoning algorithms—neither for rational nor relevant closure. In this report, we present a new approach for EL_bot that alleviates this problem for relevant closure (the strongest form of preferential reasoning currently investigated) by the use of typicality models that extend classical canonical models by domain elements that individually satisfy any amount of consistent defeasible knowledge. We also show that a certain restriction on the domain of the typicality models in this approach yields inference results that correspond to the (weaker) more commonly known rational closure.

@techreport{ PeTu-LTCS-17-01,
  address = {Dresden, Germany},
  author = {Maximilian {Pensel} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.231},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {17-01},
  title = {Making Quantification Relevant again---the Case of Defeasible $\mathcal{EL}_{\bot}$},
  type = {LTCS-Report},
  year = {2017},
}

We introduce a new description logic that extends the well-known logic ALCQ by allowing the statement of constraints on role successors that are more general than the qualified number restrictions of ALCQ. To formulate these constraints, we use the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA), in which one can express Boolean combinations of set constraints and numerical constraints on the cardinalities of sets. Though our new logic is considerably more expressive than ALCQ, we are able to show that the complexity of reasoning in it is the same as in ALCQ, both without and with TBoxes.

@techreport{ Baad-LTCS-17-02,
  address = {Dresden, Germany},
  author = {Franz {Baader}},
  doi = {https://doi.org/10.25368/2022.232},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {17-02},
  title = {Concept Descriptions with Set Constraints and Cardinality Constraints},
  type = {LTCS-Report},
  year = {2017},
}

In contrast to qualitative linear temporal logics, which can be used to state that some property will eventually be satisfied, metric temporal logics allow to formulate constraints on how long it may take until the property is satisfied. While most of the work on combining Description Logics (DLs) with temporal logics has concentrated on qualitative temporal logics, there has recently been a growing interest in extending this work to the quantitative case. In this paper, we complement existing results on the combination of DLs with metric temporal logics over the natural numbers by introducing interval-rigid names. This allows to state that elements in the extension of certain names stay in this extension for at least some specified amount of time.

@techreport{ BaBoKoOzTh-LTCS-17-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Ana {Ozaki} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.233},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {17-03},
  title = {Metric Temporal Description Logics with Interval-Rigid Names (Extended Version)},
  type = {LTCS-Report},
  year = {2017},
}

We investigate ontology-based query answering (OBQA) in a setting where both the ontology and the query can refer to concrete values such as numbers and strings. In contrast to previous work on this topic, the built-in predicates used to compare values are not restricted to being unary. We introduce restrictions on these predicates and on the ontology language that allow us to reduce OBQA to query answering in databases using the so-called combined rewriting approach. Though at first sight our restrictions are different from the ones used in previous work, we show that our results strictly subsume some of the existing first-order rewritability results for unary predicates.

@techreport{ BaBL-LTCS-17-04,
  address = {Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}},
  doi = {https://doi.org/10.25368/2022.234},
  institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden},
  note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {17-04},
  title = {Query Rewriting for \textit{{DL-Lite}} with {$n$}-ary Concrete Domains (Extended Version)},
  type = {LTCS-Report},
  year = {2017},
}

We consider ontology-based query answering in a setting where some of the data are numerical and of a probabilistic nature, such as data obtained from uncertain sensor readings. The uncertainty for such numerical values can be more precisely represented by continuous probability distributions than by discrete probabilities for numerical facts concerning exact values. For this reason, we extend existing approaches using discrete probability distributions over facts by continuous probability distributions over numerical values. We determine the exact (data and combined) complexity of query answering in extensions of the well-known description logics EL and ALC with numerical comparison operators in this probabilistic setting.

@techreport{ BaKoTu-LTCS-17-05,
  address = {Germany},
  author = {Franz {Baader} and Patrick {Koopmann} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.235},
  institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden},
  note = {See \url{https://lat.inf.tu-dresden.de/research/reports.html}},
  number = {17-05},
  title = {Using Ontologies to Query Probabilistic Numerical Data (Extended Version)},
  type = {LTCS-Report},
  year = {2017},
}

In ontology-based systems that process data stemming from different sources and that is received over time, as in context-aware systems, reasoning needs to cope with the temporal dimension and should be resilient against inconsistencies in the data. Motivated by such settings, this paper addresses the problem of handling inconsistent data in a temporal version of ontology-based query answering. We consider a recently proposed temporal query language that combines conjunctive queries with operators of propositional linear temporal logic and extend to this setting three inconsistency-tolerant semantics that have been introduced for querying inconsistent description logic knowledge bases. We investigate their complexity for DL-Lite_R temporal knowledge bases, and furthermore complete the picture for the consistent case.

@techreport{ BoTu-LTCS-17-06,
  address = {Dresden, Germany},
  author = {Camille {Bourgaux} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.236},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {see \url{http://lat.inf.tu-dresden.de/research/reports.html}},
  number = {17-06},
  title = {Temporal Query Answering in {DL-Lite} over Inconsistent Data},
  type = {LTCS-Report},
  year = {2017},
}

We investigate the use of disunification in \(\mathcal{EL}\) for ontology generation. In particular, we study how disunification can construct new SNOMED CT concepts when given information about the position of the new concept in the concept hierarchy. To evaluate our approach, we randomly select concept names from SNOMED CT, remove their definitions, and formulate disunification problems that recover these definitions from information about the parents and siblings of the removed concept names. Our evaluation shows that this approach works well for some subhierarchies of SNOMED CT. Overall, one can reconstruct about 6% of all SNOMED CT concept names in this way.

@techreport{ BaBM-LTCS-17-07,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.237},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See https://tu-dresden.de/ing/informatik/thi/lat/forschung/technische-berichte.},
  number = {17-07},
  title = {Constructing {SNOMED CT} Concepts via Disunification},
  type = {LTCS-Report},
  year = {2017},
}

Probabilistic databases (PDBs) are usually incomplete, e.g., contain only the facts that have been extracted from the Web with high confidence. However, missing facts are often treated as being false, which leads to unintuitive results when querying PDBs. Recently, open-world probabilistic databases (OpenPDBs) were proposed to address this issue by allowing probabilities of unknown facts to take any value from a fixed probability interval. In this paper, we extend OpenPDBs by Datalog^± ontologies, under which both upper and lower probabilities of queries become even more informative, enabling us to distinguish queries that were indistinguishable before. We show that the dichotomy between P and PP in (Open)PDBs can be lifted to the case of first-order rewritable positive programs (without negative constraints); and that the problem can become NP^PP-complete, once negative constraints are allowed. We also propose an approximating semantics that circumvents the increase in complexity caused by negative constraints.

@techreport{ BoCL-LTCS-17-10,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Ismail Ilkan {Ceylan} and Thomas {Lukasiewicz}},
  doi = {https://doi.org/10.25368/2023.218},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {17-10},
  title = {Ontology-Mediated Queries for Probabilistic Databases (Extended Version)},
  type = {LTCS-Report},
  year = {2017},
}

Forming the foundations of large-scale knowledge bases, probabilistic databases have been widely studied in the literature. In particular, probabilistic query evaluation has been investigated intensively as a central inference mechanism. However, despite its power, query evaluation alone cannot extract all the relevant information encompassed in large-scale knowledge bases. To exploit this potential, we study two inference tasks; namely finding the most probable database and the most probable hypothesis for a given query. As natural counterparts of most probable explanations (MPE) and maximum a posteriori hypotheses (MAP) in probabilistic graphical models, they can be used in a variety of applications that involve prediction or diagnosis tasks. We investigate these problems relative to a variety of query languages, ranging from conjunctive queries to ontology-mediated queries, and provide a detailed complexity analysis.

@techreport{ CeBL-LTCS-17-11,
  address = {Dresden, Germany},
  author = {Ismail Ilkan {Ceylan} and Stefan {Borgwardt} and Thomas {Lukasiewicz}},
  doi = {https://doi.org/10.25368/2023.220},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {17-11},
  title = {Most Probable Explanations for Probabilistic Database Queries (Extended Version)},
  type = {LTCS-Report},
  year = {2017},
}

Reasoning for Description Logics with concrete domains and w.r.t. general TBoxes easily becomes undecidable. However, with some restriction on the concrete domain, decidability can be regained. We introduce a novel way to integrate a concrete domain D into the well known description logic ALC, we call the resulting logic ALCP(D). We then identify sufficient conditions on D that guarantee decidability of the satisfiability problem, even in the presence of general TBoxes. In particular, we show decidability of ALCP(D) for several domains over the integers, for which decidability was open. More generally, this result holds for all negation-closed concrete domains with the EHD-property, which stands for `the existence of a homomorphism is definable'. Such technique has recently been used to show decidability of CTL* with local constraints over the integers.

@techreport{ CaTu-LTCS-16-01,
  address = {Dresden, Germany},
  author = {Claudia {Carapelle} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.225},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {16-01},
  title = {Decidability of $\mathcal{ALC}^P\!(\mathcal{D})$ for concrete domains with the EHD-property},
  type = {LTCS-Report},
  year = {2016},
}

In a previous paper, we have introduced an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we have defined a graded membership function deg, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C t for   in <, <=, >, >= then collect all the individuals that belong to C with degree  t. We have then investigated the complexity of reasoning in the Description Logic tEL(deg), which is obtained from EL by adding such threshold concepts. In the present paper, we extend these results, which were obtained for reasoning without TBoxes, to the case of reasoning w.r.t. acyclic TBoxes. Surprisingly, this is not as easy as might have been expected. On the one hand, one must be quite careful to define acyclic TBoxes such that they still just introduce abbreviations for complex concepts, and thus can be unfolded. On the other hand, it turns out that, in contrast to the case of EL, adding acyclic TBoxes to tEL(deg) increases the complexity of reasoning by at least on level of the polynomial hierarchy.

@techreport{ BaFe-LTCS-16-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}},
  doi = {https://doi.org/10.25368/2022.226},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {16-02},
  title = {Extending the Description Logic $\tau\mathcal{EL}(deg)$ with Acyclic TBoxes},
  type = {LTCS-Report},
  year = {2016},
}

Unification with constants modulo the theory of an associative (A), commutative (C) and idempotent (I) binary function symbol with a unit (U) corresponds to solving a very simple type of set equations. It is well-known that solvability of systems of such equations can be decided in polynomial time by reducing it to satisfiability of propositional Horn formulae. Here we introduce a modified version of this problem by no longer requiring all equations to be completely solved, but allowing for a certain number of violations of the equations. We introduce three different ways of counting the number of violations, and investigate the complexity of the respective decision problem, i.e., the problem of deciding whether there is an assignment that solves the system with at most \(\ell\) violations for a given threshold value \(\ell\).

@techreport{ BaMaOk-LTCS-16-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Pavlos {Marantidis} and Alexander {Okhotin}},
  doi = {https://doi.org/10.25368/2022.227},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {16-03},
  title = {Approximately Solving Set Equations},
  type = {LTCS-Report},
  year = {2016},
}

Unification in description logics (DLs) has been introduced as a novel inference service that can be used to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. It was first investigated in detail for the DL \(\mathcal{FL}_0\), where unification can be reduced to solving certain language equations. In order to increase the recall of this method for finding redundancies, we introduce and investigate the notion of approximate unification, which basically finds pairs of concepts that ``almost'' unify. The meaning of ``almost'' is formalized using distance measures between concepts. We show that approximate unification in \(\mathcal{FL}_0\) can be reduced to approximately solving language equations, and devise algorithms for solving the latter problem for two particular distance measures.

@techreport{ BaMaOk-LTCS-16-04,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Pavlos {Marantidis} and Alexander {Okhotin}},
  doi = {https://doi.org/10.25368/2022.228},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {16-04},
  title = {Approximate Unification in the Description Logic {$\mathcal{FL}_0$}},
  type = {LTCS-Report},
  year = {2016},
}

In a recent research paper, we have proposed an extension of the light-weight Description Logic (DL) EL in which concepts can be defined in an approximate way. To this purpose, the notion of a graded membership function m, which instead of a Boolean membership value 0 or 1 yields a membership degree from the interval [0,1], was introduced. Threshold concepts can then, for example, require that an individual belongs to a concept C with degree at least 0.8. Reasoning in the threshold DL tel(m) obtained this way of course depends on the employed graded membership function m. The paper defines a specific such function, called deg, and determines the exact complexity of reasoning in tel(deg). In addition, it shows how concept similarity measures (CSMs)   satisfying certain properties can be used to define graded membership functions m , but it does not investigate the complexity of reasoning in the induced threshold DLs tel(m ). In the present paper, we start filling this gap. In particular, we show that computability of   implies decidability of tel(m ), and we introduce a class of CSMs for which reasoning in the induced threshold DLs has the same complexity as in tel(deg).

@techreport{ BaFe-LTCS-16-07,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}},
  doi = {https://doi.org/10.25368/2022.229},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {16-07},
  title = {Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures},
  type = {LTCS-Report},
  year = {2016},
}

Recently introduced approaches for relaxed query answering, approximately defining concepts, and approximately solving unification problems in Description Logics have in common that they are based on the use of concept comparison measures together with a threshold construction. In this paper, we will briefly review these approaches, and then show how weighted automata working on infinite trees can be used to construct computable concept comparison measures for FL0 that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures in the mentioned approximation approaches.

@techreport{ BaFM-LTCS-16-08,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil} and Pavlos {Marantidis}},
  doi = {https://doi.org/10.25368/2022.230},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {16-08},
  title = {Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in $\mathcal{FL}_0$},
  type = {LTCS-Report},
  year = {2016},
}

In this paper, we explore how ontological knowledge expressed via existential rules can be combined with possibilistic networks (i) to represent qualitative preferences along with domain knowledge, and (ii) to realize preference-based answering of conjunctive queries (CQs). We call these combinations ontological possibilistic networks (OP-nets). We define skyline and k-rank answers to CQs under preferences and provide complexity (including data tractability) results for deciding consistency and CQ skyline membership for OP-nets. We show that our formalism has a lower complexity than a similar existing formalism.

@techreport{ BFLST-LTCS-16-10,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Bettina {Fazzinga} and Thomas {Lukasiewicz} and Akanksha {Shrivastava} and Oana {Tifrea-Marciuska}},
  doi = {https://doi.org/10.25368/2023.219},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {16-10},
  title = {Preferential Query Answering in the {S}emantic {W}eb with Possibilistic Networks (Extended Version)},
  type = {LTCS-Report},
  year = {2016},
}

It is well-known that the canonical implicational base of all implications valid w.r.t. a closure operator can be obtained from the set of all pseudo-closures. NextClosures is a parallel algorithm to compute all closures and pseudo-closures of a closure operator in a graded lattice, e.g., in a powerset. Furthermore, the closures and pseudo-closures can be constrained, and partially known closure operators can be explored.

@techreport{ Kr-LTCS-15-01,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-15-01}},
  number = {15-01},
  title = {{NextClosures -- Parallel Exploration of Constrained Closure Operators}},
  type = {LTCS-Report},
  year = {2015},
}

Model-based most specific concept descriptions are a useful means to compactly represent all knowledge about a certain individual of an interpretation that is expressible in the underlying description logic. Existing approaches only cover their construction in the case of \(\mathcal{E\mkern-1.618mu L}\) and \(\mathcal{F\mkern-1.618mu L\mkern-1.618mu E}\) w.r.t. greatest fixpoint semantics, and the case of \(\mathcal{E\mkern-1.618mu L}\) w.r.t. a role-depth bound, respectively. This document extends the results towards the more expressive description logic \(\mathcal{A\mkern-1.618mu L\mkern-1.618mu E\mkern-1.618mu Q}^{\geq}\mkern-1.618mu\mathcal{N}^{\leq}\mkern-1.618mu(\mathsf{Self})\) w.r.t. role-depth bounds and also gives a method for the computation of least common subsumers.

@techreport{ Kr-LTCS-15-02,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-15-02}},
  number = {15-02},
  title = {{Model-Based Most Specific Concept Descriptions and Least Common Subsumers in $\mathcal{A\mkern-1.618mu L\mkern-1.618mu E\mkern-1.618mu Q}^{\geq}\mkern-1.618mu\mathcal{N}^{\leq}\mkern-1.618mu(\mathsf{Self})$}},
  type = {LTCS-Report},
  year = {2015},
}

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.

@techreport{ BaBM-LTCS-15-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.210},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-03},
  title = {Dismatching and Local Disunification in {$\mathcal{EL}$}},
  type = {LTCS-Report},
  year = {2015},
}

To represent and reason about contextualized knowledge often two-dimensional Description Logics (DLs) are employed, where one DL is used to describe contexts (or possible worlds) and the other DL is used to describe the objects, i.e. the relational structure of the specific contexts. Previous approaches for DLs of context that combined pairs of DLs resulted in undecidability in those cases where so-called rigid roles are admitted, i.e. if parts of the relational structure are the same in all contexts. In this paper, we present a novel combination of pairs of DLs and show that reasoning stays decidable even in the presence of rigid roles. We give complexity results for various combinations of DLs involving ALC, SHOQ, and EL.

@techreport{ BoLi-LTCS-15-04,
  author = {Stephan {B{\"o}hme} and Marcel {Lippmann}},
  doi = {https://doi.org/10.25368/2022.211},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {15-04},
  title = {Description Logics of Context with Rigid Roles Revisited},
  type = {LTCS-Report},
  year = {2015},
}

Fuzzy Description Logics (DLs) are used to represent and reason about vague and imprecise knowledge that is inherent to many application domains. It was recently shown that the complexity of reasoning in finitely-valued fuzzy DLs is often not higher than that of the underlying classical DL. We show that this does not hold for fuzzy extensions of the light-weight DL EL, which is used in many biomedical ontologies, under the Lukasiewicz semantics. The complexity of reasoning increases from PTime to ExpTime, even if only one additional truth value is introduced. The same lower bound holds also for infinitely-valued Lukasiewicz extensions of EL.

@techreport{ BoCP-LTCS-15-06,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Marco {Cerami} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.212},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-06},
  title = {Subsumption in Finitely Valued Fuzzy {$\mathcal{EL}$}},
  type = {LTCS-Report},
  year = {2015},
}

We investigate a combination of EL-axioms with operators of the linear-temporal logic LTL. The complexity of deciding satisfiability is reduced when compared to ALC-LTL, but we also identify one setting where it remains the same. We additionally investigate the setting where GCIs are restricted to hold globally (at all time points), in which case the problem is PSpace-complete.

@techreport{ BoTh-LTCS-15-07,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.213},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-07},
  title = {{LTL} over {$\mathcal{EL}$} Axioms},
  type = {LTCS-Report},
  year = {2015},
}

Context-aware systems use data about their environment for adaptation at runtime, e.g., for optimization of power consumption or user experience. Ontology-based data access (OBDA) can be used to support the interpretation of the usually large amounts of data. OBDA augments query answering in databases by dropping the closed-world assumption (i.e., the data is not assumed to be complete any more) and by including domain knowledge provided by an ontology. We focus on a recently proposed temporalized query language that allows to combine conjunctive queries with the operators of the well-known propositional temporal logic LTL. In particular, we investigate temporalized OBDA w.r.t. ontologies in the DL EL, which allows for efficient reasoning and has been successfully applied in practice. We study both data and combined complexity of the query entailment problem.

@techreport{ BoTh-LTCS-15-08,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.214},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-08},
  title = {Temporal Query Answering in {$\mathcal{EL}$}},
  type = {LTCS-Report},
  year = {2015},
}

We introduce an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we use a graded membership function, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C  _t for   in <,<=,>,>= then collect all the individuals that belong to C with degree   t. We generalize a well-known characterization of membership in EL concepts to construct a specific graded membership function deg, and investigate the complexity of reasoning in the Description Logic tel(deg), which extends EL by threshold concepts defined using deg. We also compare the instance problem for threshold concepts of the form C_{> t} in tel(deg) with the relaxed instance queries of Ecke et al.

@techreport{ BaBrF-LTCS-15-09,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Gerhard {Brewka} and Oliver Fern{\'a}ndez {Gil}},
  doi = {https://doi.org/10.25368/2022.215},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-09},
  title = {Adding Threshold Concepts to the Description Logic $\mathcal{E\!L}$},
  type = {LTCS-Report},
  year = {2015},
}

A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, and that we then use to build knowledge-based programs with test conditions expressed in the epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.

@techreport{ ZaCl-LTCS-15-10,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}},
  doi = {https://doi.org/10.25368/2022.216},
  institution = {Chair of Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html},
  number = {15-10},
  title = {Verification of Knowledge-Based Programs over Description Logic Actions},
  type = {LTCS-Report},
  year = {2015},
}

Fuzzy Description Logics (FDLs) combine classical Description Logics with the semantics of Fuzzy Logics in order to represent and reason with vague knowledge. Most FDLs using truth values from the interval [0,1] have been shown to be undecidable in the presence of a negation constructor and general concept inclusions. One exception are those FDLs whose semantics is based on the infinitely valued Gödel t-norm (G). We extend previous decidability results for the FDL G-ALC to deal with complex role inclusions, nominals, inverse roles, and qualified number restrictions. Our novel approach is based on a combination of the known crispification technique for finitely valued FDLs and an automata-based procedure for reasoning in G-ALC.

@techreport{ BoPe-LTCS-15-11,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.217},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-11},
  title = {Infinitely Valued G{\"o}del Semantics for Expressive Description Logics},
  type = {LTCS-Report},
  year = {2015},
}

Ontology-based data access augments classical query answering over fact bases by adopting the open-world assumption and by including domain know-ledge provided by an ontology. We implemented temporal query answering w.r.t. ontologies formulated in the Description Logic DL-Lite. Focusing on temporal conjunctive queries (TCQs), which combine conjunctive queries via the operators of propositional linear temporal logic, we regard three approaches for answering them: an iterative algorithm that considers all data available; a window-based algorithm; and a rewriting approach, which translates the TCQs to be answered into SQL queries. Since the relevant ontological knowledge is already encoded into the latter queries, they can be answered by a standard database system. Our evaluation especially shows that implementations of both the iterative and the window-based algorithm answer TCQs within a few milliseconds, and that the former achieves a constant performance, even if data is growing over time.

@techreport{ THOe-LTCS-15-12,
  address = {Dresden, Germany},
  author = {Veronika {Thost} and Jan {Holste} and \"Ozg\"ur {\"Oz\c{c}ep}},
  doi = {https://doi.org/10.25368/2022.218},
  institution = {Chair of Automata Theory, TU Dresden},
  number = {15-12},
  title = {On Implementing Temporal Query Answering in {\textit{DL-Lite}}},
  type = {LTCS-Report},
  year = {2015},
}

Description logic knowledge bases can be used to represent knowledge about a particular domain in a formal and unambiguous manner. Their practical relevance has been shown in many research areas, especially in biology and the semantic web. However, the tasks of constructing knowledge bases itself, often performed by human experts, is difficult, time-consuming and expensive. In particular the synthesis of terminological knowledge is a challenge every expert has to face. Because human experts cannot be omitted completely from the construction of knowledge bases, it would therefore be desirable to at least get some support from machines during this process. To this end, we shall investigate in this work an approach which shall allow us to extract terminological knowledge in the form of general concept inclusions from factual data, where the data is given in the form of vertex and edge labeled graphs. As such graphs appear naturally within the scope of the Semantic Web in the form of sets of RDF triples, the presented approach opens up the possibility to extract terminological knowledge from the Linked Open Data Cloud. We shall also present first experimental results showing that our approach has the potential to be useful for practical applications.

@techreport{ BoDiKr-LTCS-15-13,
  address = {Dresden, Germany},
  author = {Daniel {Borchmann} and Felix {Distel} and Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.219},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BoDiKr-LTCS-15-13}},
  number = {15-13},
  title = {{Axiomatization of General Concept Inclusions from Finite Interpretations}},
  type = {LTCS-Report},
  year = {2015},
}

Probabilistic interpretations consist of a set of interpretations with a shared domain and a measure assigning a probability to each interpretation. Such structures can be obtained as results of repeated experiments, e.g., in biology, psychology, medicine, etc. A translation between probabilistic and crisp description logics is introduced and then utilised to reduce the construction of a base of general concept inclusions of a probabilistic interpretation to the crisp case for which a method for the axiomatisation of a base of GCIs is well-known.

@techreport{ Kr-LTCS-15-14,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  doi = {https://doi.org/10.25368/2022.220},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#Kr-LTCS-15-14}},
  number = {15-14},
  title = {{Learning General Concept Inclusions in Probabilistic Description Logics}},
  type = {LTCS-Report},
  year = {2015},
}

Ontology-based query answering augments classical query answering in databases by adopting the open-world assumption and by including domain knowledge provided by an ontology. We investigate temporal query answering w.r.t. ontologies formulated in DL-Lite, a family of description logics that captures the conceptual features of relational databases and was tailored for efficient query answering. We consider a recently proposed temporal query language that combines conjunctive queries with the operators of propositional linear temporal logic (LTL). In particular, we consider negation in the ontology and query language, and study both data and combined complexity of query entailment.

@techreport{ BoTh-LTCS-15-16,
  address = {Germany},
  author = {Stefan {Borgwardt} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.221},
  institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden},
  number = {15-16},
  title = {Temporal Query Answering in {{\textit{DL-Lite}}} with Negation},
  type = {LTCS-Report},
  year = {2015},
}

In Ontology-Based Data Access (OBDA), user queries are evaluated over a set of facts under the open world assumption, while taking into account background knowledge given in the form of a Description Logic (DL) ontology. In order to deal with dynamically changing data sources, temporal conjunctive queries (TCQs) have recently been proposed as a useful extension of OBDA to support the processing of temporal information. We extend the existing complexity analysis of TCQ entailment to very expressive DLs underlying the OWL 2 standard, and in contrast to previous work also allow for queries containing transitive roles.

@techreport{ BaBL-LTCS-15-17,
  address = {Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}},
  doi = {https://doi.org/10.25368/2022.222},
  institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden},
  number = {15-17},
  title = {Temporal Conjunctive Queries in Expressive {DLs} with Non-simple Roles},
  type = {LTCS-Report},
  year = {2015},
}

Fuzzy description logics (FDLs) are knowledge representation formalisms capable of dealing with imprecise knowledge by allowing intermediate membership degrees in the interpretation of concepts and roles. One option for dealing with these intermediate degrees is to use the so-called Gödel semantics. Despite its apparent simplicity, developing reasoning techniques for expressive FDLs under this semantics is a hard task. We present a tableau algorithm for deciding consistency of a SROIQ ontology under Gödel semantics. This is the first algorithm that can handle the full expressivity of SROIQ as well as the full Gödel semantics.

@techreport{ BoPe-LTCS-15-18,
  address = {Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.223},
  institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden},
  number = {15-18},
  title = {A Tableau Algorithm for {$\mathcal{SROIQ}$} under Infinitely Valued {G}{\"o}del Semantics},
  type = {LTCS-Report},
  year = {2015},
}

The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language's high expressiveness in terms of first-order quantification and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be context-free (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action's parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we present a new, more general class of action theories (called acyclic) that allows for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for acyclic theories in the two-variable fragment of first-order logic, verification of CTL* properties of programs over ground actions is decidable.

@techreport{ ZaCla-LTCS-15-19,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}},
  doi = {https://doi.org/10.25368/2022.224},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {15-19},
  title = {Decidable Verification of Golog Programs over Non-Local Effect Actions},
  type = {LTCS-Report},
  year = {2015},
}

Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system's behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any point in time yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to a trace satisfy (violate) the formula. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use the more expressive temporal logic ALC-LTL, which can use axioms of the Description Logic (DL) ALC instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behaviour provides us with complete information about the states of the system, we assume that states are described in an incomplete way by ALC-knowledge bases. We show that also in this setting monitors can effectively be constructed. The (double-exponential) size of the constructed monitors is in fact optimal, and not higher than in the propositional case. As an auxiliary result, we show how to construct Büchi automata for ALC-LTL-formulae, which yields alternative proofs for the known upper bounds of deciding satisfiability in ALC-LTL.

@techreport{ BaLi-LTCS-14-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Marcel {Lippmann}},
  doi = {https://doi.org/10.25368/2022.203},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-01},
  title = {Runtime Verification Using a Temporal Description Logic Revisited},
  type = {LTCS-Report},
  year = {2014},
}

The complexity of reasoning in fuzzy description logics (DLs) over finite lattices usually does not exceed that of the underlying classical DLs. This has recently been shown for the logics between L-IALC and L-ISCHI using a combination of automata- and tableau-based techniques. In this report, this approach is modified to deal with nominals and constants in L-ISCHOI. Reasoning w.r.t. general TBoxes is ExpTime-complete, and PSpace-completeness is shown under the restriction to acyclic terminologies in two sublogics. The latter implies two previously unknown complexity results for the classical DLs ALCHO and SO.

@techreport{ Borg-LTCS-14-02,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt}},
  doi = {https://doi.org/10.25368/2022.204},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-02},
  title = {The Complexity of Fuzzy Description Logics over Finite Lattices with Nominals},
  type = {LTCS-Report},
  year = {2014},
}

Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics (DLs) almost 20 years ago, motivated by applications in the Classic system. For the DL EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBoxes that satisfy a certain restriction on cyclic dependencies between concepts, but the general case is still open. For matching, we solve the general case in this paper: we show that matching in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented matching algorithm that uses non-deterministic rules to transform a given matching problem into a solved form by a polynomial number of rule applications. We also investigate some tractable variants of the matching problem.

@techreport{ BaMo-LTCS-14-3,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.205},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {14-03},
  title = {Matching with respect to general concept inclusions in the Description Logic $\mathcal{EL}$},
  type = {LTCS-Report},
  year = {2014},
}

Rough Description Logics have recently been studied as a means for representing and reasoning with imprecise knowledge. Real-world applications need to exploit reasoning over such knowledge in an efficient way. We describe how the combined approach to query answering can be extended to the rough setting. In particular, we extend both the canonical model and the rewriting procedure such that rough queries over rough EL ontologies can be answered by considering this information alone.

@techreport{ PeTT-LTCS-14-04,
  address = {Dresden, Germany},
  author = {Rafael {Pe{\~n}aloza} and Veronika {Thost} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.206},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-04},
  title = {Conjunctive Query Answering in Rough EL},
  type = {LTCS-Report},
  year = {2014},
}

Ontology repair remains one of the main bottlenecks for the development of ontologies for practical use. Many automated methods have been developed for suggesting potential repairs, but ultimately human intervention is required for selecting the adequate one, and the human expert might be overwhelmed by the amount of information delivered to her. We propose a decomposition of ontologies into smaller components that can be repaired in parallel. We show the utility of our approach for ontology repair, provide algorithms for computing this decomposition through standard reasoning, and study the complexity of several associated problems.

@techreport{ MaPe-LTCS-14-05,
  address = {Dresden, Germany},
  author = {Yue {Ma} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.207},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-05},
  title = {Towards Parallel Repair Using Decompositions},
  type = {LTCS-Report},
  year = {2014},
}

Recently, a lot of research has combined description logics (DLs) of the DL-Lite family with temporal formalisms. Such logics are proposed to be used for situation recognition and temporalized ontology-based data access. In this report, we consider DL-Lite-LTL, in which axioms formulated in a member of the DL-Lite family are combined using the operators of propositional linear-time temporal logic (LTL). We consider the satisfiability problem of this logic in the presence of so-called rigid symbols whose interpretation does not change over time. In contrast to more expressive temporalized DLs, the computational complexity of this problem is the same as for LTL, even w.r.t. rigid symbols.

@techreport{ BoLT-LTCS-13-05,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.208},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {14-06},
  title = {Reasoning with Temporal Properties over Axioms of \textit{DL-Lite}},
  type = {LTCS-Report},
  year = {2014},
}

Developing and maintaining ontologies is an expensive and error-prone task. After an error is detected, users may have to wait for a long time before a corrected version of the ontology is available. In the meantime, one might still want to derive meaningful knowledge from the ontology, while avoiding the known errors. We study error-tolerant reasoning tasks in the description logic . While these problems are intractable, we propose methods for improving the reasoning times by precompiling information about the known errors and using proof-theoretic techniques for computing justifications. A prototypical implementation shows that our approach is feasible for large ontologies used in practice.

@techreport{ LuPe-LTCS-14-11,
  address = {Dresden, Germany},
  author = {Michel {Ludwig} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.209},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-11},
  title = {Error-Tolerant Reasoning in the Description Logic EL},
  type = {LTCS-Report},
  year = {2014},
}

Ontology-based data access (OBDA) generalizes query answering in databases towards deduction since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as ontology language we use the prototypical expressive DL ALC. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem.

@techreport{ BaBoLi-LTCS-13-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}},
  doi = {https://doi.org/10.25368/2022.191},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {13-01},
  title = {On the Complexity of Temporal Query Answering},
  type = {LTCS-Report},
  year = {2013},
}

We present a general form of attribute exploration, a knowledge completion algorithm from formal concept analysis. The aim of this generalization is to extend the applicability of attribute exploration by a general description. Additionally, this may also allow for viewing different existing variants of attribute exploration as instances of a general form, as for example exploration on partial contexts.

@techreport{ Borc-LTCS-13-02,
  address = {Dresden, Germany},
  author = {Daniel {Borchmann}},
  doi = {https://doi.org/10.25368/2022.192},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-02},
  title = {{A General Form of Attribute Exploration}},
  type = {LTCS-Report},
  year = {2013},
}

Snomed CT is a widely used medical ontology which is formally expressed in a fragment of the Description Logic EL++. The underlying logics allow for expressive querying, yet make it costly to maintain and extend the ontology. Existing approaches for ontology generation mostly focus on learning superclass or subclass relations and therefore fail to be used to generate Snomed CT definitions. In this paper, we present an approach for the extraction of Snomed CT definitions from natural language texts, based on the distance relation extraction approach. By benefiting from a relatively large amount of textual data for the medical domain and the rich content of Snomed CT, such an approach comes with the benefit that no manually labelled corpus is required. We also show that the type information for Snomed CT concept is an important feature to be examined for such a system. We test and evaluate the approach using two types of texts. Experimental results show that the proposed approach is promising to assist Snomed CT development.

@techreport{ MaDi-LTCS-13-03,
  address = {Dresden, Germany},
  author = {Yue {Ma} and Felix {Distel}},
  doi = {https://doi.org/10.25368/2022.193},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-03},
  title = {{Learning Formal Definitions for Snomed CT from Text}},
  type = {LTCS-Report},
  year = {2013},
}

Within formal concept analysis, attribute exploration is a powerful tool to semi-automatically check data for completeness with respect to a given domain. However, the classical formulation of attribute exploration does not take into account possible errors which are present in the initial data. We present in this work a generalization of attribute exploration based on the notion of confidence, which will allow for the exploration of implications which are not necessarily valid in the initial data, but instead enjoy a minimal confidence therein.

@techreport{ Borch-LTCS-13-04,
  address = {Dresden, Germany},
  author = {Daniel {Borchmann}},
  doi = {https://doi.org/10.25368/2022.194},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-04},
  title = {{Exploration by Confidence}},
  type = {LTCS-Report},
  year = {2013},
}

Ontology-based data access (OBDA) generalizes query answering in relational databases. It allows to query a database by using the language of an ontology, abstracting from the actual relations of the database. For ontologies formulated in Description Logics of the DL-Lite family, OBDA can be realized by rewriting the query into a classical first-order query, e.g. an SQL query, by compiling the information of the ontology into the query. The query is then answered using classical database techniques. In this report, we consider a temporal version of OBDA. We propose a temporal query language that combines a linear temporal logic with queries over DL-Lite-core-ontologies. This language is well-suited for expressing temporal properties of dynamical systems and is useful in context-aware applications that need to detect specific situations. Using a first-order rewriting approach, we transform our temporal queries into queries over a temporal database. We then present three approaches to answering the resulting queries, all having different advantages and drawbacks.

@techreport{ BoLT-LTCS-13-05,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}},
  doi = {https://doi.org/10.25368/2022.195},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {Revised version. See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-05},
  title = {Temporal Query Answering w.r.t.\ \textit{DL-Lite}-Ontologies},
  type = {LTCS-Report},
  year = {2013},
}

In the area of Description Logics the least common subsumer (lcs) and the most specific concept (msc) are inferences that generalize a set of concepts or an individual, respectively, into a single concept. If computed w.r.t. a general -TBox neither the lcs nor the msc need to exist. So far in this setting no exact conditions for the existence of lcs- or msc-concepts are known. This paper provides necessary and suffcient conditions for the existence of these two kinds of concepts. For the lcs of a fixed number of concepts and the msc we show decidability of the existence in PTime and polynomial bounds on the maximal role-depth of the lcs- and msc-concepts. The latter allows to compute the lcs and the msc, respectively.

@techreport{ ZaTu-LTCS-13-06,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\"s}} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.196},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {13-06},
  title = {Most Specific Generalizations w.r.t.\ General $\mathcal{EL}$-TBoxes},
  type = {LTCS-Report},
  year = {2013},
}

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and declarative semantics. We show that hybrid unification in EL is NP-complete and introduce a goal-oriented algorithm for computing hybrid unifiers.

@techreport{ BaFM-LTCS-13-07,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Oliver {Fern\'{a}ndez Gil} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.197},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {13-07},
  title = {Hybrid Unification in the Description Logic EL},
  type = {LTCS-Report},
  year = {2013},
}

@techreport{ BaZa-LTCS-13-08,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Benjamin {Zarrie{\"s}}},
  doi = {https://doi.org/10.25368/2022.198},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-08},
  title = {Verification of Golog Programs over Description Logic Actions},
  type = {LTCS-Report},
  year = {2013},
}

In the last few years there has been a large effort for analysing the computational properties of reasoning in fuzzy Description Logics. This has led to a number of papers studying the complexity of these logics, depending on their chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy DLs w.r.t. witnessed models over the Goedel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in this logic in exponential time, matching the complexity of reasoning in classical ALC.

@techreport{ BoDP-LTCS-13-09,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Felix {Distel} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.199},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-09},
  title = {Goedel Description Logics: Decidability in the Absence of the Finitely-Valued Model Property},
  type = {LTCS-Report},
  year = {2013},
}

Golog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL^*. Decidability is obtained by (1) resorting to the decidable first-order fragment C² as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects.

@techreport{ ZaCla-LTCS-13-10,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}},
  doi = {https://doi.org/10.25368/2022.200},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-10},
  title = {On the Decidability of Verifying LTL Properties of Golog Programs},
  type = {LTCS-Report},
  year = {2013},
}

We present an extensions of our previous work on axiomatizing confident general concept inclusions in given finite interpretations. Within this extension we allow external experts to interactively provide counterexamples to general concept inclusions with otherwise enough confidence in the given data. This extensions allows us to distinguish between erroneous counterexamples in the data and rare, but valid counterexamples.

@techreport{ Borc-LTCS-13-11,
  address = {Dresden, Germany},
  author = {Daniel {Borchmann}},
  doi = {https://doi.org/10.25368/2022.201},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-11},
  title = {{Model Exploration by Confidence with Completely Specified Counterexamples}},
  type = {LTCS-Report},
  year = {2013},
}

The notion of concept similarity is central to several ontology tasks and can be employed to realize relaxed versions of classical reasoning services. In this paper we investigate the reasoning service of answering instance queries in a relaxed fashion, where the query concept is relaxed by means of a concept similarity measure (CSM). To this end we investigate CSMs that assess the similarity of EL-concepts defined w.r.t. a general EL-TBox. We derive such a family of CSMs from a family of similarity measures for finite interpretations and show in both cases that the resulting measures enjoy a collection of formal properties. These properties allow us to devise an algorithm for computing relaxed instances w.r.t. general EL-TBoxes, where users can specify the `appropriate' notion of similarity by instanciating our CSM appropriately.

@techreport{ EcTu-TR-13,
  address = {Dresden, Germany},
  author = {Andreas {Ecke} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.202},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {13-12},
  title = {Similarity Measures for Computing Relaxed Instances w.r.t.\ General $\mathcal{EL}$-{TBoxes}},
  type = {LTCS-Report},
  year = {2013},
}

We extend previous results on the complexity of solving language equations with one-sided concatenation and all Boolean operations to the case where also disequations (i.e., negated equations) may occur. To show that solvability of systems of equations and disequations is still in ExpTime, we introduce a new type of automata working on infinite trees, which we call looping automata with colors. As applications of these results, we show new complexity results for disunification in the description logic FL0 and for monadic set constraints with negation. We believe that looping automata with colors may also turn out to be useful in other applications.

@techreport{ BaOk-LTCS-12-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Alexander {Okhotin}},
  doi = {https://doi.org/10.25368/2022.185},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-01},
  title = {Solving Language Equations and Disequations Using Looping Tree Automata with Colors},
  type = {LTCS-Report},
  year = {2012},
}

Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies.

@techreport{ BaBM-LTCS-12-02,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.186},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-02},
  title = {{SAT} Encoding of Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies},
  type = {LTCS-Report},
  year = {2012},
}

Unification has been investigated both in modal logics and in description logics, albeit with different motivations. In description logics, unification can be used to detect redundancies in ontologies. In this context, it is not sufficient to decide unifiability, one must also compute appropriate unifiers and present them to the user. For the description logic EL, which is used to define several large biomedical ontologies, deciding unifiability is an NP-complete problem. It is known that every solvable EL-unification problem has a minimal unifier, and that every minimal unifier is a local unifier. Existing unification algorithms for EL compute all minimal unifiers, but additionally (all or some) non-minimal local unifiers. Computing only the minimal unifiers would be better since there are considerably less minimal unifiers than local ones, and their size is usually also quite small. In this paper we investigate the question whether the known algorithms for EL-unification can be modified such that they compute exactly the minimal unifiers without changing the complexity and the basic nature of the algorithms. Basically, the answer we give to this question is negative.

@techreport{ BaBM-LTCS-12-03,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.187},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-03},
  title = {Computing Minimal {$\mathcal{EL}$}-Unifiers is Hard},
  type = {LTCS-Report},
  year = {2012},
}

Fuzzy description logics can be used to model vague knowledge in application domains. This paper analyses the consistency and satisfiability problems in the description logic SHI with semantics based on a complete residuated De Morgan lattice. The problems are undecidable in the general case, but can be decided by a tableau algorithm when restricted to finite lattices. For some sublogics of SHI, we provide upper complexity bounds that match the complexity of crisp reasoning.

@techreport{ BoPe-LTCS-12-04,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.188},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-04},
  title = {Consistency in Fuzzy Description Logics over Residuated De Morgan Lattices},
  type = {LTCS-Report},
  year = {2012},
}

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. A goal-oriented NP unification algorithm for EL that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this report, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.

@techreport{ BaBM-LTCS-12-05,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.189},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-05},
  title = {A Goal-Oriented Algorithm for Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies},
  type = {LTCS-Report},
  year = {2012},
}

In the work of Baader and Distel, a method has been proposed to axiomatize all general concept inclusions (GCIs) expressible in the description logic EL^bot and valid in a given interpretation I. This provides us with an effective method to learn EL^bot ontologies from interpretations, which itself can be seen as a different representation of linked data. In another report, we have extended this approach to handle errors in the data. This has been done by not only considering valid GCIs but also those whose confidence is above a certain threshold c. In the present work, we shall extend the results by describing another way to compute bases of confident GCIs. We furthermore provide experimental evidence that this approach can be useful for practical applications. We finally show that the technique of unravelling can also be used to effectively turn confident EL_gfp^bot bases into EL^bot bases.

@techreport{ Borc-LTCS-12-06,
  address = {Dresden, Germany},
  author = {Daniel {Borchmann}},
  doi = {https://doi.org/10.25368/2022.190},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {12-06},
  title = {On Confident GCIs of Finite Interpretations},
  type = {LTCS-Report},
  year = {2012},
}

Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of considerably lower complexity than unification in other DLs of similarly restricted expressive power. However, EL allows the use of the top concept, which represents the whole interpretation domain, whereas the large medical ontology SNOMED CT makes no use of this feature. Surprisingly, removing the top concept from EL makes the unification problem considerably harder. More precisely, we will show in this paper that unification in EL without the top concept is PSpace-complete.

@techreport{ BBBM-LTCS-11-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Nguyen Thanh {Binh} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.179},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-01},
  title = {Unification in the Description Logic {$\mathcal{EL}$} Without the Top Concept},
  type = {LTCS-Report},
  year = {2011},
}

Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation, and inclusion for weighted automata on infinite trees and show that they are not harder than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.

@techreport{ BoPe-LTCS-11-02,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.180},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-02},
  title = {Complementation and Inclusion of Weighted Automata on Infinite Trees: Revised Version},
  type = {LTCS-Report},
  year = {2011},
}

Very recently, the tableau-based algorithm for deciding consistency of general fuzzy DL ontologies over the product t-norm was shown to be incorrect, due to a very weak blocking condition. In this report we take the first steps towards a correct algorithm by modifying the blocking condition, such that the (finite) structure obtained through the algorithm uniquely describes an infinite system of quadratic constraints. We show that this procedure terminates, and is sound and complete in the sense that the input is consistent iff the corresponding infinite system of constraints is satisfiable.

@techreport{ Pena-LTCS-11-03,
  address = {Dresden, Germany},
  author = {Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.181},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-03},
  title = {Towards a Tableau Algorithm for Fuzzy ALC with Product T-norm},
  type = {LTCS-Report},
  year = {2011},
}

We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL₀. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.

@techreport{ BoMo-LTCS-11-04,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.182},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-04},
  title = {Finding Finite {H}erbrand Models},
  type = {LTCS-Report},
  year = {2011},
}

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of significantly lower complexity than unification in other DLs of similarly restricted expressive power. However, the unification algorithms for EL developed so far cannot deal with general concept inclusion axioms (GCIs). This paper makes a considerable step towards addressing this problem, but the GCIs our new unification algorithm can deal with still need to satisfy a certain cycle restriction.

@techreport{ BaBM-LTCS-11-05,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.183},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-05},
  title = {Unification in the Description Logic {$\mathcal{EL}$} w.r.t.\ Cycle-Restricted {TB}oxes},
  type = {LTCS-Report},
  year = {2011},
}

Fuzzy description logics (DLs) have been investigated for over two decades, due to their capacity to formalize and reason with imprecise concepts. Very recently, it has been shown that for several fuzzy DLs, reasoning becomes undecidable. Although the proofs of these results differ in the details of each specific logic considered, they are all based on the same basic idea. In this report, we formalize this idea and provide sufficient conditions for proving undecidability of a fuzzy DL. We demonstrate the effectiveness of our approach by strengthening all previously-known undecidability results and providing new ones. In particular, we show that undecidability may arise even if only crisp axioms are considered.

@techreport{ BoPe-LTCS-11-06,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.184},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-06},
  title = {Undecidability of Fuzzy Description Logics},
  type = {LTCS-Report},
  year = {2011},
}

In the reasoning about actions community, causal relationships have been proposed as a possible approach for solving the ramification problem, i.e., the problem of how to deal with indirect effects of actions. In this paper, we show that causal relationships can be added to action formalisms based on Description Logics without destroying the decidability of the consistency and the projection problem.

@techreport{ BaLiLi-LTCS-10-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Marcel {Lippmann} and Hongkai {Liu}},
  doi = {https://doi.org/10.25368/2022.174},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {10-01},
  title = {Adding Causal Relationships to {DL}-based Action Formalisms},
  type = {LTCS-Report},
  year = {2010},
}

The Description Logic EL is an inexpressive knowledge representation language, which nevertheless has recently drawn considerable attention in the knowledge representation and the ontology community since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problem in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification.

@techreport{ BaMo-LTCS-10-04,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Barbara {Morawska}},
  doi = {https://doi.org/10.25368/2022.177},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {10-04},
  title = {SAT Encoding of Unification in $\mathcal{EL}$},
  type = {LTCS-Report},
  year = {2010},
}

The least common subsumer (lcs) w.r.t general EL-TBoxes does not need to exists in general due to cyclic axioms. In this report we present an algorithm for computing role-depth bounded EL-lcs based on the completion algorithm for EL. We extend this computation algorithm to a recently introduced probabilistic variant of EL: Prob-EL-01.

@techreport{ PenTur-ltcs-10-02,
  address = {Germany},
  author = {Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.175},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-10-02},
  title = {Completion-based computation of least common subsumers with limited role-depth for {${\mathcal{EL}}$} and Prob-{${\mathcal{EL}^{01}}$}},
  type = {LTCS-Report},
  year = {2010},
}

In Description Logics the reasoning service most specific concept (msc) constructs a concept description that generalizes an ABox individual into a concept description. For the Description Logic EL the msc may not exist, if computed with respect to general EL-TBoxes or cyclic ABoxes. However, it is still possible to find a concept description that is the msc up to a fixed role-depth, i.e. with respect to a maximal nesting of quantifiers. In this report we present a practical approach for computing the role-depth bounded msc, based on the polynomial-time completion algorithm for EL. We extend these methods to ProbEL-01, which is a probabilistic variant of EL. Together with the companion report LTCS-10-02 this report devises computation methods for the bottom-up construction of knowledge bases for EL and ProbEL-01.

@techreport{ PenTur-ltcs-10-03,
  address = {Germany},
  author = {Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.25368/2022.176},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-10-03},
  title = {Completion-based computation of most specific concepts with limited role-depth for {${\mathcal{EL}}$} and Prob-{${\mathcal{EL}^{01}}$}},
  type = {LTCS-Report},
  year = {2010},
}

Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation and inclusion for weighted automata on infinite trees and show that they are not harder than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.

@techreport{ BoPe-ltcs-10-05,
  address = {Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.178},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-10-05},
  title = {Complementation and Inclusion of Weighted Automata on Infinite Trees},
  type = {LTCS-Report},
  year = {2010},
}

When trying to apply recently developed approaches for updating Description Logic ABoxes in the context of an action programming language, one encounters two problems. First, updates generate so-called Boolean ABoxes, which cannot be handled by traditional Description Logic reasoners. Second, iterated update operations result in very large Boolean ABoxes, which, however, contain a huge amount of redundant information. In this paper, we address both issues from a practical point of view.

@techreport{ LTCS-Report09-01,
  address = {Germany},
  author = {Conrad {Drescher} and Hongkai {Liu} and Franz {Baader} and Steffen {Guhlemann} and Uwe {Petersohn} and Peter {Steinke} and Michael {Thielscher}},
  doi = {https://doi.org/10.25368/2022.170},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {09-01},
  title = {Putting ABox Updates into Action},
  type = {LTCS-Report},
  year = {2009},
}

Consider an ontology O where every axiom is labeled with an element of a lattice L. Then every element l of L determines a sub-ontology O_l, which consists of the axioms of O whose labels are greater or equal to l. These labels may be interpreted as required access rights, in which case O_l is the sub-ontology that a user with access right l is allowed to see, or as trust levels, in which case O_l consists of those axioms that we trust with level at least l. Given a consequence C (such as a subsumption relationship between concepts) that follows from the whole ontology O, we want to know from which of the sub-ontologies O_l, determined by lattice elements l, C still follows. However, instead of reasoning with O_l in the deployment phase of the ontology, we want to pre-compute this information during the development phase. More precisely, we want to compute what we call a boundary for C, i.e., an element m_C of L such that C follows from O_l iff l is smaller or equal to m_C. In this paper we show that, under certain restrictions on the elements l used to define the sub-ontologies, such a boundary always exists, and we describe black-box approaches for computing it that are generalizations of approaches for axiom pinpointing in description logics. We also present first experimental results that compare the efficiency of these approaches on real-world ontologies.

@techreport{ BaKP-LTCS-09,
  address = {Germany},
  author = {Franz {Baader} and Martin {Knechtel} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.171},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {09-02},
  title = {Computing Boundaries for Reasoning in Sub-Ontologies},
  type = {LTCS-Report},
  year = {2009},
}

We investigate the computational complexity of axiom pinpointing in Description Logics, which is the task of finding minimal subsets of a knowledge base that have a given consequence. We consider the problems of enumerating such subsets with and without order, and show hardness results that already hold for the propositional Horn fragment, or for the Description Logic . We show complexity results for several other related decision and enumeration problems for these fragments that extend to more expressive logics. In particular we show that hardness of these problems depends not only on expressivity of the fragment but also on the shape of the axioms used.

@techreport{ PeSe-LTCS-09-04,
  address = {Germany},
  author = {Rafael {Pe{\~n}aloza} and Bar\i{}\c{s} {Sertkaya}},
  doi = {https://doi.org/10.25368/2022.173},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {09-04},
  title = {On the Complexity of Axiom Pinpointing in Description Logics},
  type = {LTCS-Report},
  year = {2009},
}

The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a Büchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.

@techreport{ BMLSW-LTCS-09-03,
  address = {Germany},
  author = {Franz {Baader} and Hongkai {Liu} and Anees ul {Mehdi}},
  doi = {https://doi.org/10.25368/2022.172},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-09-03},
  title = {{I}ntegrate {A}ction {F}ormalisms into {L}inear {T}emporal {D}escription {L}ogics},
  type = {LTCS-Report},
  year = {2009},
}

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.

@techreport{ LTCS-Report08-01,
  address = {Germany},
  author = {Franz {Baader} and Silvio {Ghilardi} and Carsten {Lutz}},
  doi = {https://doi.org/10.25368/2022.164},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {08-01},
  title = {{LTL} over Description Logic Axioms},
  type = {LTCS-Report},
  year = {2008},
}

Non-standard inferences are particularly useful in the bottom-up construction of ontologies in Description Logics. One of the more common non-standard reasoning tasks is the most specific concept (msc) for an ABox-individual. In this paper we present similar non-standard reasoning task: model-based most specific concepts (model-mscs). We show that, although they look similar to ABox-mscs their computational behaviour can be different. We present constructions for model-mscs in the logics FLO and FLE with cyclic TBoxes and for ALC with acyclic TBoxes. Since subsumption in FLE with cyclic TBoxes has not been examined previously, we present a characterization of subsumption and give a construction for the least common subsumer in this setting.

@techreport{ Dist08,
  address = {Dresden, Germany},
  author = {Felix {Distel}},
  doi = {https://doi.org/10.25368/2022.167},
  institution = {Institute for theoretical computer science, TU Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {08-04},
  title = {Model-based Most Specific Concepts in Description Logics with Value Restrictions},
  year = {2008},
}

In a previous ICFCA paper we have shown that, in the Description Logics EL and ELgfp, the set of general concept inclusions holding in a finite model always has a finite basis. In this paper, we address the problem of how to compute this basis efficiently, by adapting methods from formal concept analysis.

@techreport{ BaaDi08,
  address = {Dresden},
  author = {Franz {Baader} and Felix {Distel}},
  doi = {https://doi.org/10.25368/2022.168},
  institution = {Institute for Theoretical Computer Science, TU Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {08-05},
  title = {Exploring finite models in the Description Logic {$\mathcal{EL}_\mathrm{gfp}$}},
  type = {LTCS-Report},
  year = {2008},
}

Axiom pinpointing has been introduced in Description Logics (DLs) to help the used understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in consideration. Several pinpointing algorithms have been described as extensions of the standard tableau-based reasoning algorithms for deciding 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, using specific traits of them. In the past, we have developed a general approach for extending tableau-based algorithms into pinpointing algorithms. In this paper we explore some issues of termination of general tableaux and their pinpointing extensions. We also define a subclass of tableaux that allows the use of so-called blocking conditions, which stop the execution of the algorithm once a pattern is found, and adapt the pinpointing extensions accordingly, guaranteeing its correctness and termination.

@techreport{ BaPe-LTCS-07-01,
  address = {Germany},
  author = {Franz {Baader} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.165},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-08-02},
  title = {Blocking and Pinpointing in Forest Tableaux},
  type = {LTCS-Report},
  year = {2008},
}

Axiom pinpointing has been introduced in description logics (DLs) 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 ``tableau algorithms,'' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.

@techreport{ BaPe-LTCS-08-03,
  address = {Germany},
  author = {Franz {Baader} and Rafael {Pe{\~n}aloza}},
  doi = {https://doi.org/10.25368/2022.166},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-08-03},
  title = {Pinpointing in Terminating Forest Tableaux},
  type = {LTCS-Report},
  year = {2008},
}

We investigate the computational complexity of several decision, enumeration and counting problems related to pseudo-intents. We show that given a formal context and a set of its pseudo-intents, checking whether this context has an additional pseudo-intent is in coNP and it is at least as hard as checking whether a given simple hypergraph is saturated. We also show that recognizing the set of pseudo-intents is also in coNP and it is at least as hard as checking whether a given hypergraph is the transversal hypergraph of another given hypergraph. Moreover, we show that if any of these two problems turns out to be coNP-hard, then unless P = NP, pseudo-intents cannot be enumerated in output polynomial time. We also investigate the complexity of finding subsets of a given Duquenne-Guigues Base from which a given implication follows. We show that checking the existence of such a subset within a specified cardinality bound is NP-complete, and counting all such minimal subsets is #P-complete.

@techreport{ sert-08-06,
  address = {Germany},
  author = {Bar{\i}{\c{s}} {Sertkaya}},
  doi = {https://doi.org/10.25368/2022.169},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-08-06},
  title = {Some Computational Problems Related to Pseudo-intents},
  type = {LTCS-Report},
  year = {2008},
}

Formal Concept Analysis (FCA) can be used to analyze data given in the form of a formal context. In particular, FCA provides efficient algorithms for computing a minimal basis of the implications holding in the context. In this paper, we extend classical FCA by considering data that are represented by relational structures rather than formal contexts, and by replacing atomic attributes by complex formulae defined in some logic. After generalizing some of the FCA theory to this more general form of contexts, we instantiate the general framework with attributes defined in the Description Logic (DL) EL, and with relational structures over a signature of unary and binary predicates, i.e., models for EL. In this setting, an implication corresponds to a so-called general concept inclusion axiom (GCI) in EL. The main technical result of this report is that, in EL, for any finite model there is a finite set of implications (GCIs) holding in this model from which all implications (GCIs) holding in the model follow.

@techreport{ Dist07,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Felix {Distel}},
  doi = {https://doi.org/10.25368/2022.160},
  institution = {Inst.\ f{\"u}r Theoretische Informatik, TU Dresden},
  number = {07-02},
  title = {A finite basis for the set of {EL}-implications holding in a finite model},
  year = {2007},
}

The description logic EL+ has recently proved practically useful in the life science domain with presence of several large-scale biomedical ontologies such as SNOMED CT. To deal with ontologies of this scale, standard reasoning of classification is essential but not sufficient. The ability to extract relevant fragments from a large ontology and to incrementally classify it has become more crucial to support ontology design, maintenance and re-use. In this paper, we propose a pragmatic approach to module extraction and incremental classification for EL+ ontologies and report on empirical evaluations of our algorithms which have been implemented as an extension of the CEL reasoner.

@techreport{ Sun-07-LTCS,
  address = {Germany},
  author = {Boontawee {Suntisrivaraporn}},
  doi = {https://doi.org/10.25368/2022.161},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-07-03},
  title = {Module Extraction and Incremental Classification: A Pragmatic Approach for EL+ Ontologies},
  type = {LTCS-Report},
  year = {2007},
}

Language equations are equations where both the constants occurring in the equations and the solutions are formal languages. They have first been introduced in formal language theory, but are now also considered in other areas of computer science. In the present paper, we restrict the attention to language equations with one-sided concatenation, but in contrast to previous work on these equations, we allow not just union but all Boolean operations to be used when formulating them. In addition, we are not just interested in deciding solvability of such equations, but also in deciding other properties of the set of solutions, like its cardinality (finite, infinite, uncountable) and whether it contains least/greatest solutions. We show that all these decision problems are ExpTime-complete.

@techreport{ BaaderOkhotin-LTCS-06-01,
  address = {Germany},
  author = {Franz {Baader} and Alexander {Okhotin}},
  doi = {https://doi.org/10.25368/2022.154},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-01},
  title = {On Language Equations with One-sided Concatenation},
  type = {LTCS-Report},
  year = {2006},
}

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 assertional part 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 sense.

@techreport{ BGSS-LTCS-06-02,
  address = {Germany},
  author = {Franz {Baader} and Bernhard {Ganter} and Ulrike {Sattler} and Baris {Sertkaya}},
  doi = {https://doi.org/10.25368/2022.155},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-02},
  title = {Completing Description Logic Knowledge Bases using Formal Concept Analysis},
  type = {LTCS-Report},
  year = {2006},
}

Action formalisms based on description logics (DLs) have recently been introduced as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. However, existing DL action formalisms fail to include general TBoxes as provided by almost all state-of-the-art description logics. We define a DL action formalism that admits general TBoxes, propose a pragmatic approach to addressing the ramification problem that is introduced in this way, show that our formalim is decidable and perform a detailed investigation of its computational complexity.

@techreport{ LiLuMiWo-LTCS-06-03,
  address = {Germany},
  author = {H. {Liu} and C. {Lutz} and M. {Milicic} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.156},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-03},
  title = {Description Logic Actions with general {T}{B}oxes: a Pragmatic Approach},
  type = {LTCS-Report},
  year = {2006},
}

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.

@techreport{ BaaHlaPen-LTCS-06,
  address = {Germany},
  author = {F. {Baader} and J. {Hladik} and R. {Penaloza}},
  doi = {https://doi.org/10.25368/2022.157},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-04},
  title = {{PSPACE} Automata with Blocking for Description Logics},
  type = {LTCS-Report},
  year = {2006},
}

Tableau-based decision procedures have been successfully used for solving a wide variety of problems. For some applications, nonetheless, it is desirable not only to obtain a Boolean answer, but also to detect the causes for such a result. In this report, a method for finding explanations on tableau-based procedures is explored, generalizing previous results on the field. The importance and use of the method is shown by means of examples.

@techreport{ Penaloza-LTCS-06-05,
  address = {Germany},
  author = {Rafael {Penaloza}},
  doi = {https://doi.org/10.25368/2022.158},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-05},
  title = {Pinpointing in Tableaus},
  type = {LTCS-Report},
  year = {2006},
}

Axiom pinpointing has been introduced in description logics (DLs) 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.

@techreport{ BaaderPenaloza-LTCS-07-01,
  address = {Germany},
  author = {Franz {Baader} and Rafael {Penaloza}},
  doi = {https://doi.org/10.25368/2022.159},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-07-01},
  title = {Axiom Pinpointing in General Tableaux},
  type = {LTCS-Report},
  year = {2006},
}

Recently, it has been shown that the small DL EL, which allows for conjunction and existential restrictions, has better algorithmic properties than its counterpart FL0, which allows for conjunction and value restrictions. Whereas the subsumption problem in FL0 becomes already intractable in the presence of acyclic TBoxes, it remains tractable in EL even w.r.t. general concept inclusion axioms (GCIs). On the one hand, we will extend the positive result for EL by identifying a set of expressive means that can be added to EL without sacrificing tractability. On the other hand, we will show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even ExpTime-complete. In addition, we will show that subsumption in FL0 with GCIs is ExpTime complete.

@techreport{ BaaderBrandtLutz-LTCS-05-01,
  address = {Germany},
  author = {F. {Baader} and S. {Brandt} and C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.144},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-01},
  title = {Pushing the EL Envelope},
  type = {LTCS-Report},
  year = {2005},
}

Motivated by the need for semantically well-founded and algorithmically managable formalisms for describing the functionality of Web services, we introduce an action formalism that is based on description logics (DLs), but is also 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.

@techreport{ BMLSW-LTCS-05-02,
  address = {Germany},
  author = {F. {Baader} and M. {Milicic} and C. {Lutz} and U. {Sattler} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2010.145},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-02},
  title = {Integrating Description Logics and Action Formalisms for Reasoning about Web Services},
  type = {LTCS-Report},
  year = {2005},
}

The addition of metric operators to qualitative temporal logics often leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. The main result states that the language obtained by extending since/until logic of the real line with the operators "sometime within n time units", n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.

@techreport{ LutzWaltherWolter-LTCS-05-03,
  address = {Germany},
  author = {C. {Lutz} and D. {Walther} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.146},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-03},
  title = {Quantitative Temporal Logics: PSpace and below},
  type = {LTCS-Report},
  year = {2005},
}

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.

@techreport{ BaaderGhilardiLTCS-05-04,
  address = {Germany},
  author = {Franz {Baader} and Silvio {Ghilardi}},
  doi = {https://doi.org/10.25368/2022.147},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-04},
  title = {Connecting Many-Sorted Theories},
  type = {LTCS-Report},
  year = {2005},
}

In its many guises and variations, propositional dynamic logic (PDL) plays an important role 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).

@techreport{ Lutz-LTCS-05-05,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.148},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-05},
  title = {PDL with Intersection and Converse is Decidable},
  type = {LTCS-Report},
  year = {2005},
}

Recent applications of description logics (DLs) strongly suggest the integration of non-monotonic features into DLs, with particular attention to defeasible inheritance. However, the existing non-monotonic extensions of DLs are usually based on default logic or autoepistemic logic, and have to be seriously restricted in expressive power to preserve decidability of reasoning. In particular, such DLs allow the modelling of defeasible inheritance only in a very restricted form, where non-monotonic reasoning is limited to individuals that are explicitly identified by constants in the knowledge base. In this paper, we consider non-monotonic extensions of expressive DLs based on circumscription. We prove that reasoning in such DLs is decidable even without the usual, strong restrictions in expressive power. We pinpoint the exact computational complexity of reasoning as complete for NP^NExp and NExp^NP, depending on whether or not the number of minimized and fixed predicates is assumed to be bounded by a constant. These results assume that only concept names, but not role names can be minimized and fixed during minimization. On the other hand, we show that fixing role names during minimization leads to undecidability of reasoning.

@techreport{ BonattiLutzWolter-LTCS-05-06,
  address = {Germany},
  author = {P. {Bonatti} and C. {Lutz} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.149},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-06},
  title = {Expressive Non-Monotonic Description Logics Based on Circumscription},
  type = {LTCS-Report},
  year = {2005},
}

We identify a general property of concrete domains that is sufficient for proving decidability of DLs equipped with them and GCIs. We show that some useful concrete domains, such as a temporal one based on the Allen relations and a spatial one based on the RCC-8 relations, have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with such concrete domains.

@techreport{ LutzMilicic-LTCS-05-07,
  address = {Germany},
  author = {C. {Lutz} and M. {Milicic}},
  doi = {https://doi.org/10.25368/2022.150},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-07},
  title = {A Tableau Algorithm for DLs with Concrete Domains and GCIs},
  type = {LTCS-Report},
  year = {2005},
}

Motivated by a chemical process engineering application, we introduce a new concept constructor in Description Logics (DLs), an n-ary variant of the existential restriction constructor, which generalizes both the usual existential restrictions and so-called qualified number restrictions. We show that the new constructor can be expressed in ALCQ, the extension of the basic DL ALC by qualified number restrictions. However, this representation results in an exponential blow-up. By giving direct algorithms for ALC extended with the new constructor, we can show that the complexity of reasoning in this new DL is actually not harder than the one of reasoning in ALCQ. Moreover, in our chemical process engineering application, a restricted DL that provides only the new constructor together with conjunction, and satisfies an additional restriction on the occurrence of roles names, is sufficient. For this DL, the subsumption problem is polynomial.

@techreport{ BaaderEtAll-LTCS-05-08,
  address = {Germany},
  author = {Franz {Baader} and Carsten {Lutz} and Eldar {Karabaev} and Manfred {Thei{\ss}en}},
  doi = {https://doi.org/10.25368/2022.151},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-08},
  title = {A New $n$-ary Existential Quantifier in Description Logics},
  type = {LTCS-Report},
  year = {2005},
}

There is a recent trend of extending epistemic logic (EL) with dynamic operators that allow to express the evolution of knowledge and belief induced by knowledge-changing actions. The most basic such extension is public announcement logic (PAL), which is obtained from EL by adding an operator for truthful public announcements. In this paper, we consider the computational complexity of PAL and show that it coincides with that of EL. This holds in the single- and multi-agent case, and also in the presence of common knowledge operators. We also prove that there are properties that can be expressed exponentially more succinct in PAL than in EL. This shows that, despite the known fact that PAL and EL have the same expressive power, there is a benefit in adding the public announcement operator to EL: it exponentially increases the succinctness of formulas without having negative effects on computational complexity.

@techreport{ Lutz-LTCS-05-09,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.152},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-09},
  title = {Complexity and Succinctness of Public Announcement Logic},
  type = {LTCS-Report},
  year = {2005},
}

Description logic (DL) ABoxes are a tool for describing the states of affairs in an application domain. In this paper, we consider the problem of updating ABoxes when the state changes. We assume that changes are described at an atomic level, i.e., in terms of possibly negated ABox assertions that involve only atomic concepts and roles. We analyze such basic ABox updates in several standard DLs by investigating whether the updated ABox can be expressed in these DLs and, if so, whether it is computable and what is its size. It turns out that DLs have to include nominals and the ``@'' constructor of hybrid logic (or, equivalently, admit Boolean ABoxes) for updated ABoxes to be expressible. We give algorithms to compute updated ABoxes in several expressive DLs and exhibit ways to avoid an exponential blowup in the size of the original ABox. We also show that an exponential blowup in the size of the update information cannot be avoided (unless every PTime problem is LogTime-parallelizable).

@techreport{ LiLuMiWo-LTCS-05-10,
  address = {Germany},
  author = {H. {Liu} and C. {Lutz} and M. {Milicic} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.153},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-10},
  title = {Updating Description Logic ABoxes},
  type = {LTCS-Report},
  year = {2005},
}

In this paper we improve a goal-directed \(E\)-unification procedure by introducing a new rule, Cycle, for the case of collapsing equations, i.e. equations of the type x = v where x appears in v. In the case of these equations some obviously unnecessary infinite paths of inferences were possible, because it was not known if the inference system is still complete if the inferences were not allowed into positions of x in v. Cycle does not allow such inferences and we prove that the system is complete. Hence we prove that as in other approaches, inferences into variable positions in our goal-directed procedure are not needed.

@techreport{ Morawska-LTCS-04-01,
  address = {Germany},
  author = {B. {Morawska}},
  doi = {https://doi.org/10.25368/2022.138},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-01},
  title = {A nice Cycle Rule for Goal-Directed $E$-Unification},
  type = {LTCS-Report},
  year = {2004},
}

In two previous papers we have investigates the problem of computing the least common subsumer (lcs) and the most specific concept (msc) for the description logic EL in the presence of terminological cycles that are interpreted with descriptive semantics, which is the usual first-order semantics for description logics. In this setting, neither the lcs nor the msc needs to exist. We were able to characterize the cases in which the lcs/msc exists, but it was not clear whether this characterization yields decidability of the existence problem. In the present paper, we develop a common graph-theoretic generalization of these characterizations, and show that the resulting property is indeed decidable, thus yielding decidability of the existence of the lcs and the msc. This is achieved by expressing the property in monadic second-order logic on infinite trees. We also show that, if it exists, then the lcs/msc can be computed in polynomial time.

@techreport{ Baader-LTCS-04-02,
  address = {Germany},
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.139},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-02},
  title = {A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL},
  type = {LTCS-Report},
  year = {2004},
}

In the area of Description Logic (DL) based knowledge representation, research on reasoning w.r.t. general terminologies has mainly focused on very expressive DLs. Recently, though, it was shown for the DL EL, providing only the constructors conjunction and existential restriction, that the subsumption problem w.r.t. cyclic terminologies can be decided in polynomial time, a surprisingly low upper bound. In this paper, we show that even admitting general concept inclusion (GCI) axioms and role hierarchies in EL terminologies preserves the polynomial time upper bound for subsumption. We also show that subsumption becomes co-NP hard when adding one of the constructors number restriction, disjunction, and `allsome', an operator used in the DL K-Rep. An interesting implication of the first result is that reasoning over the widely used medical terminology SNOMED is possible in polynomial time.

@techreport{ Brandt-LTCS-04-03,
  address = {Germany},
  author = {S. {Brandt}},
  doi = {https://doi.org/10.25368/2022.140},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-03},
  title = {Reasoning in $\mathcal{ELH}$ w.r.t.\ General Concept Inclusion Axioms},
  type = {LTCS-Report},
  year = {2004},
}

Recently, it was shown for the DL EL that subsumption and instance problem w.r.t. cyclic terminologies can be decided in polynomial time. In this paper, we show that both problems remain tractable even when admitting general concept inclusion axioms and simple role inclusion axioms.

@techreport{ Brandt-LTCS-04-04,
  address = {Germany},
  author = {S. {Brandt}},
  doi = {https://doi.org/10.25368/2022.141},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-04},
  title = {Subsumption and Instance Problem in $\mathcal{ELH}$ w.r.t.\ General TBoxes},
  type = {LTCS-Report},
  year = {2004},
}

The eight topological RCC8 (or Egenhofer-Franzosa)-relations between spatial regions play a fundamental role in spatial reasoning, spatial and constraint databases, and geographical information systems. In analogy with Halpern and Shoham's modal logic of time intervals based on the Allen relations, we introduce a family of modal logics equipped with eight modal operators that are interpreted by the RCC8-relations. The semantics is based on region spaces induced by standard topological spaces, in particular the real plane. We investigate the expressive power and computational complexity of the logics obtained in this way. It turns our that, similar to Halpern and Shoham's logic, the expressive power is rather natural, but the computational behavior is problematic: topological modal logics are usually undecidable and often not even recursively enumerable. This even holds if we restrict ourselves to classes of finite region spaces or to substructures of region spaces induced by topological spaces. We also analyze modal logics based on the set of RCC5-relations, with similar results.

@techreport{ LutzWolter-LTCS-04-05,
  address = {Germany},
  author = {C. {Lutz} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.142},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-05},
  title = {Modal Logics of Topological Relations},
  type = {LTCS-Report},
  year = {2004},
}

Description Logics (DLs) with concrete domains are a useful tool in many applications. To further enhance the expressive power of such DLs, it has been proposed to add database-style key constraints. Up to now, however, only uniqueness constraints have been considered in this context, thus neglecting the second fundamental family of key constraints: functional dependencies. In this paper, we consider the basic DL with concrete domains , extend it with functional dependencies, and analyze the impact of this extension on the decidability and complexity of reasoning. Though intuitively the expressivity of functional dependencies seems weaker than that of uniqueness constraints, we are able to show that the former have a similarly severe impact on the computational properties: reasoning is undecidable in the general case, and -complete in some slightly restricted variants of our logic.

@techreport{ LutzMilicic-LTCS-04-06,
  address = {Germany},
  author = {C. {Lutz} and M. {Milicic}},
  doi = {https://doi.org/10.25368/2022.143},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-04-06},
  title = {Description Logics with Concrete Domains and Functional Dependencies},
  type = {LTCS-Report},
  year = {2004},
}

Description Logics (DLs) are a family of knowledge representation formalisms used for terminological reasoning. They have a wide range of applications such as medical knowledge-bases, or the semantic web. Research on DLs has been focused on the development of sound and complete inference algorithms to decide satisfiability and subsumption for increasingly expressive DLs. Non-standard inferences are a group of relatively new inference services which provide reasoning support for the building, maintaining, and deployment of DL knowledge-bases. So far, non-standard inferences are not available for very expressive DLs. In this paper we present first results on non-standard inferences for DLs with transitive roles. As a basis, we give a structural characterization of subsumption for DLs where existential and value restrictions can be imposed on transitive roles. We propose sound and complete algorithms to compute the least common subsumer (lcs).

@techreport{ BrTuKu-LTCS-03-02,
  address = {Germany},
  author = {S. {Brandt} and A.-Y. {Turhan} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.127},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  number = {03-02},
  title = {Foundations of non-standard Inferences for Description Logics with transitive Roles and Role Hierarchies},
  type = {LTCS-Report},
  year = {2003},
}

and non-standard inferences in the presence of terminological cycles for the description logic EL, which allows for conjunctions, existential restrictions, and the top concept. Regarding standard inference problems, it was shown there that the subsumption problem remains polynomial for all three types of semantics usually considered for cyclic definitions in description logics, and that the instance problem remains polynomial for greatest fixpoint semantics. Regarding non-standard inference problems, it was shown that, w.r.t. greatest fixpoint semantics, the least common subsumer and the most specific concept always exist and can be computed in polynomial time, and that, w.r.t. descriptive semantics, the least common subsumer need not exist. The present report is concerned with two problems left open by this previous work, namely the instance problem and the problem of computing most specific concepts w.r.t. descriptive semantics, which is the usual first-order semantics for description logics. We will show that the instance problem is polynomial also in this context. Similar to the case of the least common subsumer, the most specific concept w.r.t. descriptive semantics need not exist, but we are able to characterize the cases in which it exists and give a decidable sufficient condition for the existence of the most specific concept. Under this condition, it can be computed in polynomial time.

@techreport{ Baader-LTCS-03-01,
  address = {Germany},
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.126},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-03-01},
  title = {The Instance Problem and the Most Specific Concept in the Description Logic {$\mathcal{EL}$} w.r.t.\ Terminological Cycles with Descriptive Semantics},
  type = {LTCS-Report},
  year = {2003},
}

The report contains a proof of completeness of a goal-directed inference system for general \(E\)-unification with eager Variable Elimination. The proof is based on an analysis of a concept of ground, equational proof. The theory of equational proofs is developed in the first part. Solving variables in a goal is then shown to be reflected in defined transformations of an equational proof. The termination of these transformations proves termination of inferences with eager Variable Elimination.

@techreport{ Morawska-LTCS-03-03,
  address = {Germany},
  author = {B. {Morawska}},
  doi = {https://doi.org/10.25368/2022.128},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-03-03},
  title = {Completness of $E$-unification with eager Variable Elimination},
  type = {LTCS-Report},
  year = {2003},
}

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, it is long-known that 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 Buechi tree automata.

@techreport{ LuWa-LTCS-03-04,
  address = {Germany},
  author = {C. {Lutz} and D. {Walther}},
  doi = {https://doi.org/10.25368/2022.129},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-03-04},
  title = {PDL with Negation of Atomic Programs},
  type = {LTCS-Report},
  year = {2003},
}

Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics—whose combination is not disjoint since they share the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

@techreport{ BaGiTiLTCS-03-05,
  address = {Germany},
  author = {F. {Baader} and Silvio {Ghilardi} and Cesare {Tinelli}},
  doi = {https://doi.org/10.25368/2022.130},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-03-05},
  title = {A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics},
  type = {LTCS-Report},
  year = {2003},
}

An approximation of an ALC-concept by an ALE-concept can be computed in double exponential time. Consequently, one needs powerful optimization techniques for approximating an entire unfoldable TBox. Addressing this issue we identify a special form of ALC-concepts, which can be divided into parts s.t. each part can be approximated independently. This independent approximation in turn facilitates caching during the computation of approximation.

@techreport{ BrTu-LTCS-02,
  address = {Germany},
  author = {S. {Brandt} and A.-Y. {Turhan}},
  doi = {https://doi.org/10.25368/2022.121},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {02-03},
  title = {An Approach for Optimizing {ALE}-Approximation of {ALC}-Concepts},
  type = {LTCS-Report},
  year = {2002},
}

Entity Relationship (ER) diagrams are among the most popular formalisms for the support of database design. To aid database designers in building (extended) ER schemas, Description Logics (DLs) have been proposed and successfully used as a tool for reasoning about such schemas. In this paper, we propose the extension of ER diagrams with dependencies on attributes and show how such dependencies can be translated into DLs with concrete domains. The result is an integrated approach to reasoning with conceptual models and attribute dependencies.

@techreport{ Lutz-LTCS-02-01,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.119},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-02-01},
  title = {Reasoning about Entity Relationship Diagrams with Complex Attribute Dependencies},
  type = {LTCS-Report},
  year = {2002},
}

Cyclic definitions in description logics have until now been investigated only for description logics allowing for value restrictions. Even for the most basic language FL0, which allows for conjunction and value restrictions only, deciding subsumption in the presence of terminological cycles is a PSPACE-complete problem. This report investigates subsumption in the presence of terminological cycles for the language EL, which allows for conjunction and existential restrictions. In contrast to the results for FL0, subsumption in EL remains polynomial, independent of whether we use least fixpoint semantics, greatest fixpoint semantics, or descriptive semantics. These results are shown via a characterization of subsumption through the existence of certain simulation relations between nodes of the description graph associated with a given cyclic terminology.

@techreport{ Baader-LTCS-02-02,
  address = {Germany},
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.120},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-02},
  title = {Terminological Cycles in a Description Logic with Existential Restrictions},
  type = {LTCS-Report},
  year = {2002},
}

Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to "concrete" domains such as numbers and strings with built-in predicates such as <, +, and prefix-of. These hybrid DLs have turned out to be quite useful for reasoning about conceptual models of information systems, and as 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 naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.

@techreport{ LutAreHorSat-LTCS-02-04,
  address = {Germany},
  author = {C. {Lutz} and C. {Areces} and I. {Horrocks} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.122},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-04},
  title = {Keys, Nominals, and Concrete Domains},
  type = {LTCS-Report},
  year = {2002},
}

We analyze 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.

@techreport{ LutzSattlerTendera-LTCS-02-05,
  address = {Germany},
  author = {C. {Lutz} and U. {Sattler} and L. {Tendera}},
  doi = {https://doi.org/10.25368/2022.123},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-05},
  title = {The Complexity of Finite Model Reasoning in Description Logics},
  type = {LTCS-Report},
  year = {2002},
}

Motivated by medical terminology applications, we investigate the decidability of an expressive and prominent DL, SHIQ, extended with role inclusion axioms of the form R o S => T (where "o" denotes composition of binary relations). It is well-known that a naive such extension leads to undecidability, and thus we restrict our attention to axioms of the form R o S => R or S o R => 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 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 behaves well in practise and provides important additional functionality in a medical terminology application.

@techreport{ HorrocksSattler-LTCS-02-06,
  address = {Germany},
  author = {I. {Horrocks} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.124},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-06},
  title = {Decidability of {SHIQ} with Complex Role Inclusion Axioms},
  type = {LTCS-Report},
  year = {2002},
}

In a previous report we have investigates subsumption in the presence of terminological cycles for the description logic EL, which allows conjunctions, existential restrictions, and the top concept, and have shown that the subsumption problem remains polynomial for all three types of semantics usually considered for cyclic definitions in description logics. This result depends on a characterization of subsumption through the existence of certain simulation relations on the graph associated with a terminology. In the present report we will use this characterization to show how the most specific concept and the least common subsumer can be computed in EL with cyclic definitions. In addition, we show that subsumption in EL (with or without cyclic definitions) remains polynomial even if one adds a certain restricted form of global role-value-maps to EL. In particular, this kind of role-value-maps can express transitivity of roles.

@techreport{ Baader-LTCS-02-07,
  address = {Germany},
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.125},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-07},
  title = {Least Common Subsumers, Most Specific Concepts, and Role-Value-Maps in a Description Logic with Existential Restrictions and Terminological Cycles},
  type = {LTCS-Report},
  year = {2002},
}

Whereas matching in Description Logics is now relatively well-investigated, there are only very few formal results on matching under additional side conditions, though these side conditions were already present in the original paper by Borgida and McGuinness introducing matching in DLs. The present paper closes this gap for the DL \(\aln\) and its sublanguages.

@techreport{ BaaderBrandt+-LTCS-01-02,
  address = {Germany},
  author = {F. {Baader} and S. {Brandt} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.112},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {01-02},
  title = {Matching under Side Conditions in Description Logics},
  type = {LTCS-Report},
  year = {2001},
}

Tableaux-based decision procedures for satisfiability of modal and description logics behave quite well in practice, but it is sometimes hard to obtain exact worst-case complexity results using these approaches, especially for EXPTIME-complete logics.In contrast, automata-based approaches often yield algorithms for which optimal worst-case complexity can easily be proved. However, the algorithms obtained this way are usually not only worst-case, but also best-case exponential: they first construct an automaton that is always exponential in the size of the input, and then apply the (polynomial) emptiness test to this large automaton. To overcome this problem, one must try to construct the automaton ``on-the-fly'' while performing the emptiness test. In this paper we will show that Voronkov's inverse method for the modal logic K can be seen as an on-the-fly realization of the emptiness test done by the automata approach for K. The benefits of this result are two-fold. First, it shows that Voronkov's implementation of the inverse method, which behaves quite well in practice, is an optimized on-the-fly implementation of the automata-based satisfiability procedure for K. Second, it can be used to give a simpler proof of the fact that Voronkov's optimizations do not destroy completeness of the procedure. We will also show that the inverse method can easily be extended to handle global axioms, and that the correspondence to the automata approach still holds in this setting. In particular, the inverse method yields an EXPTIME-algorithm for satisfiability in K w.r.t. global axioms.

@techreport{ BaaderTobies-LTCS-01-03,
  address = {Germany},
  author = {F. {Baader} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.113},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {01-03},
  title = {The Inverse Method Implements the Automata Approach for Modal Satisfiability},
  type = {LTCS-Report},
  year = {2001},
}

Unification of concept descriptions was introduced by Baader and Narendran as a tool for detecting redundancies in knowledge bases. It was shown that unification in the small description logic FL₀, which allows for conjunction, value restriction, and the top concept only, is already ExpTime-complete. The present paper shows that the complexity does not increase if one additionally allows for composition, union, and transitive closure of roles. It also shows that matching (which is polynomial in FL₀) is PSpace-complete in the extended description logic. These results are proved via a reduction to linear equations over regular languages, which are then solved using automata. The obtained results are also of interest in formal language theory.

@techreport{ BaaderKuesters-LTCS-01-05,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.115},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {01-05},
  title = {Unification in a Description Logic with Transitive Closure of Roles},
  type = {LTCS-Report},
  year = {2001},
}

Approximation is a new inference service in Description Logics first mentioned by Baader, K&uuml;sters, and Molitor. Approximating a concept, defined in one Description Logic, means to translate this concept to another concept, defined in a second typically less expressive Description Logic, such that both concepts are as closely related as possible with respect to subsumption. The present paper provides the first in-depth investigation of this inference task. We prove that approximations from the Description Logic ALC to ALE always exist and propose an algorithm computing them. As a measure for the accuracy of the approximation, we introduce a syntax-oriented difference operator, which yields a concept description that contains all aspects of the approximated concept that are not present in the approximation. It is also argued that a purely semantical difference operator, as introduced by Teege, is less suited for this purpose. Finally, for the logics under consideration, we propose an algorithm computing the difference.

@techreport{ BrandtKuesters+-LTCS-01-06,
  address = {Germany},
  author = {S. {Brandt} and R. {K{\"u}sters} and A.-Y. {Turhan}},
  doi = {https://doi.org/10.25368/2022.116},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  number = {01-06},
  title = {Approximation and Difference in Description Logics},
  type = {LTCS-Report},
  year = {2001},
}

We show how to combine the standard tableau system for the basic description logic ALC with Wolper's tableau calculus for propositional temporal logic PTL in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic PTL_ALC interpreted in models with constant domains. We use the method of quasimodels to represent models with infinite domains, and the technique of minimal types to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics.

@techreport{ LuStuWoZa-LTCS-01-01,
  address = {Germany},
  author = {C. {Lutz} and H. {Sturm} and F. {Wolter} and M. {Zakharyaschev}},
  doi = {https://doi.org/10.25368/2022.111},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-01},
  title = {A Tableau Calculus for Temporal Description Logic: The Constant Domain Case},
  type = {LTCS-Report},
  year = {2001},
}

We introduce a modal language L which is obtained from standard modal logic by adding the difference operator and modal operators interpreted by boolean combinations and the converse of accessibility relations. It is proved that L has the same expressive power as the two-variable fragment FO² 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 FO² satisfiability is NExpTime-complete. We indicate that the relation between L and FO² provides a general framework for comparing modal and temporal languages with first-order languages.

@techreport{ LutzSattlerWolter-LTCS-01-04,
  address = {Germany},
  author = {C. {Lutz} and U. {Sattler} and F. {Wolter}},
  doi = {https://doi.org/10.25368/2022.114},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-04},
  title = {Modal Logic and the two-variable fragment},
  type = {LTCS-Report},
  year = {2001},
}

Recently, the Description Logic (DL) SHIQ has found a large number of applications. This success is due to the fact that SHIQ combines a rich expressivity with efficient reasoning, as is demonstrated by its implementation in DL systems such as FaCT and RACER. One weakness of SHIQ, however, limits its usability in several application areas: numerical knowledge such as knowledge about the age, weight, or temperature of real-world entities cannot be adequately represented. In this paper, we propose an extension of SHIQ that aims at closing this gap. The new Description Logic Q-SHIQ, which augments SHIQ by additional, ``concrete domain'' style concept constructors, allows to refer to rational numbers in concept descriptions, and also to define concepts based on the comparison of numbers via predicates such as ``<'' or ``=''. We argue that this kind of expressivity is needed in many application areas such as reasoning about the semantic web. We prove reasoning with Q-SHIQ to be ExpTime-complete (thus not harder than reasoning with SHIQ) by devising an automata-based decision procedure.

@techreport{ Lutz-LTCS-01-07,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.117},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-07},
  title = {Adding Numbers to the ${\cal SHIQ}$ Description Logic---First Results},
  type = {LTCS-Report},
  year = {2001},
}

The tableau algorithm implemented in the FaCT knowledge representation system decides satisfiability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. Intuitively, the algorithm searches for a tree-shaped abstraction of a model. To ensure termination of this algorithm without compromising correctness, it stops expanding paths in the search tree using a so-called ``double-blocking'' condition. <p> This condition was clearly more exacting than was strictly necessary, but it was assumed that more precisely defined blocking conditions would, on the one hand, make the proof of the algorithm's correctness far more difficult and, on the other hand (and more importantly), be so costly to check as to outweigh any benefit that might be derived. <p> However, FaCT's failure to solve UML derived knowledge bases led us to reconsider this conjecture and to formulate more precisely defined blocking conditions. We prove that the revised algorithm is still sound and complete, and demonstrate that it greatly improves FaCT's performance - in some cases by more than two orders of magnitude.

@techreport{ HorrocksSattler-LTCS-01-08,
  address = {Germany},
  author = {I. {Horrocks} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.118},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-08},
  title = {Optimised Reasoning for SHIQ},
  type = {LTCS-Report},
  year = {2001},
}

The problem of rewriting a concept given a terminology can informally be stated as follows: given a terminology T (i.e., a set of concept definitions) and a concept description C that does not contain concept names defined in T, can this description be rewritten into a "related better" description E by using (some of) the names defined in T? In this paper, we first introduce a general framework for the rewriting problem in description logics, and then concentrate on one specific instance of the framework, namely the minimal rewriting problem (where "better" means shorter, and "related" means equivalent). We investigate the complexity of the decision problem induced by the minimal rewriting problem for the languages FL0, ALN, ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings for the languages ALE and ALN. Finally, we sketch other interesting instances of the framework. Our interest for the minimal rewriting problem stems from the fact that algorithms for non-standard inferences, such as computing least common subsumers and matchers, usually produce concept descriptions not containing defined names. Consequently, these descriptions are rather large and hard to read and comprehend. First experiments in a chemical process engineering application show that rewriting can reduce the size of concept descriptions obtained as least common subsumers by almost two orders of magnitude.

@techreport{ BaaderKuestersMolitor-LTCS-00-04,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.107},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {00-04},
  title = {Rewriting Concepts Using Terminologies -- Revisited},
  type = {LTCS-Report},
  year = {2000},
}

Computing the most specific concept (msc) is an inference task that allows to abstract from individuals defined in description logic (DL) knowledge bases. For DLs that allow for number restrictions or existential restrictions, however, the msc need not exist unless one allows for cyclic concepts interpreted with the greatest fixed-point semantics. Since such concepts cannot be handled by current DL-systems, we propose to approximate the msc. We show that for the DL ALE, which has concept conjunction, a restricted form of negation, existential restrictions, and value restrictions as constructors, approximations of the msc always exist and can effectively be computed.

@techreport{ KuestersMolitor-LTCS-00-05,
  address = {RWTH Aachen, Germany},
  author = {R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.108},
  institution = {LuFG Theoretical Computer Science},
  number = {00-05},
  title = {Computing Most Specific Concepts in Description Logics with Existential Restrictions},
  type = {LTCS-Report},
  year = {2000},
}

Computing the least common subsumer (lcs) in description logics is an inference task first introduced for sublanguages of CLASSIC. Roughly speaking, the lcs of a set of concept descriptions is the most specific concept description that subsumes all of the input descriptions. As such, the lcs allows to extract the commonalities from given concept descriptions, a task essential for several applications like, e.g., inductive learning, information retrieval, or the bottom-up construction of KR-knowledge bases. Previous work on the lcs has concentrated on description logics that either allow for number restrictions or for existential restrictions. Many applications, however, require to combine these constructors. In this work, we present an lcs algorithm for the description logic ALEN, which allows for both constructors (as well as concept conjunction, primitive negation, and value restrictions). The proof of correctness of our lcs algorithm is based on an appropriate structural characterization of subsumption in ALEN also introduced in this paper.

@techreport{ KuestersMolitor-LTCS-00-07,
  address = {Germany},
  author = {R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.110},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {00-07},
  title = {Computing Least Common Subsumers in ALEN},
  type = {LTCS-Report},
  year = {2000},
}

Description Logics (DLs) are well-suited for the representation of abstract conceptual knowledge. Concrete knowledge such as knowledge about numbers, time intervals, and spatial regions can be incorporated into DLs by using so-called concrete domains. The basic Description Logics providing concrete domains is ALC(D) which was introduced by Baader and Hanschke. Reasoning with ALC(D) concepts is known to be PSpace-complete if reasoning with the concrete domain D is in PSpace. In this paper, we consider the following three extensions of ALC(D) and examine the computational complexity of the resulting formalism: <UL> <LI> acyclic TBoxes <LI> inverse roles, and <LI> a role-forming predicate constructor. </UL> As lower bounds, we show that there exists a concrete domain P for which reasoning is in PTime such that reasoning with ALC(P) and any of the above extensions (separately) is NExpTime-hard. This is rather surprising since acyclic TBoxes and inverse roles are known to ``usually'' not increase the complexity of reasoning. As a corresponding upper bound, we show that reasoning with ALC(D) and all of the above extensions (together) is in NExpTime if reasoning with the concrete domain D is in NP. For proving the lower bound, we introduce a NExpTime-complete variant of the Post Correspondence Problem and reduce it to the three logics under consideration. The upper bound is proved by giving a tableau algorithm.

@techreport{ Lutz-LTCS-00-01,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.104},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-00-01},
  title = {NExpTime-complete Description Logics with Concrete Domains},
  type = {LTCS-Report},
  year = {2000},
}

Boolean Modal Logics extend multi-modal K by allowing the use of boolean operators to define complex relation terms. In this paper, we investigate the complexity of reasoning with various such logics. The main results are that (1) adding negation of modal parameters to K makes reasoning ExpTime-complete, which is shown by using an automata-theoretic approach, and that (2) adding atomic negation and conjunction to K even yields a NExpTime- complete logic, which is shown by a reduction of a variant of the domino problem. 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. This is shown by a reduction to K enriched with the universal modality.

@techreport{ Lutz-Sattler-LTCS-00-02,
  address = {Germany},
  author = {C. {Lutz} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.105},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-00-02},
  title = {The Complexity of Reasoning with Boolean Modal Logics (Extended Version)},
  type = {LTCS-Report},
  year = {2000},
}

@techreport{ Hirsch-Tobies-LTCS-00-03,
  address = {Germany},
  author = {C. {Hirsch} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.106},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-00-03},
  title = {A Tableaux Algorithm for the Clique Guarded Fragment, Preliminary Version},
  type = {LTCS-Report},
  year = {2000},
}

Until now, interval-based temporal Description Logics (DLs) did—if at all—only admit TBoxes of a very restricted form, namely acyclic macro definitions. In this paper, we present a temporal DL that overcomes this deficieny and combines interval-based temporal reasoning with general TBoxes. We argue that this combination is very interesting for many application domains. An automata-based decision procedure is devised and a tight ExpTime-complexity bound is obtained. Since the presented logic can be viewed as being equipped with a concrete domain, our results can be seen from a different perspective: We show that there exist interesting concrete domains for which reasoning with general TBoxes in decidable.

@techreport{ Lutz-LTCS-00-06,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.109},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-00-06},
  title = {Interval-based Temporal Reasoning with General TBoxes},
  type = {LTCS-Report},
  year = {2000},
}

The problem of rewriting a concept given a terminology can informally be stated as follows: given a terminology T (i.e., a set of concept definitions) and a concept description C that does not contain concept names defined in T, can this description be rewritten into a "related better" description E by using (some of) the names defined in T? In this paper, we first introduce a general framework for the rewriting problem in description logics, and then concentrate on one specific instance of the framework, namely the minimal rewriting problem (where "better" means shorter, and "related" means equivalent). We investigate the complexity of the decision problem induced by the minimal rewriting problem for the languages FL0, ALN, ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings for the languages ALE and ALN. Finally, we sketch other interesting instances of the framework. Our interest for the minimal rewriting problem stems from the fact that algorithms for non-standard inferences, such as computing least common subsumers and matchers, usually produce concept descriptions not containing defined names. Consequently, these descriptions are rather large and hard to read and comprehend. First experiments in a chemical process engineering application show that rewriting can reduce the size of concept descriptions obtained as least common subsumers by almost two orders of magnitude.

@techreport{ BaaderKuestersMolitor-LTCS-99-12,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.97},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {Please refer to the revised version LTCS-Report 00-04.},
  number = {99-12},
  title = {Rewriting Concepts Using Terminologies -- Revisited},
  type = {LTCS-Report},
  year = {1999},
}

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.

@techreport{ Baader-Tinelli-Report-99-13,
  author = {Franz {Baader} and Cesare {Tinelli}},
  institution = {Department of Computer Science, University of Iowa},
  month = {October},
  number = {99-13},
  title = {Combining Equational Theories Sharing Non-Collapse-Free Constructors},
  year = {1999},
}

@techreport{ BorgidaKuesters-DCS-TR-391-1999,
  author = {A. {Borgida} and R. {K{\"u}sters}},
  institution = {Rutgers University, USA},
  number = {DCS-TR-391},
  title = {What's not in a name? {I}nitial Explorations of a Structural Approach to Integrating Large Concept Knowledge-Bases},
  year = {1999},
}

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.

@techreport{ KuestersBorgida-DCS-TR-404-1999,
  author = {R. {K{\"u}sters} and A. {Borgida}},
  institution = {Rutgers University, USA},
  number = {DCS-TR-404},
  title = {What's in an Attribute? {C}onsequences for the Least Common Subsumer},
  year = {1999},
}

Description logics are knowledge representation and reasoning formalisms which represent conceptual knowledge on an abstract logical level. Concrete domains are a theoretically well-founded approach to the integration of description logic reasoning with reasoning about concrete objects such as numbers, time intervals or spatial regions. In this paper, the complexity of combined reasoning with description logics and concrete domains is investigated. We extend ALC(D), which is the basic description logic for reasoning with concrete domains, by the operators "feature agreement" and "feature disagreement". For the extended logic, called ALCF(D), an algorithm for deciding the ABox consistency problem is devised. The strategy employed by this algorithm is vital for the efficient implementation of reasoners for description logics incorporating concrete domains. Based on the algorithm, it is proved that the standard reasoning problems for both logics ALC(D) and (D) are PSpace-complete - provided that the satisfiability test of the concrete domain used is in PSpace.

@techreport{ Lutz-LTCS-99-01,
  address = {Germany},
  author = {C. {Lutz}},
  doi = {https://doi.org/10.25368/2022.88},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.},
  number = {LTCS-99-01},
  title = {The Complexity of Reasoning with Concrete Domains (Revised Version)},
  type = {LTCS-Report},
  year = {1999},
}

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. Traditional database management systems are inadequate for the handling of such data types. They require new techniques for query formulation, retrieval, evaluation, and navigation. In this paper we develop a knowledge-based framework for modeling and retrieving image data by content. 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, i.e., a general schema about the classes of objects represented in the object layer. 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). These languages employ a variable free notation, and they are well suited for the design, verification and complexity analysis of algorithms. 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. The algorithm we propose is sound and complete and relatively efficient.

@techreport{ Hacid-Rigotti-LTCS-99,
  address = {Germany},
  author = {M.-S. {~Hacid} and C. {Rigotti}},
  doi = {https://doi.org/10.25368/2022.89},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html},
  number = {LTCS-99-02},
  title = {{R}epresenting and {R}easoning on {C}onceptual {Q}ueries {O}ver {I}mage {D}atabases},
  type = {LTCS-Report},
  year = {1999},
}

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 (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 (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.

@techreport{ Decleir-Hacid-Kouloumdjian-LTCS-99,
  address = {Germany},
  author = {C. {Decleir} and M.-S. {Hacid} and J. {Kouloumdjian}},
  doi = {https://doi.org/10.25368/2022.90},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html},
  number = {LTCS-99-03},
  title = {{A} {D}atabase {A}pproach for {M}odeling and {Q}uerying {V}ideo {D}ata},
  type = {LTCS-Report},
  year = {1999},
}

TBoxes are an important component 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 focused on reasoning without (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. An example for a logic of the former type is ALC while examples for logics of the latter kind include ALC(D) and ALCF. This demonstrates that it is necessary to take TBoxes into account for complexity analyses. Furthermore, we show that reasoning with the description logic ALCRP(D) is NExpTime-complete regardless of whether TBoxes are admitted or not.

@techreport{ Lutz-LTCS-99-04,
  address = {Germany},
  author = {C. {Lutz}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {This report is superceded by the LTCS-00-01 technical report and my LPAR'99 paper.},
  number = {LTCS-99-04},
  title = {On the Complexity of Terminological Reasoning},
  type = {LTCS-Report},
  year = {1999},
}

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², the two variable fragment of predicate logic with counting quantifiers. We prove that ALCQI has the same complexity as C² but does not reach its expressive power.

@techreport{ Tobies-LTCS-99-05,
  address = {Germany},
  author = {S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.91},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {An abriged version appeared at CSL-99.},
  number = {LTCS-99-05},
  title = {A NEXPTIME-complete Description Logic Strictly Contained in {$C^2$}},
  type = {LTCS-Report},
  year = {1999},
}

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. For 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.

@techreport{ BaaderMolitor-LTCS-99-06,
  address = {Germany},
  author = {F. {Baader} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.92},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html},
  number = {LTCS-99-06},
  title = {Rewriting Concepts using Terminologies},
  type = {LTCS-Report},
  year = {1999},
}

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 has concentrated on (sub-)languages of CLASSIC, which in particular do not allow for existential restrictions. In this work, we present sound and complete decision algorithms for the solvability of matching problems and for computing sets of matchers for matching problems in description logics with existential restrictions.

@techreport{ BaaderKuesters-LTCS-99-07-1999,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.93},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html},
  number = {LTCS-99-07},
  title = {Matching in Description Logics with Existential Restrictions},
  type = {LTCS-Report},
  year = {1999},
}

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 successively present algorithms that decides satisfiability of the DL extended with transitive and inverse roles, role hierarchies, and qualifying number restrictions. Early experiments indicate that this algorithm is well-suited for implementation.

@techreport{ HoSatTob-LTCS-99-08,
  author = {I. {Horrocks} and U. {Sattler} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.94},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {Revised version. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html},
  number = {LTCS-99-08},
  title = {A Description Logic with Transitive and Converse Roles, Role Hierarchies and Qualifying Number Restrictions},
  type = {LTCS-Report},
  year = {1999},
}

The description logic ALCQI extends the ``standard'' description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#Tobies-CADE-99>A PSPACE Algorithm for Graded Modal Logic</A> to deal with qualifying number restrictions and from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#HorrocksSattlerTobies-M4M-99>Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies</A> to deal with converse roles.

@techreport{ Tobies-LTCS-99-09,
  address = {Germany},
  author = {S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.95},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.},
  number = {LTCS-99-09},
  title = {A {PSpace}-algorithm for {ALCQI}-satisfiability},
  type = {LTCS-Report},
  year = {1999},
}

The description logic ALCQI extends the ``standard'' description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#Tobies-CADE-99>A PSPACE Algorithm for Graded Modal Logic</A> to deal with qualifying number restrictions and from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#HorrocksSattlerTobies-M4M-99>Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies</A> to deal with converse roles. Additionally, we extend the result to ALCQIR which extends ALCQI by role intersections.

@techreport{ Tobies-LTCS-99-11,
  address = {Germany},
  author = {S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.96},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.},
  number = {LTCS-99-11},
  title = {{PSpace} Reasoning for {DLs} with Qualifying Number Restrictions},
  type = {LTCS-Report},
  year = {1999},
}

Matching of concepts against patterns is a new inference task in Description Logics, which was originally motivated by applications of the Classic system. Consequently, the work on this problem was until now mostly concerned with sublanguages of the Classic language, which does not allow for existential restrictions. Motivated by an application in chemical process engineering, which requires a description language with existential restrictions, this paper investigates the matching problem in Description Logics with existential restrictions. It turns out that existential restrictions make matching more complex in two respects. First, whereas matching in sublanguages of Classic is polynomial, deciding the existence of matchers is an NP-complete problem in the presence of existential restrictions. Second, whereas in sublanguages of Classic solvable matching problems have a unique least matcher, this is not the case for languages with existential restrictions. Thus, it is not a priori clear which of the (possibly infinitely many) matchers should be returned by a matching algorithm. After determining the complexity of the decision problem, the present paper first investigates the question of what are "interesting" sets of matchers, and then describes algorithms for computing these sets for the languages EL (which allows for conjunction and existential restrictions) and ALE.

@techreport{ BaaderKuesters-LTCS-99-13-1999,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.98},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-99-13},
  title = {Matching Concept Descriptions with Existential Restrictions Revisited},
  type = {LTCS-Report},
  year = {1999},
}

When reasoning in description, modal or temporal logics it is often useful to consider axioms representing universal truths in the domain of discourse. Reasoning with respect to an arbitrary set of axioms is hard, even for relatively inexpressive logics, and it is essential to deal with such axioms in an efficient manner if implemented systems are to be effective in real applications. This is particularly relevant to Description Logics, where subsumption reasoning with respect to a terminology is a fundamental problem. Two optimisation techniques that have proved to be particularly effective in dealing with terminologies are lazy unfolding and absorption. In this paper we seek to improve our theoretical understanding of these important techniques. We define a formal framework that allows the techniques to be precisely described, establish conditions under which they can be safely applied, and prove that, provided these conditions are respected, subsumption testing algorithms will still function correctly. These results are used to show that the procedures used in the FaCT system are correct and, moreover, to show how efficiency can be significantly improved, while still retaining the guarantee of correctness, by relaxing the safety conditions for absorption.

@techreport{ HorrocksTobies-LTCS-99-14,
  author = {I. {Horrocks} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.99},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html},
  number = {LTCS-99-14},
  title = {Optimisation of Terminological Reasoning},
  type = {LTCS-Report},
  year = {1999},
}

Query containment under constraints is the problem of determining whether the result of one query is contained in the result of another query for every database satisfying a given set of constraints. This problem is of particular importance in information integration and warehousing where, in addition to the constraints derived from the source schemas and the global schema, inter-schema constraints can be used to specify relationships between objects in different schemas. A theoretical framework for tackling this problem using the DLR logic has been established, and in this paper we show how the framework can be extended to a practical decision procedure. The proposed technique is to extend DLR with an Abox (a set of assertions about named individuals and tuples), and to transform query subsumption problems into DLR Abox satisfiability problems. We then show how such problems can be decided, via a reification transformation, using a highly optimised reasoner for the SHI description logic.

@techreport{ HorrocksSattler+-LTCS-99-15,
  address = {Germany},
  author = {I. {Horrocks} and U. {Sattler} and S. {Tessaris} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.100},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-99-15},
  title = {Query Containment Using a {DLR} {ABox}},
  type = {LTCS-Report},
  year = {1999},
}

Formal Methods are becoming more an more important for the development of hardware and software systems. Verification tools support the employment of Formal Methods. This paper gives an overview of the design and implementation of the verification tool Truth. We define and explain requirements for verification tools. Furthermore, we discuss several semantic models, specification languages and logics and their visualisation from a tool builder's perspective and show how these requirements were adopted in Truth.

@techreport{ LeuckerTobies-AIB-98-5,
  author = {Martin {Leucker} and Stephan {Tobies}},
  institution = {RWTH Aachen},
  month = {May},
  number = {98-05},
  title = {Truth---A Platform for Verification of Distributed Systems},
  type = {Aachener Informatik Bericht},
  year = {1998},
}

This work introduces the concept language ALC(FM) which is an extension of ALC to many-valued logics. ALC(FM) allows to express vague concepts, e.g. `more or less enlarged' or `very small'. To realize this extension to many-valued logics, the classical notions of satisfiability and subsumption had to be modified appropriately. For example, ALC(FM)-concepts are no longer either satisfiable or unsatisfiable, but they are satisfiable to a certain degree. The main contribution of this paper is a sound and complete method for computing the degree of subsumption between two ALC(FM)-concepts.

@techreport{ TrespMolitor-LTCS-98-01,
  address = {Germany},
  author = {C.B. {Tresp} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.77},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html},
  number = {LTCS-98-01},
  title = {A Description Logic for Vague Knowledge},
  type = {LTCS-Report},
  year = {1998},
}

@techreport{ BaSat98,
  author = {F. {Baader} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.78},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-98-02},
  title = {Description Logics with Aggregates and Concrete Domains, Part II (extended)},
  type = {LTCS-Report},
  year = {1998},
}

@techreport{ Molitor-LTCS-98-03,
  author = {R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.79},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-98-03},
  title = {Structural {S}ubsumption for {$\cal A\!L\!N$}},
  type = {LTCS-Report},
  year = {1998},
}

This paper compares two approaches for deriving subsumption algorithms for the description logic ALN: structural subsumption and an automata-theoretic characterization of subsumption. It turns out that structural subsumption algorithms can be seen as special implementations of the automata-theoretic characterization.

@techreport{ BaaderKuestersMolitor-LTCS-98-04,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.80},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-98-04},
  title = {Structural Subsumption Considered from an Automata Theoretic Point of View},
  type = {LTCS-Report},
  year = {1998},
}

@techreport{ HoSat98,
  author = {I. {Horrocks} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.81},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-98-05},
  title = {A Description Logic with Transitive and Converse Roles and Role Hierarchies},
  type = {LTCS-Report},
  year = {1998},
}

Computing least common subsumers (lcs) and most specific concepts (msc) are inference tasks that can be used to support the ``bottom up'' construction of knowledge bases for KR systems based on description logic. For the description logic ALN, the msc need not always exist if one restricts the attention to acyclic concept descriptions. In this paper, we extend the notions lcs and msc to cyclic descriptions, and show how they can be computed. Our approach is based on the automata-theoretic characterizations of fixed-point semantics for cyclic terminologies developed in previous papers.

@techreport{ BaaderKuesters-LTCS-98-06-1998,
  author = {F. {Baader} and R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.82},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-98-06},
  title = {Computing the least common subsumer and the most specific concept in the presence of cyclic ALN-concept descriptions},
  type = {LTCS-Report},
  year = {1998},
}

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to substitute certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language. This is a revised version of LTCS-Report 97-02: it provides a stronger complexity result in Section 6.

@techreport{ Baader-Narendran-LTCS-98,
  author = {F. {Baader} and P. {Narendran}},
  doi = {https://doi.org/10.25368/2022.83},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-98-07},
  title = {Unification of Concept Terms in Description Logics: Revised Version},
  type = {LTCS-Report},
  year = {1998},
}

ALCI_R⁺—ALC 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 ALCI_R⁺-concepts. The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution. This algorithm will be the basis for an efficient implementation.

@techreport{ HoSatTob98,
  author = {I. {Horrocks} and U. {Sattler} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.84},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  number = {LTCS-98-08},
  title = {A PSpace-algorithm for deciding {$\mathcal{ALCNI}_{R^+}$}-satisfiability},
  type = {LTCS-Report},
  year = {1998},
}

Computing least common subsumers (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. More precisely, we show that, for the description logic ALE (which allows for conjunction, universal value restrictions, existential restrictions, negation of atomic concepts, as well as the top and the bottom concept), the lcs always exists and can effectively be computed. 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.

@techreport{ BaaderKuesters+-LTCS-98-09,
  address = {Germany},
  author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}},
  doi = {https://doi.org/10.25368/2022.85},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.},
  number = {LTCS-98-09},
  title = {Computing Least Common Subsumers in Description Logics with Existential Restrictions},
  type = {LTCS-Report},
  year = {1998},
}

Conceptual graphs (CGs) are an expressive and intuitive formalism, which plays an important role in the area of knowledge representation. Due to their expressiveness, most interesting problems for CGs are inherently undecidable. We identify the syntactically defined guarded fragment of CGs, for which both subsumption and validity is decidable in deterministic exponential time.

@techreport{ Baader-Molitor-Tobies-LTCS-98a,
  address = {Germany},
  author = {F. {Baader} and R. {Molitor} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.86},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html},
  number = {LTCS-98-10},
  title = {The Guarded Fragment of Conceptual Graphs},
  type = {LTCS-Report},
  year = {1998},
}

@techreport{ BaaderMolitorTobies-LTCS-98-11,
  address = {Germany},
  author = {F. {Baader} and R. {Molitor} and S. {Tobies}},
  doi = {https://doi.org/10.25368/2022.87},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-98-11},
  title = {On the Relation between Descripion Logics and Conceptual Graphs},
  type = {LTCS-Report},
  year = {1998},
}

The main contribution of this report is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, it is based on transformation rules, and also applies to theories sharing ``constructors.'' In addition, we show that—contrary to a common belief—the Nelson-Oppen combination method cannot be used to combine decision procedures for the word problem, even in the case of equational theories with disjoint signatures.

@techreport{ Baader-Tinelli-UIUCDCS-R-98-2073,
  author = {F. {Baader} and C. {Tinelli}},
  institution = {Department of Computer Science, University of Illinois at Urbana-Champaign},
  number = {UIUCDCS-R-98-2073},
  title = {Deciding the Word Problem in the Union of Equational Theories},
  type = {{UIUCDCS}-Report},
  year = {1998},
}

This work is a preliminary version of the chapter on unification theory in a volume on automated deduction produced by the participants of the nationwide German research programme on automated deduction (SSP ``Deduktion'').

@techreport{ BaaderSchulz-CIS-97-103,
  address = {Oettingenstra{\ss}e 67, D-80538 Munich, Germany},
  author = {Franz {Baader} and Klaus U. {Schulz}},
  doi = {https://doi.org/10.25368/2022.135},
  institution = {Center for Language and Information Processing (CIS)},
  month = {January},
  number = {CIS-Rep-97-103},
  title = {Unification Theory -- {A}n Introduction},
  type = {Research Report},
  year = {1997},
}

We show that extending description logics by simple aggregation functions as available in database systems may lead to undecidability of inference problems such as satisfiability and subsumption.

@techreport{ BaSat97,
  author = {F. {Baader} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.73},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  note = {An abridged version has appeared in the Proceedings of the International Workshop on Description Logics 97.},
  number = {LTCS-97-01},
  title = {Description Logics with Aggregates and Concrete Domains},
  type = {LTCS-Report},
  year = {1997},
}

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to substitute certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

@techreport{ Baader-Narendran-LTCS-97,
  author = {F. {Baader} and P. {Narendran}},
  doi = {https://doi.org/10.25368/2022.134},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-97-02},
  title = {Unification of Concept Terms in Description Logics},
  type = {LTCS-Report},
  year = {1997},
}

Unification modulo the theory of Boolean algebras has been investigated by several autors. Nevertheless, the exact complexity of the decision problem for unification with constants and general unification was not known. In this research note, we show that the decision problem is \(\Pi^p_2\)-complete for unification with constants and PSPACE-complete for general unification. In contrast, the decision problem for elementary unification (where the terms to be unified contain only symbols of the signature of Boolean algebras) is ``only'' NP-complete.

@techreport{ Baader-LTCS-97-03,
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.74},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-97-03},
  title = {On the Complexity of Boolean Unification},
  type = {LTCS-Report},
  year = {1997},
}

The representation of terminological knowledge may naturally lead to terminological cycles. In addition to descriptive semantics, the meaning of cyclic terminologies can also be captured by fixed-point semantics, namely, greatest and least fixed-point semantics. To gain a more profound understanding of these semantics and to obtain inference algorithms as well as complexity results for inconsistency, subsumption, and related inference tasks, this paper provides automata theoretic characterizations of these semantics. More precisely, the already existing results for FL₀ are extended to the language ALN, which additionally allows for primitive negation and number-restrictions. Unlike FL₀, the language ALN can express inconsistent concepts, which makes non-trivial extensions of the characterizations and algorithms necessary. Nevertheless, the complexity of reasoning does not increase when going from FL₀ to ALN. This distinguishes ALN from the very expressive languages with fixed-point operators proposed in the literature. It will be shown, however, that cyclic ALN-terminologies are expressive enough to capture schemata in certain semantic data models.

@techreport{ Kuesters-LTCS-97-04,
  author = {R. {K{\"u}sters}},
  doi = {https://doi.org/10.25368/2022.75},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-97-04},
  title = {Characterizing the semantics of terminological cycles in {$\mathcal{ALN}$} using finite automata},
  type = {LTCS-Report},
  year = {1997},
}

This paper proposes an extension of Datalog devoted to data manipulations in On-Line Analytical Processing (OLAP) systems. This language provides a declarative and concise way to specify the basic standard restructuring and summarizing operations on multidimensional cubes used in these systems. We define its model-theoretic semantics and an equivalent fixpoint semantics that leads to a naive evaluation procedure. We also illustrate its applicability to specify usefull more complex data manipulations arising in OLAP systems.

@techreport{ Hacid&al97a,
  author = {M. S. {Hacid} and P. {Marcel} and C. {Rigotti}},
  booktitle = {Proc. of the 5th Intl. Conf. on Deductive and Object-Oriented Databases (DOOD'97)},
  doi = {https://doi.org/10.25368/2022.76},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {A short version has appeared in the Proceedings of the 5th International Conference on Deductive and Object-Oriented Databases (DOOD'97), Montreux, Switzerland},
  number = {LTCS-97-05},
  publisher = {SPRINGER},
  series = {LNCS},
  title = {A rule based data manipulation language for {OLAP} systems},
  type = {LTCS-Report},
  year = {1997},
}

The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.

@techreport{ Baader-Tinelli-LTCS-96,
  author = {F. {Baader} and C. {Tinelli}},
  doi = {https://doi.org/10.25368/2022.69},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {An abridged version has appeared in Proc.\ CADE'97, Springer LNAI 1249.},
  number = {LTCS-96-01},
  title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {Nelson-Oppen} Combination Method},
  type = {LTCS-Report},
  year = {1996},
}

@techreport{ BaaderSattler-LTCS-96-02,
  author = {F. {Baader} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.70},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {An abridged version has appeared in the Proceedings of the Fifth International Conference on Knowledge Representation and Reasoning, 1996, Cambridge, Massachusetts.},
  number = {LTCS-96-02},
  title = {Number Restrictions on Complex Roles in Description Logics},
  year = {1996},
}

@techreport{ BaaderSattler-LTCS-96-03,
  author = {F. {Baader} and U. {Sattler}},
  doi = {https://doi.org/10.25368/2022.71},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {An abridged version has appeared in the Proceedings of the 12th European Conference on Artificial Intelligence, 1996, Budapest, Hungary.},
  number = {LTCS-96-03},
  title = {Description Logics with Symbolic Number Restrictions},
  year = {1996},
}

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 two optimisation methods, called the iterative and the deductive method. The iterative method reorders and localises the non-deterministic decisions. The deductive method uses specific algorithms for the components to reach certain decisions deterministically. 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.

@techreport{ KepserRichts-LTCS-96-04,
  address = {Germany},
  author = {S. {Kepser} and J. {Richts}},
  doi = {https://doi.org/10.25368/2022.72},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  number = {LTCS-96-04},
  title = {Optimisation Techniques for Combining Constraint Solvers},
  type = {LTCS-Report},
  year = {1996},
}

Reduction orderings that are compatible with an equational theory \(E\) and total on (the \(E\)-equivalence classes of) ground terms play an important role in automated deduction. We present a general approach for combining such orderings. To be more precise, we show how \(E_1\)-compatible reduction orderings total on \(\Sigma_1\)-ground terms and \(E_2\)-compatible reduction orderings total on \(\Sigma_2\)-ground terms can be used to construct an \((E_1\cup E_2)\)-compatible reduction ordering total on \((\Sigma_1\cup \Sigma_2)\)-ground terms, provided that the signatures are disjoint and some other (rather weak) restrictions are satisfied. This work was motivated by the observation that it is often easier to construct such orderings for ``small'' signatures and theories separately, rather than directly for their union.

@techreport{ Baader-LTCS-96,
  author = {F. {Baader}},
  doi = {https://doi.org/10.25368/2022.68},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-96-05},
  title = {Combination of Compatible Reduction Orderings that are Total on Ground Terms},
  type = {LTCS-Report},
  year = {1996},
}

An extension of the concept description language ALC used in KL-ONE-like terminological reasoning is presented. The extension includes multi-modal operators that can either stand for the usual role quantifications or for modalities such as belief, time etc. The modal operators can be used at all levels of the concept terms, and they can be used to modify both concepts and roles. This is an instance of a new kind of combination of modal logics where the modal operators of one logic may operate directly on the operators of the other logic. Different versions of this logic are investigated and various results about decidability and undecidability are presented. The main problem, however, decidability of the basic version of the logic, remains open.

@techreport{ MPI-I-95-2-005,
  address = {Saarbr{\"u}cken},
  author = {Franz {Baader} and Hans J{\"u}rgen {Ohlbach}},
  institution = {Max-Planck-Institut f{\"u}r Informatik},
  number = {MPI-I-95-2-005},
  pages = {32},
  title = {A Multi-Dimensional Terminological Knowledge Representation Language},
  type = {Technical Report},
  year = {1995},
}

When combining languages for symbolic constraints, one is typically faced with the problem of how to treat ``mixed'' constraints. The two main problems are (1) how to define a combined solution structure over which these constraints are to be solved, and (2) how to combine the constraint solving methods for pure constraints into one for mixed constraints. The paper introduces the notion of a ``free amalgamated product'' as a possible solution to the first problem. Subsequently, we define so-called simply-combinable structures (SC-structures). For SC-structures over disjoint signatures, a canonical amalgamation construction exists, which for the subclass of strong SC-structures yields the free amalgamated product. The combination technique of [Baader&Schulz92,Baader&Schulz95] can be used to combine constraint solvers for (strong) SC-structures over disjoint signatures into a solver for their (free) amalgamated product. In addition to term algebras modulo equational theories, the class of SC-structures contains many solution structures that have been used in constraint logic programming, such as the algebra of rational trees, feature structures, domains consisting of hereditarily finite (wellfounded or non-wellfounded) nested sets and lists.

@techreport{ CIS-94-82,
  author = {F. {Baader} and K. {Schulz}},
  institution = {Universit\"at M\"unchen},
  number = {94-82},
  title = {On the Combination of Symbolic Constraints, Solution Domains, and Constraint Solvers},
  type = {{CIS}-Report},
  year = {1994},
}

In a previous paper we have introduced a method that allows one to combine decision procedures for unifiability in disjoint equational theories. Lately, it has turned out that the prerequisite for this method to apply—namely that unification with so-called linear constant restrictions is decidable in the single theories—is equivalent to requiring decidability of the positive fragment of the first order theory of the equational theories. Thus, the combination method can also be seen as a tool for combining decision procedures for positive theories of free algebras defined by equational theories. The present paper uses this observation as the starting point of a more abstract, algebraic approach to formulating and solving the combination problem. Its contributions are twofold. As a new result, we describe an (optimized) extension of our combination method to the case of constraint solvers that also take relational constraints (such as ordering constraints) into account. The second contribution is a new proof method, which depends on abstract notions and results from universal algebra, as opposed to technical manipulations of terms (such as ordered rewriting, abstraction functions, etc.)

@techreport{ BaaderSchulz-CIS-94-75,
  address = {Wagm\"ullerstra{\ss}e 23, D-80538 Munich, Germany},
  author = {Franz {Baader} and Klaus U. {Schulz}},
  institution = {Center for Language and Information Processing (CIS)},
  month = {July},
  number = {CIS-Rep-94-75},
  title = {Combination of Constraint Solving Techniques: {A}n Algebraic Point of View},
  type = {Research Report},
  year = {1994},
}

Terminological knowledge representation formalisms can be used to represent objective, time-independent facts about an application domain. Notions like belief, intentions, time—which are essential for the representation of multi-agent environments—can only be expressed in a very limited way. For such notions, modal logics with possible worlds semantics provides a formally well-founded and well-investigated basis. <P> This paper presents a framework for integrating modal operators into terminological knowledge representation languages. These operators can be used both inside of concept expressions and in front of terminological and assertional axioms. The main restrictions are that all modal operators are interpreted in the basic logic <em>K</em>, and that we consider increasing domains instead of constant domains. We introduce syntax and semantics of the extended language, and show that satisfiability of finite sets of formulas is decidable.

@techreport{ DFKI-RR-94-33,
  author = {F. {Baader} and A. {Laux}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-94-33},
  title = {Terminological Logics with Modal Operators},
  type = {{DFKI} Research Report},
  year = {1994},
}

@techreport{ MPII-I-93-212,
  author = {F. {Baader} and H.-J. {Ohlbach}},
  institution = {Max-Planck-Institut f\"ur Informatik, Saarbr\"ucken},
  number = {MPI-I-93-212},
  title = {A Multi-Dimensional Terminological Knowledge Representation Language},
  type = {{MPII} Report},
  year = {1993},
}

@techreport{ DFKI-RR-93-03,
  author = {F. {Baader} and B. {Hollunder} and B. {Nebel} and H.J. {Profitlich} and E. {Franconi}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-93-03},
  title = {An Empirical Analysis of Optimization Techniques for Terminological Representation Systems, or: {M}aking {KRIS} get a move on},
  type = {{DFKI} Research Report},
  year = {1993},
}

@techreport{ DFKI-RR-93-05,
  author = {F. {Baader} and K. {Schulz}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-93-05},
  title = {Combination Techniques and Decision Problems for Disunification},
  type = {{DFKI} Research Report},
  year = {1993},
}

@techreport{ DFKI-RR-93-13,
  author = {F. {Baader} and K. {Schlechta}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-93-13},
  title = {A Semantics for Open Normal Defaults via a Modified Preferential Approach},
  type = {{DFKI} Research Report},
  year = {1993},
}

We consider the problem of integrating Reiter's default logic into terminological representation systems. It turns out that such an integration is less straightforward than we expected, considering the fact that the terminological language is a decidable sublanguage of first-order logic. Semantically, one has the unpleasant effect that the consequences of a terminological default theory may be rather unintuitive, and may even vary with the syntactic structure of equivalent concept expressions. This is due to the unsatisfactory treatment of open defaults via Skolemization in Reiter's semantics. On the algorithmic side, we show that this treatment may lead to an undecidable default consequence relation, even though our base language is decidable, and we have only finitely many (open) defaults. Because of these problems, we then consider a restricted semantics for open defaults in our terminological default theories: default rules are only applied to individuals that are explicitly present in the knowledge base. In this semantics it is possible to compute all extensions of a finite terminological default theory, which means that this type of default reasoning is decidable.

@techreport{ DFKI-RR-93-20,
  author = {F. {Baader} and B. {Hollunder}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-93-20},
  title = {Embedding Defaults into Terminological Representation Systems},
  type = {{DFKI} Research Report},
  year = {1993},
}

The concept description formalisms of existing terminological systems allow the user to express local cardinality restrictions on the fillers of a particular role. It is not possible, however, to introduce global restrictions on the number of instances of a given concept. The paper argues that such cardinality restrictions on concepts are of importance in applications such as configuration of technical systems, an application domain of terminological systems that is currently gaining in interest. It shows that including such restrictions into the description language leaves the important inference problems such as instance testing decidable. The algorithm combines and simplifies the ideas developed for the treatment of qualifying number restrictions and of general terminological axioms.

@techreport{ DFKI-RR-93-48,
  author = {F. {Baader} and M. {Buchheit} and B. {Hollunder}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  note = {A short version has appeared in Proceedings of the {KI}'94, Springer LNCS 861},
  number = {{RR}-93-48},
  title = {Cardinality Restrictions on Concepts},
  type = {{DFKI} Research Report},
  year = {1993},
}

@techreport{ CIS-92-58,
  author = {F. {Baader} and K. {Schulz}},
  institution = {Universit\"at M\"unchen},
  number = {92-58},
  title = {General {A}- and {AX}-Unification via Optimized Combination Procedures},
  type = {{CIS}-Report},
  year = {1992},
}

This work investigates general <em>AC</em>-unification, i.e. unification in the combination of free function symbols and free Abelian semigroups, whose function symbols fulfill associativity and commutativity.<p> The three necessary parts of general <em>AC</em>-unification are presented: a combination algorithm, a procedure for elementary <em>AC</em>-unification, and methods for solving systems of diophantine equations. Starting with A. Boudet's unification algorithm for the combination of regular and collapse-free theories, an efficient algorithm for general <em>AC</em>-unification is developed, setting out conditions that must be fulfilled by the solutions of elementary <em>AC</em>-unification. These conditions are used by the procedure for elementary <em>AC</em>-unification whereby further conditions are set out that must be fulfilled by the solutions of the diophantine equations. Then three methods (those of E. Contejean and H. Devie, E. Domenjoud, L. Pottier) for solving systems of diophantine equations are presented. The three methods are compared and evaluated, trying to use the conditions efficiently.<p> Finally some problems which arise from the reuse of <em>AC</em>-unifiers in unification, such as merging, are presented. It is shown that reusing <em>AC</em>-unifiers for partial problems is often worse than solving the entire problem from the beginning.

@techreport{ SWP-92-12,
  address = {Postfach 3049, D--67663 Kaiserslautern, Germany},
  author = {J{\"o}rn {Richts}},
  institution = {Fachbereich Informatik, Universit{\"a}t Kaiserslautern},
  number = {SWP--92--12},
  title = {Allgemeine {$AC$}-{U}nifikation durch {V}ariablenabstraktion mit {F}remdtermbedingungen},
  type = {Seki Working Paper},
  year = {1992},
}

@techreport{ DFKI-RR-92-33,
  author = {F. {Baader}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-92-33},
  title = {Unification Theory},
  type = {{DFKI} Research Report},
  year = {1992},
}

@techreport{ DFKI-RR-92-36,
  author = {F. {Baader} and P. {Hanschke}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-92-36},
  title = {Extensions of Concept Languages for a Mechanical Engineering Application},
  type = {{DFKI} Research Report},
  year = {1992},
}

@techreport{ DFKI-RR-92-58,
  author = {F. {Baader} and B. {Hollunder}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-92-58},
  title = {How to Prefer More Specific Defaults in Terminological Default Logic},
  type = {{DFKI} Research Report},
  year = {1992},
}

@techreport{ DFKI-RR-91-01,
  author = {F. {Baader} and H.-J. {B\"urckert} and B. {Nebel} and W. {Nutt} and G. {Smolka}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-91-01},
  title = {On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations},
  type = {{DFKI} Research Report},
  year = {1991},
}

@techreport{ DFKI-RR-91-03,
  author = {B. {Hollunder} and F. {Baader}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-91-03},
  title = {Qualifying Number Restrictions in Concept Languages},
  type = {{DFKI} Research Report},
  year = {1991},
}

A drawback which concept languages based on KL-ONE have is that all the terminological knowledge has to be defined on an abstract logical level. In many applications, one would like to be able to refer to concrete domains and predicates on these domains when defining concepts. Examples for such concrete domains are the integers, the real numbers, or also non-arithmetic domains, and predicates could be equality, inequality, or more complex predicates. In the present paper we shall propose a scheme for integrating such concrete domains into concept languages rather than describing a particular extension by some specific concrete domain. We shall define a terminological and an assertional language, and consider the important inference problems such as subsumption, instantiation, and consistency. The formal semantics as well as the reasoning algorithms are given on the scheme level. In contrast to existing KL-ONE based systems, these algorithms will be not only sound but also complete. They generate subtasks which have to be solved by a special purpose reasoner of the concrete domain.

@techreport{ DFKI-RR-91-10,
  author = {F. {Baader} and P. {Hanschke}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-91-10},
  title = {A Scheme for Integrating Concrete Domains into Concept Languages},
  type = {{DFKI} Research Report},
  year = {1991},
}

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms which compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms which just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures which works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories. As a consequence of this new method, we can for example show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol. Our method can also be used to combine algorithms which compute finite complete sets of unifiers. Manfred Schmidt-Schauss' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also get the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.

@techreport{ DFKI-RR-91-33,
  author = {F. {Baader} and K. {Schulz}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-91-33},
  title = {Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures},
  type = {{DFKI} Research Report},
  year = {1991},
}

@techreport{ DFKI-RR-90-01,
  author = {F. {Baader}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-90-01},
  title = {Terminological Cycles in {KL}-{ONE}-based Knowledge Representation Languages},
  type = {{DFKI} Research Report},
  year = {1990},
}

@techreport{ DFKI-RR-90-05,
  author = {F. {Baader}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-90-05},
  title = {A Formal Definition for Expressive Power of Knowledge Representation Languages},
  type = {{DFKI} Research Report},
  year = {1990},
}

@techreport{ DFKI-RR-90-10,
  author = {F. {Baader} and H.-J. {B\"urckert} and B. {Hollunder} and W. {Nutt} and J. {Siekmann}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-90-10},
  title = {Concept Logic},
  type = {{DFKI} Research Report},
  year = {1990},
}

@techreport{ DFKI-RR-90-13,
  author = {F. {Baader}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-90-13},
  title = {Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles},
  type = {{DFKI} Research Report},
  year = {1990},
}

@techreport{ DFKI-RR-90-16,
  author = {F. {Baader} and W. {Nutt}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{RR}-90-16},
  title = {Adding Homomorphisms to Commutative/Monoidal Theories, or: {H}ow Algebra Can Help in Equational Unification},
  type = {{DFKI} Research Report},
  year = {1990},
}

@techreport{ SEKI-SR-90-1,
  author = {F. {Baader}},
  institution = {Universit\"at Kaiserslautern},
  number = {{SR}-90-1},
  title = {Unification in Commutative Theories, {H}ilbert's Basis Theorem and {G}r\"obner Bases},
  type = {{SEKI} Report},
  year = {1990},
}

@techreport{ SEKI-SR-90-2,
  author = {F. {Baader}},
  institution = {Universit\"at Kaiserslautern},
  number = {{SR}-90-2},
  title = {Unification, Weak Unification, Upper Bound, Lower Bound and Generalization Problems},
  type = {{SEKI} Report},
  year = {1990},
}

@techreport{ DFKI-TM-90-03,
  author = {F. {Baader} and B. {Hollunder}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  number = {{TM}-90-03},
  title = {{KRIS}: Knowledge Representation and Inference System, System Description},
  type = {{DFKI} Technical Memo},
  year = {1990},
}

This paper contains a proposal for a terminological logic. The formalisms for representing knowledge as well as the needed inferences are described.

@techreport{ DFKI-TM-90-04,
  author = {F. {Baader} and H.-J. {B\"urckert} and J. {Heinsohn} and J. {M\"uller} and B. {Hollunder} and B. {Nebel} and W. {Nutt} and H.-J. {Profitlich}},
  institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern},
  note = {Updated version, taking into account the results of a discussion at the ``International Worksop on Terminological Logics,'' Dagstuhl, May 1991.},
  number = {{TM}-90-04},
  title = {Terminological Knowledge Representation: A Proposal for a Terminological Logic},
  type = {{DFKI} Technical Memo},
  year = {1990},
}

@techreport{ IMMD-89-22-8,
  author = {F. {Baader}},
  institution = {Institut f{\"u}r Mathematische Maschinen und Datenverarbeitung, Universit{\"a}t Erlangen},
  note = {Dissertation},
  number = {8},
  title = {Unifikation und {R}eduktionssysteme f{\"u}r {H}albgruppenvariet{\"a}ten},
  type = {Arbeitsbericht},
  volume = {22},
  year = {1989},
}

@techreport{ IMMD-85-18-8,
  author = {F. {Baader}},
  institution = {Institut f{\"u}r Mathematische Maschinen und Datenverarbeitung, Universit{\"a}t Erlangen},
  number = {8},
  title = {Die {S}-{V}ariet{\"a}t {DS} und einige {U}ntervariet{\"a}ten},
  type = {Arbeitsbericht},
  volume = {18},
  year = {1985},
}