Franz Baader

IJCAI Conference 2025 Conference Paper

Contractions Based on Optimal Repairs (Extended Abstract)

• Franz Baader
• Renata Wassermann

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. Similarly, optimal repairs, which are syntax-independent and maximize the retained consequences, may not exist. Our KR 2024 paper 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. It introduces this new approach in a very general setting, and proves a characterization theorem that relates the obtained contractions with well-known rationality postulates. Then, it describes a variety of 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.

FSCD Conference 2025 Conference Paper

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

• Franz Baader
• Oliver Fernández Gil

The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w. r. t. the restricted instantiation preorder, but not unitary w. r. t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w. r. t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w. r. t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.

KR Conference 2024 Conference Paper

Contractions Based on Optimal Repairs

• Franz Baader
• Renata Wassermann

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

AIJ Journal 2024 Journal Article

Extending the description logic EL with threshold concepts induced by concept measures

• Franz Baader
• Oliver Fernández Gil

In applications of AI systems where exact definitions of the important notions of the application domain are hard to come by, the use of traditional logic-based knowledge representation languages such as Description Logics may lead to very large and unintuitive definitions, and high complexity of reasoning. To overcome this problem, we define new concept constructors that allow us to define concepts in an approximate way. To be more precise, we present a family τ EL ( m ) of extensions of the lightweight Description Logic EL that use threshold constructors for this purpose. To define the semantics of these constructors we employ graded membership functions m, which for each individual in an interpretation and concept yield a number in the interval [ 0, 1 ] expressing the degree to which the individual belongs to the concept in the interpretation. Threshold concepts C ⋈ t for ⋈ ∈ { <, ≤, >, ≥ } then collect all the individuals that belong to C with degree ⋈t. The logic τ EL ( m ) extends EL with threshold concepts whose semantics is defined relative to a function m. To construct appropriate graded membership functions, we show how concept measures ∼ (which are graded generalizations of subsumption or equivalence between concepts) can be used to define graded membership functions m ∼. Then we introduce a large class of concept measures, called simi-d, for which the logics τ EL ( m ∼ ) have good algorithmic properties. Basically, we show that reasoning in τ EL ( m ∼ ) is NP/coNP-complete without TBox, PSpace-complete w. r. t. acyclic TBoxes, and ExpTime-complete w. r. t. general TBoxes. The exception is the instance problem, which is already PSpace-complete without TBox w. r. t. combined complexity. While the upper bounds hold for all elements of simi-d, we could prove some of the hardness results only for a subclass of simi-d. This article considerably improves on and generalizes results we have shown in three previous conference papers and it provides detailed proofs of all our results.

FSCD Conference 2024 Conference Paper

On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems

• Franz Baader
• Jürgen Giesl

Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system R, a term s, and a natural number n, decide whether there is a term t of size ≤ n reachable from s using the rules of R. We investigate the complexity of this problem depending on how termination of R can be established. We show that the problem is NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases.

JELIA Conference 2023 Invited Paper

Optimal Repairs in the Description Logic E ℒ Revisited

• Franz Baader
• Patrick Koopmann
• Francesco Kriegel

Abstract 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{E}\mathcal{L}\) 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.

KR Conference 2022 Conference Paper

Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs

• Franz Baader
• Francesco Kriegel

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 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 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 EL, which yields a fragment of the well-known DL Horn-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-ALCOI TBoxes with regular role inclusions.

JELIA Conference 2021 Conference Paper

An Algebraic View on p-Admissible Concrete Domains for Lightweight Description Logics

• Franz Baader
• Jakub Rydval

Abstract 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 \(\mathcal {ALC}\) decidable. When integrating concrete domains into lightweight DLs of the \(\mathcal {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 \(\mathcal {ALC}\) yields decidable DLs.

LPAR Conference 2020 Conference Paper

Finding Small Proofs for Description Logic Entailments: Theory and Practice

• Christian Alrabbaa
• Franz Baader
• Stefan Borgwardt
• Patrick Koopmann
• Alisa Kovtunova

Logic-based approaches to AI have the advantage that their behaviour can in principle be explained by providing their users with proofs for the derived consequences. However, if such proofs get very large, then it may be hard to understand a consequence even if the individual derivation steps are easy to comprehend. This motivates our interest in finding small proofs for Description Logic (DL) entailments. Instead of concentrating on a specific DL and proof calculus for this DL, we introduce a general framework in which proofs are represented as labeled, directed hypergraphs, where each hyperedge corresponds to a single sound derivation step. On the theoretical side, we investigate the complexity of deciding whether a certain consequence has a proof of size at most n along the following orthogonal dimensions: (i) the underlying proof system is polynomial or exponential; (ii) proofs may or may not reuse already derived consequences; and (iii) the number n is represented in unary or binary. We have determined the exact worst-case complexity of this decision problem for all but one of the possible combinations of these options. On the practical side, we have developed and implemented an approach for generating proofs for expressive DLs based on a non-standard reasoning task called forgetting. We have evaluated this approach on a set of realistic ontologies and compared the obtained proofs with proofs generated by the DL reasoner ELK, finding that forgetting-based proofs are often better w. r. t. different measures of proof complexity.

ECAI Conference 2020 Conference Paper

Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints

• Franz Baader
• Bartosz Bednarczyk
• Sebastian Rudolph

We introduce and investigate the expressive description logic (DL) ALCSCC ++, in which the global and local cardinality constraints introduced in previous papers can be mixed. We prove that the added expressivity does not increase the complexity of satisfiability checking and other standard inference problems. However, reasoning in ALCSCC ++ becomes undecidable if inverse roles are added or conjunctive query entailment is considered. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted. In this setting, query entailment can be shown to be EXPTIME-complete and hence not harder than reasoning in ALC.

JELIA Conference 2019 Conference Paper

Counting Strategies for the Probabilistic Description Logic 𝓐ℒ𝒞 ME Under the Principle of Maximum Entropy

• Marco Wilhelm
• Gabriele Kern-Isberner
• Andreas Ecke
• Franz Baader

Abstract We present \(\mathcal {ALC}^\mathsf {ME}\), a probabilistic variant of the Description Logic \(\mathcal {ALC}\) that allows for representing and processing conditional statements of the form “if E holds, then F follows with probability p ” under the principle of maximum entropy. Probabilities are understood as degrees of belief and formally interpreted by the aggregating semantics. We prove that both checking consistency and drawing inferences based on approximations of the maximum entropy distribution is possible in \(\mathcal {ALC}^\mathsf {ME}\) in time polynomial in the domain size. A major problem for probabilistic reasoning from such conditional knowledge bases is to count models and individuals. To achieve our complexity results, we develop sophisticated counting strategies on interpretations aggregated with respect to the so-called conditional impacts of types, which refine their conditional structure.

JELIA Conference 2019 Conference Paper

Privacy-Preserving Ontology Publishing for EL Instance Stores

• Franz Baader
• Francesco Kriegel
• Adrian Nuradiansyah

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

KR Conference 2018 Conference Paper

Making Repairs in Description Logics More Gentle

• Franz Baader
• Francesco Kriegel
• Adrian Nuradiansyah
• Rafael Peñaloza

The classical approach for repairing a Description Logic ontology O in the sense of removing an unwanted consequence α is to delete a minimal number of axioms from O such that the resulting ontology O0 does not have the consequence α. 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 notion of repair in which axioms are not 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 EL.

LPAR Conference 2018 Conference Paper

Matching in the Description Logic FL0 with respect to General TBoxes

• Franz Baader
• Oliver Fernández Gil
• Pavlos Marantidis

Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics two decades ago, motivated by applications in the Classic system. Shortly afterwards, a polynomial-time matching algorithm was developed for the DL FL0. However, this algorithm cannot deal with general TBoxes (i. e. , finite sets of general concept inclusions). Here we show that matching in FL0 w. r. t. general TBoxes is in ExpTime, which is the best possible complexity for this problem since already subsumption w. r. t. general TBoxes is ExpTime-hard in FL0. We also show that, w. r. t. a restricted form of TBoxes, the complexity of matching in FL0 can be lowered to PSpace.

IJCAI Conference 2017 Conference Paper

Query Rewriting for DL-Lite with n-ary Concrete Domains

• Franz Baader
• Stefan Borgwardt
• Marcel Lippmann

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.

JELIA Conference 2016 Conference Paper

Approximate Unification in the Description Logic FL _0

• Franz Baader
• Pavlos Marantidis
• Alexander Okhotin

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

ECAI Conference 2016 Conference Paper

Extending the Description Logic with Acyclic TBoxes

• Franz Baader
• Oliver Fernández Gil

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~tfor ~&isin; {<, &le; ,>, &ge; } then collect all the individuals that belong to C with degree ~t. We have then investigated the complexity of reasoning in the Description Logic, which is obtained fromby 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 toincreases the complexity of reasoning by at least on level of the polynomial hierarchy.

JAIR Journal 2016 Journal Article

Query and Predicate Emptiness in Ontology-Based Data Access

• Franz Baader
• Meghyn Bienvenu
• Carsten Lutz
• Frank Wolter

In ontology-based data access (OBDA), database querying is enriched with an ontology that provides domain knowledge and additional vocabulary for query formulation. We identify query emptiness and predicate emptiness as two central reasoning services in this context. Query emptiness asks whether a given query has an empty answer over all databases formulated in a given vocabulary. Predicate emptiness is defined analogously, but quantifies universally over all queries that contain a given predicate. In this paper, we determine the computational complexity of query emptiness and predicate emptiness in the EL, DL-Lite, and ALC-families of description logics, investigate the connection to ontology modules, and perform a practical case study to evaluate the new reasoning services.

KR Conference 2012 Short Paper

Extending Unification in EL towards General TBoxes

• Franz Baader
• Stefan Borgwardt
• Barbara Morawska

can obviously be made equivalent by treating the concept names Head injury and Severe injury as variables, and substituting the first one by Injury u ∃finding site. Head and the second one by Injury u ∃severity. Severe. In this case, we say that the descriptions are unifiable, and call the substitution that makes them equivalent a unifier. Intuitively, such a unifier proposes definitions for the concept names that are used as variables: in our example, we know that, if we define Head injury as Injury u ∃finding site. Head and Severe injury as Injury u ∃severity. Severe, then the two concept descriptions (1) and (2) are equivalent w. r. t. these definitions. Here equivalence holds without additional GCIs. To motivate our interest in unification w. r. t. GCIs, assume that the second developer uses the description 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. 1 ∃status. Emergency u ∃finding. (Severe injury u ∃finding site. Head)

LPAR Conference 2012 Conference Paper

Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints

• Franz Baader
• Alexander Okhotin

Abstract 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 \(\mathcal{FL}_0\) and for monadic set constraints with negation. We believe that looping automata with colors may also turn out to be useful in other applications.

KR Conference 2010 Conference Paper

Query and Predicate Emptiness in Description Logics

• Franz Baader
• Meghyn Bienvenu
• Carsten Lutz
• Frank Wolter

Ontologies can be used to provide an enriched vocabulary for the formulation of queries over instance data. We identify query emptiness and predicate emptiness as two central reasoning services in this context. Query emptiness asks whether a given query has an empty answer over all data sets formulated in a given signature. Predicate emptiness is defined analogously, but quantifies universally over all queries that contain a given predicate. In this paper, we determine the computational complexity of query emptiness and predicate emptiness in the EL, DL-Lite, and ALC-families of description logics, investigate the connection to ontology modules, and perform a practical case study to evaluate the new reasoning services.

ECAI Conference 2010 Conference Paper

Verifying Properties of Infinite Sequences of Description Logic Actions

• Franz Baader
• Hongkai Liu
• Anees ul Mehdi

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.

I&C Journal 2008 Journal Article

Automata can show PSpace results for description logics

• Franz Baader
• Jan Hladik
• Rafael Peñaloza

In the area of Description Logic (DL), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal algorithms in the case of PSpace-complete logics, it is often very hard to design optimal tableau-based algorithms for ExpTime-complete DLs. In contrast, the automata-based approach is usually well-suited to prove ExpTime upper-bounds, but its direct application will usually also yield an ExpTime-algorithm for a PSpace-complete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate conditions under which an on-the-fly construction of such an exponentially large automaton can be used to obtain a PSpace-algorithm. We illustrate the usefulness of this approach by proving a new PSpace upper-bound for satisfiability of concepts with respect to acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles.

KR Conference 2008 Conference Paper

LTL over Description Logic Axioms

• Franz Baader
• Silvio Ghilardi
• Carsten Lutz

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.

IJCAI Conference 2007 Conference Paper

• Franz Baader
• Bernhard Ganter
• Ulrike Sattler
• Baris Sertkaya

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

I&C Journal 2006 Journal Article

A new combination procedure for the word problem that generalizes fusion decidability results in modal logics

• Franz Baader
• Silvio Ghilardi
• Cesare Tinelli

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—which are not disjoint for sharing 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 types of 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.

AAAI Conference 2005 Conference Paper

Integrating Description Logics and Action Formalisms: First Results

• Franz Baader
• Maja Milicic

We propose an action formalism that is based on description logics (DLs) and may be viewed as an instance of the Situation Calculus (SitCalc). In particular, description logic concepts can be used for describing the state of the world, and the pre- and post-conditions of actions. The main advantage of such a combination is that, on the one hand, the expressive power for describing world states and conditions is higher than in other decidable fragments of the SitCalc, which are usually propositional. On the other hand, in contrast to the full SitCalc, effective reasoning is still possible. In this paper, we perform a detailed investigation of how the choice of the DL influences the complexity of the standard reasoning tasks executability and projection in the corresponding action formalism. We also discuss semantic and computational problems in natural extensions of our framework.

IJCAI Conference 2005 Conference Paper

Pushing the EL Envelope

• Franz Baader
• Sebastian Brandt
• Carsten

Recently, it has been shown that the small description logic (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 with general concept inclusion axioms (GCIs). On the one hand, we 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 show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even EXPTIMEcomplete. In addition, we show that subsumption in FL0 with GCIs is EXPTIME-complete.

JELIA Conference 2004 Conference Paper

Computing the Least Common Subsumer w. r. t. a Background Terminology

• Franz Baader
• Baris Sertkaya
• Anni-Yasmin Turhan

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

JELIA Conference 2004 Invited Paper

Engineering of Logics for the Content-Based Representation of Information

• Franz Baader

Abstract The content-based representation of information, which tries to represent the meaning of the information in a machine-understandable way, requires representation formalisms with a well-defined formal semantics. This semantics can elegantly be provided by the use of a logic-based formalism. However, in this setting there is a fundamental tradeoff between the expressivity of the representation formalism and the efficiency of reasoning with this formalism. This motivates the “engineering of logics”, i. e. , the design of logical formalisms that are tailored to specific representation tasks. The talk will illustrate this approach with the example of so-called Description Logics and their application for databases and as ontology languages for the semantic web.

LPAR Conference 2003 Conference Paper

From Tableaux to Automata for Description Logics

• Franz Baader
• Jan Hladik
• Carsten Lutz
• Frank Wolter

This paper investigates the relationship between automata- and tableau-based inference procedures for Description Logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then show, on this abstract level, how tableau-based algorithms can be converted into automata-based algorithms. In particular, this allows us to characterize a large class of tableau-based algorithms that imply an ExpTime upper-bound for reasoning in the description logics for which such an algorithm exists.

IJCAI Conference 2003 Conference Paper

Least Common Subsumers and Most Specific Concepts in a Description Logic with Existential Restrictions and Terminological Cycles

• Franz Baader

Computing least common subsumers (Ics) and most specific concepts (msc) are inference tasks that can support the bottom-up construction of knowledge bases in description logics. In description logics with existential restrictions, the most specific concept need not exist if one restricts the attention to concept descriptions or acyclic TBoxes. In this paper, we extend the notions les and msc to cyclic TBoxes. For the description logic EC (which allows for conjunctions, existential restrictions, and the top-concept), we show that the les and msc always exist and can be computed in polynomial time if we interpret cyclic definitions with greatest fixpoint semantics.

IJCAI Conference 2003 Conference Paper

Terminological Cycles in a Description Logic with Existential Restrictions

• Franz Baader

Cyclic definitions in description logics have until now been investigated only for description logics allowing for value restrictions. Even for the most basic language which allows for conjunction and value restrictions only, deciding subsumption in the presence of terminological cycles is a PSPACE-complete problem. This paper investigates subsumption in the presence of terminological cycles for the language. , which allows for conjunction, existential restrictions, and the topconcept. In contrast to the results for, subsumption in remains polynomial, independent of whether we use least fixpoint semantics, greatest fixpoint semantics, or descriptive semantics.

I&C Journal 2002 Journal Article

Deciding the Word Problem in the Union of Equational Theories

• Franz Baader
• Cesare Tinelli

The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, this method is based on transformation rules. Furthermore, it is not limited to theories with disjoint signatures but it also applies to theories sharing constructors.

LPAR Conference 2001 Conference Paper

Unification in a Description Logic with Transitive Closure of Roles

• Franz Baader
• Ralf Küsters

Abstract 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 \( \mathcal{F}\mathcal{L}_0 \), 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 \( \mathcal{F}\mathcal{L}_0 \) ) 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.

IJCAI Conference 1999 Conference Paper

Computing Least Common Subsumers in Description Logics with Existential Restrictions

• Franz Baader
• Ralf Kuster
• Ralf Molitor

Computing the least common subsunier (les) is an inference task that can be used to support, the "bottom-up" construction of knowledge bases for KR systems based on description logics. Previous work on how to compute the lcs has concentrated on description logics that allow for universal value restrictions, but not for existential restrictions. The main new contribution of this paper is the treatment of description logics with existential restrictions. Our approach for computing the lcs is based on an appropriate representation of concept descriptions by certain trees, and a characterization of subsumption by homomorphisins between these trees. The lcs operation then corresponds to the product operation on trees.

TCS Journal 1998 Journal Article

Combination of constraint solvers for free and quasi-free structures

• Franz Baader
• Klaus U. Schulz

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. We define so-called quasi-free structures (called “strong simply-combinable structures” in a previous publication) as a generalization of free structures. For quasi-free structures over disjoint signatures, we describe a canonical amalgamation construction that yields the free amalgamated product. The combination techniques known from unification theory can be used to combine constraint solvers for quasi-free structures over disjoint signatures into a solver for their free amalgamated product. In addition to term algebras modulo equational theories (i. e. , free algebras), the class of quasi-free structures contains many solution structures that are of interest in constraint logic programming, such as the algebra of rational trees, feature structures, and domains consisting of hereditarily finite (well-founded or non-well-founded) nested sets and lists.

ECAI Conference 1998 Conference Paper

Description Logics with Concrete Domains and Aggregation

• Franz Baader
• Ulrike Sattler

ECAI Conference 1998 Conference Paper

Unification of Concept Terms in Description Logics

• Franz Baader
• Paliath Narendran

AIJ Journal 1996 Journal Article

Cardinality restrictions on concepts

• Franz Baader
• Martin Buchheit
• Bernhard Hollander

The concept description formalisms of existing description logics 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. This article argues that such cardinality restrictions on concepts are of importance in applications such as configuration of technical systems, an application domain of description logics systems that is currently gaining in interest. It shows that including such restrictions in 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 qualified number restrictions and of general terminological axioms.

ECAI Conference 1996 Conference Paper

Description Logics with Symbolic Number Restrictions

• Franz Baader
• Ulrike Sattler

TCS Journal 1995 Journal Article

Combination techniques and decision problems for disunification

• Franz Baader
• Klaus U. Schulz

Previous work on combination techniques considered the question of how to combine unification algorithms for disjoint equational theories E 1, …, En in order to obtain a unification algorithm for the union E 1 ∪ ⋯ ∪ En of the theories. Here we want to show that variants of this method may be used to decide solvability and ground solvability of disunification problems in E 1 ∪ ⋯ ∪ En. Our first result says that solvability of disunification problems in the free algebra of the combined theory E 1 ∪ ⋯ ∪ En is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories Ei (i = 1, …, n) is decidable. In order to decide ground solvability (i. e. , solvability in the initial algebra) of disunification problems in E 1 ∪ ⋯ ∪ En we have to consider a new kind of subproblem for the particular theories Ei, namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not Ei -equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, (1) if one theory Ei is the free theory with at least one function symbol and one constant, or (2) if the initial algebras of all theories Ei are infinite. Our results can be used to show that the existential fragment of the theory of the (ground) term algebra modulo associativity of a finite number of function symbols is decidable; the same result follows for function symbols which are associative and commutative, or associative, commutative and idempotent.

KER Journal 1995 Journal Article

Reasoning about structured objects: Knowledge representation meets databases

• Franz Baader
• Martin Buchheit
• Manfred A. Jeusfeld
• Werner Nutt

Structured objects are items with defined properties that are to be represented in a computer system. Research in Knowledge Representation (KR) and in Database Design (DB) has produced languages for describing structured objects. Although different in the particular means for defining properties, both areas share the goal of representing a part of the world in a structured way. Moreover, the rise of object-centred formalisms in the last decade has significantly influenced the convergence of languages.

IJCAI Conference 1995 Conference Paper

Terminological Logics with Modal Operators

• Franz Baader
• Armin Laux

Terminological knowledge representation formalisms can be used to represent objective, time-independent facts about an application domain. Notions like belief, intentions, and 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 wellinvestigated basis. 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. We introduce syntax and semantics of the extended language, and show that satisfiability of finite sets of formulas is decidable, provided that all modal operators are interpreted in the basic logic K, and that the increasing domain assumption is used.

IJCAI Conference 1993 Conference Paper

How to Prefer More Specific Defaults in Terminological Default Logic

• Franz Baader
• Bernhard Hollunder

IJCAI Conference 1991 Conference Paper

A Scheme for Integrating Concrete Domains into Concept Languages

• Franz Baader
• Philipp

A drawback which concept languages based on K L - O N E 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 can be given on the scheme level. In contrast to existing KL-ONE based systems, these algorithms are not only sound but also complete. They generate subtasks which have to be solved by a special purpose reasoner of the concrete domain.

ECAI Conference 1990 Conference Paper

A Formal Definition for the Expressive Power of Knowledge Representation Languages

• Franz Baader

AAAI Conference 1990 Conference Paper

Terminological Cycles in KL-ONE-based Knowledge Representation Languages

• Franz Baader

TCS Journal 1988 Journal Article

Unification in commutative idempotent monoids

• Franz Baader
• Wolfram Büttner

Embedding sets as a datastructure into resolution-based deduction requires a unification algorithm respecting associativity, commutativity and idempotence of the constructor function union. We shall present such an algorithm and prove its correctness and termination. Although this algorithm is very simple, the enormous proliferation of unifiers restricts its value to theoretical considerations. For practical purposes, the more special, unitary theory of boolean expressions seem to be better suited.