Showing 1–50 of 50 results for author: Wolter, F

Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)

Authors: Alessandro Artale, Roman Kontchakov, Andrea Mazzullo, Frank Wolter

Abstract: Definite descriptions, such as 'the General Chair of KR 2024', are a semantically transparent device for object identification in knowledge representation. In first-order modal logic, definite descriptions have been widely investigated for their non-rigidity, which allows them to designate different objects (or none at all) at different states. We propose expressive modal description logics with n… ▽ More Definite descriptions, such as 'the General Chair of KR 2024', are a semantically transparent device for object identification in knowledge representation. In first-order modal logic, definite descriptions have been widely investigated for their non-rigidity, which allows them to designate different objects (or none at all) at different states. We propose expressive modal description logics with non-rigid definite descriptions and names, and investigate decidability and complexity of the satisfaction problem. We first systematically link satisfiability for the one-variable fragment of first-order modal logic with counting to our modal description logics. Then, we prove a promising NEXPTIME-completeness result for concept satisfiability for the fundamental epistemic multi-agent logic $\mathbf{S5}^{n}$ and its neighbours, and show that some expressive logics that are undecidable with constant domain become decidable (but Ackermann-hard) with expanding domains. Finally, we conduct a fine-grained analysis of decidability of temporal logics. △ Less

Submitted 10 September, 2024; v1 submitted 13 May, 2024; originally announced May 2024.

Extremal Separation Problems for Temporal Instance Queries

Authors: Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: The separation problem for a class Q of database queries is to find a query in Q that distinguishes between a given set of `positive' and `negative' data examples. Separation provides explanations of examples and underpins the query-by-example paradigm to support database users in constructing and refining queries. As the space of all separating queries can be large, it is helpful to succinctly re… ▽ More The separation problem for a class Q of database queries is to find a query in Q that distinguishes between a given set of `positive' and `negative' data examples. Separation provides explanations of examples and underpins the query-by-example paradigm to support database users in constructing and refining queries. As the space of all separating queries can be large, it is helpful to succinctly represent this space by means of its most specific (logically strongest) and general (weakest) members. We investigate this extremal separation problem for classes of instance queries formulated in linear temporal logic LTL with the operators conjunction, next, and eventually. Our results range from tight complexity bounds for verifying and counting extremal separators to algorithms computing them. △ Less

Submitted 7 June, 2024; v1 submitted 6 May, 2024; originally announced May 2024.

Comments: Accepted for IJCAI 2024

ACM Class: I.2.4; F.2.2

Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations

Authors: Frank Wolter, Michael Zakharyaschev

Abstract: The interpolant existence problem (IEP) for a logic L is to decide, given formulas P and Q, whether there exists a formula I, built from the shared symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the Craig interpolation property (CIP), then the IEP reduces to validity in L. Recently, the IEP has been studied for logics without the CIP. The results obtained so far indica… ▽ More The interpolant existence problem (IEP) for a logic L is to decide, given formulas P and Q, whether there exists a formula I, built from the shared symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the Craig interpolation property (CIP), then the IEP reduces to validity in L. Recently, the IEP has been studied for logics without the CIP. The results obtained so far indicate that even though the IEP can be computationally harder than validity, it is decidable when L is decidable. Here, we give the first examples of decidable fragments of first-order logic for which the IEP is undecidable. Namely, we show that the IEP is undecidable for the two-variable fragment with two equivalence relations and for the two-variable guarded fragment with individual constants and two equivalence relations. We also determine the corresponding decidable Boolean description logics for which the IEP is undecidable. △ Less

Submitted 3 April, 2024; originally announced April 2024.

MSC Class: 03B45 (Primary) 03C40 (Secondary)

The interpolant existence problem for weak K4 and difference logic

Authors: Agi Kurucz, Frank Wolter, Michael Zakharyaschev

Abstract: As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the nonexistence of an interpolant can always be witnessed by a pair of bisimilar models of polynomial size for DL and of triple-exponential size for weak K4, and so the int… ▽ More As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the nonexistence of an interpolant can always be witnessed by a pair of bisimilar models of polynomial size for DL and of triple-exponential size for weak K4, and so the interpolant existence problems for these logics are decidable in coNP and coN3ExpTime, respectively. We also establish coNExpTime-hardness of this problem for weak K4, which is higher than the PSpace-completeness of its decision problem. △ Less

Submitted 17 June, 2024; v1 submitted 17 March, 2024; originally announced March 2024.

A non-uniform view of Craig interpolation in modal logics with linear frames

Authors: Agi Kurucz, Frank Wolter, Michael Zakharyaschev

Abstract: Normal modal logics extending the logic K4.3 of linear transitive frames are known to lack the Craig interpolation property, except some logics of bounded depth such as S5. We turn this `negative' fact into a research question and pursue a non-uniform approach to Craig interpolation by investigating the following interpolant existence problem: decide whether there exists a Craig interpolant betwee… ▽ More Normal modal logics extending the logic K4.3 of linear transitive frames are known to lack the Craig interpolation property, except some logics of bounded depth such as S5. We turn this `negative' fact into a research question and pursue a non-uniform approach to Craig interpolation by investigating the following interpolant existence problem: decide whether there exists a Craig interpolant between two given formulas in any fixed logic above K4.3. Using a bisimulation-based characterisation of interpolant existence for descriptive frames, we show that this problem is decidable and coNP-complete for all finitely axiomatisable normal modal logics containing K4.3. It is thus not harder than entailment in these logics, which is in sharp contrast to other recent non-uniform interpolation results. We also extend our approach to Priorean temporal logics (with both past and future modalities) over the standard time flows-the integers, rationals, reals, and finite strict linear orders-none of which is blessed with the Craig interpolation property. △ Less

Submitted 10 December, 2023; originally announced December 2023.

MSC Class: 03B45 (Primary) 03C40 (Secondary)

Approximating Voltage Stability Boundary Under High Variability of Renewables Using Differential Geometry

Authors: Dan Wu, Franz-Erich Wolter, Sijia Geng

Abstract: This paper proposes a novel method rooted in differential geometry to approximate the voltage stability boundary of power systems under high variability of renewable generation. We extract intrinsic geometric information of the power flow solution manifold at a given operating point. Specifically, coefficients of the Levi-Civita connection are constructed to approximate the geodesics of the manifo… ▽ More This paper proposes a novel method rooted in differential geometry to approximate the voltage stability boundary of power systems under high variability of renewable generation. We extract intrinsic geometric information of the power flow solution manifold at a given operating point. Specifically, coefficients of the Levi-Civita connection are constructed to approximate the geodesics of the manifold starting at an operating point along any interested directions that represent possible fluctuations in generation and load. Then, based on the geodesic approximation, we further predict the voltage collapse point by solving a few univariate quadratic equations. Conventional methods mostly rely on either expensive numerical continuation at specified directions or numerical optimization. Instead, the proposed approach constructs the Christoffel symbols of the second kind from the Riemannian metric tensors to characterize the complete local geometry which is then extended to the proximity of the stability boundary with efficient computations. As a result, this approach is suitable to handle high-dimensional variability in operating points due to the large-scale integration of renewable resources. Using various case studies, we demonstrate the advantages of the proposed method and provide additional insights and discussions on voltage stability in renewable-rich power systems. △ Less

Submitted 3 October, 2023; originally announced October 2023.

Comments: 8 pages, 9 figures

Current and Future Challenges in Knowledge Representation and Reasoning

Authors: James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, Frank Wolter

Abstract: Knowledge Representation and Reasoning is a central, longstanding, and active area of Artificial Intelligence. Over the years it has evolved significantly; more recently it has been challenged and complemented by research in areas such as machine learning and reasoning under uncertainty. In July 2022 a Dagstuhl Perspectives workshop was held on Knowledge Representation and Reasoning. The goal of t… ▽ More Knowledge Representation and Reasoning is a central, longstanding, and active area of Artificial Intelligence. Over the years it has evolved significantly; more recently it has been challenged and complemented by research in areas such as machine learning and reasoning under uncertainty. In July 2022 a Dagstuhl Perspectives workshop was held on Knowledge Representation and Reasoning. The goal of the workshop was to describe the state of the art in the field, including its relation with other areas, its shortcomings and strengths, together with recommendations for future progress. We developed this manifesto based on the presentations, panels, working groups, and discussions that took place at the Dagstuhl Workshop. It is a declaration of our views on Knowledge Representation: its origins, goals, milestones, and current foci; its relation to other disciplines, especially to Artificial Intelligence; and on its challenges, along with key priorities for the next decade. △ Less

Submitted 8 August, 2023; originally announced August 2023.

Unique Characterisability and Learnability of Temporal Queries Mediated by an Ontology

Authors: Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: Algorithms for learning database queries from examples and unique characterisations of queries by examples are prominent starting points for developing automated support for query construction and explanation. We investigate how far recent results and techniques on learning and unique characterisations of atemporal queries mediated by an ontology can be extended to temporal data and queries. Based… ▽ More Algorithms for learning database queries from examples and unique characterisations of queries by examples are prominent starting points for developing automated support for query construction and explanation. We investigate how far recent results and techniques on learning and unique characterisations of atemporal queries mediated by an ontology can be extended to temporal data and queries. Based on a systematic review of the relevant approaches in the atemporal case, we obtain general transfer results identifying conditions under which temporal queries composed of atemporal ones are (polynomially) learnable and uniquely characterisable. △ Less

Submitted 28 July, 2024; v1 submitted 13 June, 2023; originally announced June 2023.

Comments: Full version of a KR'2024 paper

ACM Class: I.2.4; F.4.1

Reverse Engineering of Temporal Queries Mediated by LTL Ontologies

Authors: Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter, Michael Zakharyaschev

Abstract: In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explanation of the answers and non-answers. We investigate this query-by-example problem for queries formulated in positive fragments of linear temporal logic LTL over timestamped data, focusing on the design of suitable query… ▽ More In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explanation of the answers and non-answers. We investigate this query-by-example problem for queries formulated in positive fragments of linear temporal logic LTL over timestamped data, focusing on the design of suitable query languages and the combined and data complexity of deciding whether there exists a query in the given language that separates the given answers from non-answers. We consider both plain LTL queries and those mediated by LTL-ontologies. △ Less

Submitted 4 May, 2023; v1 submitted 2 May, 2023; originally announced May 2023.

Comments: To be published in IJCAI 2023 proceedings

ACM Class: I.2.4

Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic

Authors: Agi Kurucz, Frank Wolter, Michael Zakharyaschev

Abstract: None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to valid… ▽ More None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity as in classical first-order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable. △ Less

Submitted 5 June, 2024; v1 submitted 8 March, 2023; originally announced March 2023.

Efficient Sampling for Realized Variance Estimation in Time-Changed Diffusion Models

Authors: Timo Dimitriadis, Roxana Halbleib, Jeannine Polivka, Jasper Rennspies, Sina Streicher, Axel Friedrich Wolter

Abstract: This paper analyzes the benefits of sampling intraday returns in intrinsic time for the standard and pre-averaging realized variance (RV) estimators. We theoretically show in finite samples and asymptotically that the RV estimator is most efficient under the new concept of realized business time, which samples according to a combination of observed trades and estimated tick variance. Our asymptoti… ▽ More This paper analyzes the benefits of sampling intraday returns in intrinsic time for the standard and pre-averaging realized variance (RV) estimators. We theoretically show in finite samples and asymptotically that the RV estimator is most efficient under the new concept of realized business time, which samples according to a combination of observed trades and estimated tick variance. Our asymptotic results carry over to the pre-averaging RV estimator under market microstructure noise. The analysis builds on the assumption that asset prices follow a diffusion that is time-changed with a jump process that separately models the transaction times. This provides a flexible model that separately captures the empirically varying trading intensity and tick variance processes, which are particularly relevant for disentangling the driving forces of the sampling schemes. Extensive simulations confirm our theoretical results and show that realized business time remains superior also under more general noise and process specifications. An application to stock data provides empirical evidence for the benefits of using realized business time sampling to construct more efficient RV estimators as well as for an improved forecasting performance. △ Less

Submitted 23 December, 2023; v1 submitted 22 December, 2022; originally announced December 2022.

Unique Characterisability and Learnability of Temporal Instance Queries

Authors: Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter, Michael Zakharyaschev

Abstract: We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considering queries formulated in fragments of propositional linear temporal logic LTL that correspond to conjunctive queries (CQs) or extensions thereof induced by the until operator. Not all of these queries admit polynomial cha… ▽ More We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considering queries formulated in fragments of propositional linear temporal logic LTL that correspond to conjunctive queries (CQs) or extensions thereof induced by the until operator. Not all of these queries admit polynomial characterisations but by restricting them further to path-shaped queries we identify natural classes that do. We then investigate how far the obtained characterisations can be lifted to temporal knowledge graphs queried by 2D languages combining LTL with concepts in description logics EL or ELI (i.e., tree-shaped CQs). While temporal operators in the scope of description logic constructors can destroy polynomial characterisability, we obtain general transfer results for the case when description logic constructors are within the scope of temporal operators. Finally, we apply our characterisations to establish (polynomial) learnability of temporal instance queries using membership queries in the active learning framework. △ Less

Submitted 3 May, 2022; originally announced May 2022.

Comments: accepted for KR2022

ACM Class: I.2.4; F.2.2

Interpolants and Explicit Definitions in Extensions of the Description Logic EL

Authors: Marie Fortin, Boris Konev, Frank Wolter

Abstract: We show that the vast majority of extensions of the description logic $\mathcal{EL}$ do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for $\mathcal{EL}$ with nominals, $\mathcal{EL}$ with the universal role, $\mathcal{EL}$ with a role inclusion of the form $r\circ s\sqsubseteq s$, and for $\mathcal{ELI}$. It follows in particular th… ▽ More We show that the vast majority of extensions of the description logic $\mathcal{EL}$ do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for $\mathcal{EL}$ with nominals, $\mathcal{EL}$ with the universal role, $\mathcal{EL}$ with a role inclusion of the form $r\circ s\sqsubseteq s$, and for $\mathcal{ELI}$. It follows in particular that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants and explicit definitions can be decided in polynomial time for standard tractable extensions of $\mathcal{EL}$ (such as $\mathcal{EL}^{++}$) and in ExpTime for $\mathcal{ELI}$ and various extensions. It follows that these existence problems are not harder than subsumption which is in sharp contrast to the situation for expressive DLs. We also obtain tight bounds for the size of interpolants and explicit definitions and the complexity of computing them: single exponential for tractable standard extensions of $\mathcal{EL}$ and double exponential for $\mathcal{ELI}$ and extensions. We close with a discussion of Horn-DLs such as Horn-$\mathcal{ALCI}$. △ Less

Submitted 29 May, 2022; v1 submitted 14 February, 2022; originally announced February 2022.

First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries

Authors: Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z,<). Our main concern is first-order rewritability of ontology-mediated queries (OMQs) that consist of a 2D ontology and a positive temporal instance query. Our target langua… ▽ More Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z,<). Our main concern is first-order rewritability of ontology-mediated queries (OMQs) that consist of a 2D ontology and a positive temporal instance query. Our target languages for FO-rewritings are two-sorted FO(<) - first-order logic with sorts for time instants ordered by the built-in precedence relation < and for the domain of individuals - its extension FOE with the standard congruence predicates t \equiv 0 mod n, for any fixed n > 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FOE- and FO(RPR)-rewritability guarantee answering OMQs in uniform AC0 and NC1, respectively. We proceed in three steps. First, we define a hierarchy of 2D DL-Lite/LTL ontology languages and investigate the FO-rewritability of OMQs with atomic queries by constructing projections onto 1D LTL OMQs and employing recent results on the FO-rewritability of propositional LTL OMQs. As the projections involve deciding consistency of ontologies and data, we also consider the consistency problem for our languages. While the undecidability of consistency for 2D ontology languages with expressive Boolean role inclusions might be expected, we also show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to decidability (and ExpSpace-completeness), even if one admits full Booleans on concepts. As a final step, we lift some of the rewritability results for atomic OMQs to OMQs with expressive positive temporal instance queries. The lifting results are based on an in-depth study of the canonical models and only concern Horn ontologies. △ Less

Submitted 21 October, 2022; v1 submitted 12 November, 2021; originally announced November 2021.

Comments: Accepted for JAIR

ACM Class: I.2.4

How to Approximate Ontology-Mediated Queries

Authors: Anneke Haga, Carsten Lutz, Leif Sabellek, Frank Wolter

Abstract: We introduce and study several notions of approximation for ontology-mediated queries based on the description logics ALC and ALCI. Our approximations are of two kinds: we may (1) replace the ontology with one formulated in a tractable ontology language such as ELI or certain TGDs and (2) replace the database with one from a tractable class such as the class of databases whose treewidth is bounded… ▽ More We introduce and study several notions of approximation for ontology-mediated queries based on the description logics ALC and ALCI. Our approximations are of two kinds: we may (1) replace the ontology with one formulated in a tractable ontology language such as ELI or certain TGDs and (2) replace the database with one from a tractable class such as the class of databases whose treewidth is bounded by a constant. We determine the computational complexity and the relative completeness of the resulting approximations. (Almost) all of them reduce the data complexity from coNP-complete to PTime, in some cases even to fixed-parameter tractable and to linear time. While approximations of kind (1) also reduce the combined complexity, this tends to not be the case for approximations of kind (2). In some cases, the combined complexity even increases. △ Less

Submitted 30 June, 2022; v1 submitted 12 July, 2021; originally announced July 2021.

Separating Data Examples by Description Logic Concepts with Restricted Signatures

Authors: Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, Frank Wolter

Abstract: We study the separation of positive and negative data examples in terms of description logic concepts in the presence of an ontology. In contrast to previous work, we add a signature that specifies a subset of the symbols that can be used for separation, and we admit individual names in that signature. We consider weak and strong versions of the resulting problem that differ in how the negative ex… ▽ More We study the separation of positive and negative data examples in terms of description logic concepts in the presence of an ontology. In contrast to previous work, we add a signature that specifies a subset of the symbols that can be used for separation, and we admit individual names in that signature. We consider weak and strong versions of the resulting problem that differ in how the negative examples are treated and we distinguish between separation with and without helper symbols. Within this framework, we compare the separating power of different languages and investigate the complexity of deciding separability. While weak separability is shown to be closely related to conservative extensions, strongly separating concepts coincide with Craig interpolants, for suitably defined encodings of the data and ontology. This enables us to transfer known results from those fields to separability. Conversely, we obtain original results on separability that can be transferred backward. For example, rather surprisingly, conservative extensions and weak separability in ALCO are both 3ExpTime-complete. △ Less

Submitted 12 July, 2021; originally announced July 2021.

Comments: A short version of this paper has been accepted for publication in the Proceedings of KR 2021

MSC Class: 03B70

On Free Description Logics with Definite Descriptions

Authors: Alessandro Artale, Andrea Mazzullo, Ana Ozaki, Frank Wolter

Abstract: Definite descriptions are phrases of the form 'the $x$ such that $\varphi$', used to refer to single entities in a context. They are often more meaningful to users than individual names alone, in particular when modelling or querying data over ontologies. We investigate free description logics with both individual names and definite descriptions as terms of the language, while also accounting for… ▽ More Definite descriptions are phrases of the form 'the $x$ such that $\varphi$', used to refer to single entities in a context. They are often more meaningful to users than individual names alone, in particular when modelling or querying data over ontologies. We investigate free description logics with both individual names and definite descriptions as terms of the language, while also accounting for their possible lack of denotation. We focus on the extensions of $\mathcal{ALC}$ and, respectively, $\mathcal{EL}$ with nominals, the universal role, and definite descriptions. We show that standard reasoning in these extensions is not harder than in the original languages, and we characterise the expressive power of concepts relative to first-order formulas using a suitable notion of bisimulation. Moreover, we lay the foundations for automated support for definite descriptions generation by studying the complexity of deciding the existence of definite descriptions for an individual under an ontology. Finally, we provide a polynomial-time reduction of reasoning in other free description logic languages based on dual-domain semantics to the case of partial interpretations. △ Less

Submitted 29 June, 2021; originally announced June 2021.

First Order-Rewritability and Containment of Conjunctive Queries in Horn Description Logics

Authors: Meghyn Bienvenu, Peter Hansen, Carsten Lutz, Frank Wolter

Abstract: We study FO-rewritability of conjunctive queries in the presence of ontologies formulated in a description logic between EL and Horn-SHIF, along with related query containment problems. Apart from providing characterizations, we establish complexity results ranging from ExpTime via NExpTime to 2ExpTime, pointing out several interesting effects. In particular, FO-rewriting is more complex for conju… ▽ More We study FO-rewritability of conjunctive queries in the presence of ontologies formulated in a description logic between EL and Horn-SHIF, along with related query containment problems. Apart from providing characterizations, we establish complexity results ranging from ExpTime via NExpTime to 2ExpTime, pointing out several interesting effects. In particular, FO-rewriting is more complex for conjunctive queries than for atomic queries when inverse roles are present, but not otherwise. △ Less

Submitted 19 November, 2020; originally announced November 2020.

From Conjunctive Queries to Instance Queries in Ontology-Mediated Querying

Authors: Cristina Feier, Carsten Lutz, Frank Wolter

Abstract: We consider ontology-mediated queries (OMQs) based on expressive description logics of the ALC family and (unions) of conjunctive queries, studying the rewritability into OMQs based on instance queries (IQs). Our results include exact characterizations of when such a rewriting is possible and tight complexity bounds for deciding rewritability. We also give a tight complexity bound for the related… ▽ More We consider ontology-mediated queries (OMQs) based on expressive description logics of the ALC family and (unions) of conjunctive queries, studying the rewritability into OMQs based on instance queries (IQs). Our results include exact characterizations of when such a rewriting is possible and tight complexity bounds for deciding rewritability. We also give a tight complexity bound for the related problem of deciding whether a given MMSNP sentence is equivalent to a CSP. △ Less

Submitted 22 October, 2020; originally announced October 2020.

Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions

Authors: Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, Frank Wolter

Abstract: The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP reduce potentially hard existence problems to entailment in the underlying logic. Description (and modal) logics with nomin… ▽ More The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP reduce potentially hard existence problems to entailment in the underlying logic. Description (and modal) logics with nominals and/or role inclusions do not enjoy the CIP nor the PBDP, but interpolants and explicit definitions have many applications, in particular in concept learning, ontology engineering, and ontology-based data management. In this article we show that, even without Beth and Craig, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHOI and corresponding hybrid modal logics. However, living without Beth and Craig makes this problem harder than entailment: the existence problems become 2ExpTime-complete in the presence of an ontology or the universal modality, and coNExpTime-complete otherwise. We also analyze explicit definition existence if all symbols (except the one that is defined) are admitted in the definition. In this case the complexity depends on whether one considers individual or concept names. Finally, we consider the problem of computing interpolants and explicit definitions if they exist and turn the complexity upper bound proof into an algorithm computing them, at least for description logics with role inclusions. △ Less

Submitted 28 April, 2023; v1 submitted 6 July, 2020; originally announced July 2020.

Comments: We have revised a few sections from the previous version. The relationship between interpolants and explicit definitions is analysed in more detail now

MSC Class: 03B70

Separating Positive and Negative Data Examples by Concepts and Formulas: The Case of Restricted Signatures

Authors: Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, Frank Wolter

Abstract: We study the separation of positive and negative data examples in terms of description logic (DL) concepts and formulas of decidable FO fragments, in the presence of an ontology. In contrast to previous work, we add a signature that specifies a subset of the symbols from the data and ontology that can be used for separation. We consider weak and strong versions of the resulting problem that differ… ▽ More We study the separation of positive and negative data examples in terms of description logic (DL) concepts and formulas of decidable FO fragments, in the presence of an ontology. In contrast to previous work, we add a signature that specifies a subset of the symbols from the data and ontology that can be used for separation. We consider weak and strong versions of the resulting problem that differ in how the negative examples are treated. Our main results are that (a projective form of) the weak version is decidable in $\mathcal{ALCI}$ while it is undecidable in the guarded fragment GF, the guarded negation fragment GNF, and the DL $\mathcal{ALCFIO}$, and that strong separability is decidable in $\mathcal{ALCI}$, GF, and GNF. We also provide (mostly tight) complexity bounds. △ Less

Submitted 6 July, 2020; originally announced July 2020.

Comments: 35 pages

ACM Class: I.2.4; F.4.1

Logical Separability of Labeled Data Examples under Ontologies

Authors: Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, Frank Wolter

Abstract: Finding a logical formula that separates positive and negative examples given in the form of labeled data items is fundamental in applications such as concept learning, reverse engineering of database queries, generating referring expressions, and entity comparison in knowledge graphs. In this paper, we investigate the existence of a separating formula for data in the presence of an ontology. Both… ▽ More Finding a logical formula that separates positive and negative examples given in the form of labeled data items is fundamental in applications such as concept learning, reverse engineering of database queries, generating referring expressions, and entity comparison in knowledge graphs. In this paper, we investigate the existence of a separating formula for data in the presence of an ontology. Both for the ontology language and the separation language, we concentrate on first-order logic and the following important fragments thereof: the description logic $\mathcal{ALCI}$, the guarded fragment, the two-variable fragment, and the guarded negation fragment. For separation, we also consider (unions of) conjunctive queries. We consider several forms of separability that differ in the treatment of negative examples and in whether or not they admit the use of additional helper symbols to achieve separation. Our main results are model-theoretic characterizations of (all variants of) separability, the comparison of the separating power of different languages, and the investigation of the computational complexity of deciding separability. △ Less

Submitted 17 August, 2022; v1 submitted 3 July, 2020; originally announced July 2020.

Comments: Full Version of KR'20 paper

ACM Class: I.2.4; F.4.1

Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments

Authors: Jean Christoph Jung, Frank Wolter

Abstract: In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragm… ▽ More In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragment, GF, of first-order logic both fail to have the CIP and the PBDP. We show that nevertheless in both fragments the existence of interpolants and explicit definitions is decidable. In GF, both problems are 3ExpTime-complete in general, and 2ExpTime-complete if the arity of relation symbols is bounded by a constant c not smaller than 3. In FO2, we prove a coN2ExpTime upper bound and a 2ExpTime lower bound for both problems. Thus, both for GF and FO2 existence of interpolants and explicit definitions are decidable but harder than validity (in case of FO2 under standard complexity assumptions). △ Less

Submitted 18 April, 2021; v1 submitted 3 July, 2020; originally announced July 2020.

Comments: This is an updated version that also investigates the two-variable fragment of FO. The paper will appear in the proceedings of LICS 2021

MSC Class: 03B70

Searching for the Shortest Path to the Point of Voltage Collapse on the Algebraic Manifold

Authors: Dan Wu, Franz-Erich Wolter, Bin Wang, Le Xie

Abstract: Voltage instability is one of the main causes of power system blackouts. Emerging technologies such as renewable energy integration, distributed energy resources and demand responses may introduce significant uncertainties in analyzing of system-wide voltage stability. This paper starts with summarizing different known voltage instability mechanisms, and then focuses on a class of voltage instabil… ▽ More Voltage instability is one of the main causes of power system blackouts. Emerging technologies such as renewable energy integration, distributed energy resources and demand responses may introduce significant uncertainties in analyzing of system-wide voltage stability. This paper starts with summarizing different known voltage instability mechanisms, and then focuses on a class of voltage instability which is induced by the singular surface of the algebraic manifold. We argue and demonstrate that this class can include both dynamic and static voltage instabilities. To determine the minimum distance to the point of voltage collapse, a new formulation is proposed on the algebraic manifold. This formulation is further converted into an optimal control framework for identifying the path with minimum distance on the manifold. Comprehensive numerical studies are conducted on some manifolds of different power system test cases and demonstrate that the proposed method yields candidates for the local shortest paths to the singular surface on the manifold for both the dynamic model and the static model. Simulations show that the proposed method can identify shorter paths on the manifold than the paths associated with the minimum Euclidean distances. Furthermore, the proposed method always locates the right path ending at the correct singular surface which is responsible for the voltage instability; while the Euclidean distance formulation can mistakenly find solutions on the wrong singular surface. A broad range of potential applications using the proposed method are also discussed. △ Less

Submitted 16 June, 2020; v1 submitted 15 June, 2020; originally announced June 2020.

Comments: 11 pages, 9 figures

Differential Geometric Foundations for Power Flow Computations

Authors: Franz-Erich Wolter, Benjamin Berger, Alexander Vais

Abstract: This paper aims to systematically and comprehensively initiate a foundation for using concepts from computational differential geometry as instruments for power flow computing and research. At this point we focus our discussion on the static case, with power flow equations given by quadratic functions defined on voltage space with values in power space; both spaces have real Euclidean coordinates.… ▽ More This paper aims to systematically and comprehensively initiate a foundation for using concepts from computational differential geometry as instruments for power flow computing and research. At this point we focus our discussion on the static case, with power flow equations given by quadratic functions defined on voltage space with values in power space; both spaces have real Euclidean coordinates. The central issue is a differential geometric analysis of the power flow solution space boundary (SSB, also in a simplifying way, called saddle node bifurcation set, SNB) both in voltage and in power space. We present different methods for computing tangent vectors, tangent planes and normals of the SSB and the normals' derivatives. Using the latter we compute normal and principal curvatures. All this is needed for tracing the orthogonal projection of points on curves in voltage or power space onto the SSB on points closest to the given points on the curve, thus obtaining estimates for their distance to the SSB. As another example how these concepts can be useful, we present a new high precision continuation method for power flow solutions close to and on the SSB called local inversion of the power flow map from voltage to power space, assuming the dimension of power flow's Jacobean zero space, called KERNEL, is one. For inversion, we present two different geometry-based splitting techniques with one of them using the aforementioned orthogonal tracing method. △ Less

Submitted 27 April, 2020; originally announced May 2020.

Comments: 10 pages, 7 figures. arXiv admin note: substantial text overlap with arXiv:1903.11131

First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic

Authors: Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time (Z,<). Queries are given in LTL or MFO(<), monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account o… ▽ More We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time (Z,<). Queries are given in LTL or MFO(<), monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account of the temporal operators used in the ontology and distinguishing between ontologies given in full LTL and its core, Krom and Horn fragments, we identify a hierarchy of OMQs with atomic queries by proving rewritability into either FO(<), first-order logic with the built-in linear order, or FO(<,E), which extends FO(<) with the standard arithmetic predicates saying that "x is equivalent to 0 modulo n", for any fixed n > 1, or FO(RPR), which extends FO(<) with relational primitive recursion. In terms of circuit complexity, FO(<,E)- and FO(RPR)-rewritability guarantee OMQ answering in uniform AC0 and, respectively, NC1. We obtain similar hierarchies for more expressive types of queries: positive LTL-formulas, monotone MFO(<)- and arbitrary MFO(<)-formulas. Our results are directly applicable if the temporal data to be accessed is one-dimensional; moreover, they lay foundations for investigating ontology-based access using combinations of temporal and description logics over two-dimensional temporal data. △ Less

Submitted 25 May, 2021; v1 submitted 15 April, 2020; originally announced April 2020.

A Journey into Ontology Approximation: From Non-Horn to Horn

Authors: Anneke Haga, Carsten Lutz, Johannes Marti, Frank Wolter

Abstract: We study complete approximations of an ontology formulated in a non-Horn description logic (DL) such as $\mathcal{ALC}$ in a Horn DL such as~$\mathcal{EL}$. We provide concrete approximation schemes that are necessarily infinite and observe that in the $\mathcal{ELU}$-to-$\mathcal{EL}$ case finite approximations tend to exist in practice and are guaranteed to exist when the original ontology is ac… ▽ More We study complete approximations of an ontology formulated in a non-Horn description logic (DL) such as $\mathcal{ALC}$ in a Horn DL such as~$\mathcal{EL}$. We provide concrete approximation schemes that are necessarily infinite and observe that in the $\mathcal{ELU}$-to-$\mathcal{EL}$ case finite approximations tend to exist in practice and are guaranteed to exist when the original ontology is acyclic. In contrast, neither of this is the case for $\mathcal{ELU}_\bot$-to-$\mathcal{EL}_\bot$ and for $\mathcal{ALC}$-to-$\mathcal{EL}_\bot$ approximations. We also define a notion of approximation tailored towards ontology-mediated querying, connect it to subsumption-based approximations, and identify a case where finite approximations are guaranteed to exist. △ Less

Submitted 15 June, 2020; v1 submitted 21 January, 2020; originally announced January 2020.

Comments: 21 pages, 4 figures, paragraph with examples added

Model Comparison Games for Horn Description Logics

Authors: Jean Christoph Jung, Fabio Papacchini, Frank Wolter, Michael Zakharyaschev

Abstract: Horn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTime for data complexity. They were independently introduced in modal logic to capture the intersection of Horn first-order logic with modal logic. In this paper, we introduce model comparison games… ▽ More Horn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTime for data complexity. They were independently introduced in modal logic to capture the intersection of Horn first-order logic with modal logic. In this paper, we introduce model comparison games for the basic Horn description logic hornALC (corresponding to the basic Horn modal logic) and use them to obtain an Ehrenfeucht-Fraïssé type definability result and a van Benthem style expressive completeness result for hornALC. We also establish a finite model theory version of the latter. The Ehrenfeucht-Fraïssé type definability result is used to show that checking hornALC indistinguishability of models is ExpTime-complete, which is in sharp contrast to ALC indistinguishability (i.e., bisimulation equivalence) checkable in PTime. In addition, we explore the behavior of Horn fragments of more expressive description and modal logics by defining a Horn guarded fragment of first-order logic and introducing model comparison games for it. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Comments: Full version of LICS'19 paper

ACM Class: F.4.1

Differential Geometric Foundations for Power Flow Computations

Authors: Franz-Erich Wolter, Benjamin Berger

Abstract: This paper aims to systematically and comprehensively initiate a foundation for using concepts from computational differential geometry as instruments for power flow computing and research. At this point we focus our discussion on the static case, with power flow equations given by quadratic functions defined on voltage space with values in power space; both spaces have real Euclidean coordinates.… ▽ More This paper aims to systematically and comprehensively initiate a foundation for using concepts from computational differential geometry as instruments for power flow computing and research. At this point we focus our discussion on the static case, with power flow equations given by quadratic functions defined on voltage space with values in power space; both spaces have real Euclidean coordinates. Central issue is a differential geometric analysis of the power flow solution space boundary (SSB) both in voltage and in power space. We present different methods for computing tangent vectors, tangent planes and normals of the SSB and the normals' derivatives. Using the latter we compute normal and principal curvatures. All this is needed for tracing the orthogonal projection of curves in voltage and power space onto the SSB for points on the SSB cosest to given points on the curves, thus obtaining estimates for the distance to the SSB. Furthermore, we present a new high precision continuation method for power flow solutions. We also compute geodesics on the SSB or an implicitly defined submanfold thereof and, used to define geodesic coordinates together with their Jacobians on the manifolds. These computations might be the most innovative and most significant contribution of this paper, because this concept provides a comprehensive coordinate system for sub many folds defined by implicit equations. Therefore while moving on geodesics described by the geodesic coordinates of the sub manifold at hand we get, via systematic navigation guided by geodesic coordinates, access to all feasible operation points of the system. We propose some applications and show some properties of the Jacobian of the power flow map. △ Less

Submitted 25 June, 2019; v1 submitted 26 March, 2019; originally announced March 2019.

MSC Class: 53B21 (Primary); 97R30; 70G55; 53C22; 65D99 (Secondary)

Query Inseparability for ALC Ontologies

Authors: Elena Botoeva, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: We investigate the problem whether two ALC ontologies are indistinguishable (or inseparable) by means of queries in a given signature, which is fundamental for ontology engineering tasks such as ontology versioning, modularisation, update, and forgetting. We consider both knowledge base (KB) and TBox inseparability. For KBs, we give model-theoretic criteria in terms of (finite partial) homomorphis… ▽ More We investigate the problem whether two ALC ontologies are indistinguishable (or inseparable) by means of queries in a given signature, which is fundamental for ontology engineering tasks such as ontology versioning, modularisation, update, and forgetting. We consider both knowledge base (KB) and TBox inseparability. For KBs, we give model-theoretic criteria in terms of (finite partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs), but 2ExpTime-complete for unions of CQs (UCQs). The same results hold if (U)CQs are replaced by rooted (U)CQs, where every variable is connected to an answer variable. We also show that inseparability by CQs is still undecidable if one KB is given in the lightweight DL EL and if no restrictions are imposed on the signature of the CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query over any ABox in a given signature and show that, for CQs, this problem is undecidable, too. We then develop model-theoretic criteria for Horn-ALC TBoxes and show using tree automata that, in contrast, inseparability becomes decidable and 2ExpTime-complete, even ExpTime-complete when restricted to (unions of) rooted CQs. △ Less

Submitted 31 January, 2019; originally announced February 2019.

Comments: arXiv admin note: text overlap with arXiv:1604.04164

The Data Complexity of Ontology-Mediated Queries with Closed Predicates

Authors: Carsten Lutz, Inanc Seylan, Frank Wolter

Abstract: In the context of ontology-mediated querying with description logics (DLs), we study the data complexity of queries in which selected predicates can be closed (OMQCs). We provide a non-uniform analysis, aiming at a classification of the complexity into tractable and non-tractable for ontologies in the lightweight DLs DL-Lite and EL, and the expressive DL ALCHI. At the level of ontologies, we prove… ▽ More In the context of ontology-mediated querying with description logics (DLs), we study the data complexity of queries in which selected predicates can be closed (OMQCs). We provide a non-uniform analysis, aiming at a classification of the complexity into tractable and non-tractable for ontologies in the lightweight DLs DL-Lite and EL, and the expressive DL ALCHI. At the level of ontologies, we prove a dichotomy between FO-rewritable and coNP-complete for DL-Lite and between PTime and coNP-complete for EL. The meta problem of deciding tractability is proved to be in PTime. At the level of OMQCs, we show that there is no dichotomy (unless NP equals PTime) if both concept and role names can be closed. If only concept names can be closed, we tightly link the complexity of query evaluation to the complexity of surjective CSPs. We also identify a class of OMQCs based on ontologies formulated in DL-Lite that are guaranteed to be tractable and even FO-rewritable. △ Less

Submitted 27 August, 2019; v1 submitted 1 September, 2018; originally announced September 2018.

MSC Class: 68

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (August 28, 2019) lmcs:4804

Open Tactile - An open, modular hardware system for controlling tactile displays

Authors: Andreas Tarnowsky, Jan Jamaszyk, Daniel Brandes, Franz-Erich Wolter

Abstract: Tactile displays have a wide potential field of applications, ranging from enhancing Virtual-Reality scenarios up to aiding telesurgery as well as in fundamental psychological and neurophysiological research. In this paper, we describe an open source hardware and software architecture that is designed to drive a variety of different tactile displays. For demonstration purposes, a tactile computer… ▽ More Tactile displays have a wide potential field of applications, ranging from enhancing Virtual-Reality scenarios up to aiding telesurgery as well as in fundamental psychological and neurophysiological research. In this paper, we describe an open source hardware and software architecture that is designed to drive a variety of different tactile displays. For demonstration purposes, a tactile computer mouse featuring a simple tactile display, based on lateral piezoelectric (PZT) actuators, is presented. Even though we will focus on driving mechanical actuators in this paper, the system can be extended to different working principles. The suggested architecture is supplied with a custom, easy to use, software stack allowing a simple definition of tactile scenarios as well as user studies while being especially tailored to non-computer scientists. By releasing the OpenTactile system under MIT license we hope to ease the burden of controlling tactile displays as well as designing and reproducing the related experiments. △ Less

Submitted 24 April, 2018; originally announced April 2018.

Comments: 17 pages, 10 figures. This paper has not been submitted to any journal yet. It is intended to supplement the information given at the opentactile.org project pages

Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey

Authors: Elena Botoeva, Boris Konev, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: The question whether an ontology can safely be replaced by another, possibly simpler, one is fundamental for many ontology engineering and maintenance tasks. It underpins, for example, ontology versioning, ontology modularization, forgetting, and knowledge exchange. What safe replacement means depends on the intended application of the ontology. If, for example, it is used to query data, then the… ▽ More The question whether an ontology can safely be replaced by another, possibly simpler, one is fundamental for many ontology engineering and maintenance tasks. It underpins, for example, ontology versioning, ontology modularization, forgetting, and knowledge exchange. What safe replacement means depends on the intended application of the ontology. If, for example, it is used to query data, then the answers to any relevant ontology-mediated query should be the same over any relevant data set; if, in contrast, the ontology is used for conceptual reasoning, then the entailed subsumptions between concept expressions should coincide. This gives rise to different notions of ontology inseparability such as query inseparability and concept inseparability, which generalize corresponding notions of conservative extensions. We survey results on various notions of inseparability in the context of description logic ontologies, discussing their applications, useful model-theoretic characterizations, algorithms for determining whether two ontologies are inseparable (and, sometimes, for computing the difference between them if they are not), and the computational complexity of this problem. △ Less

Submitted 20 April, 2018; originally announced April 2018.

Dichotomies in Ontology-Mediated Querying with the Guarded Fragment

Authors: Andre Hernich, Carsten Lutz, Fabio Papacchini, Frank Wolter

Abstract: We study the complexity of ontology-mediated querying when ontologies are formulated in the guarded fragment of first-order logic (GF). Our general aim is to classify the data complexity on the level of ontologies where query evaluation w.r.t. an ontology O is considered to be in PTime if all (unions of conjunctive) queries can be evaluated in PTime w.r.t. O and coNP-hard if at least one query is… ▽ More We study the complexity of ontology-mediated querying when ontologies are formulated in the guarded fragment of first-order logic (GF). Our general aim is to classify the data complexity on the level of ontologies where query evaluation w.r.t. an ontology O is considered to be in PTime if all (unions of conjunctive) queries can be evaluated in PTime w.r.t. O and coNP-hard if at least one query is coNP-hard w.r.t. O. We identify several large and relevant fragments of GF that enjoy a dichotomy between PTime and coNP, some of them additionally admitting a form of counting. In fact, almost all ontologies in the BioPortal repository fall into these fragments or can easily be rewritten to do so. We then establish a variation of Ladner's Theorem on the existence of NP-intermediate problems and use this result to show that for other fragments, there is provably no such dichotomy. Again for other fragments (such as full GF), establishing a dichotomy implies the Feder-Vardi conjecture on the complexity of constraint satisfaction problems. We also link these results to Datalog-rewritability and study the decidability of whether a given ontology enjoys PTime query evaluation, presenting both positive and negative results. △ Less

Submitted 18 April, 2018; originally announced April 2018.

Exact Learning of Lightweight Description Logic Ontologies

Authors: Boris Konev, Carsten Lutz, Ana Ozaki, Frank Wolter

Abstract: We study the problem of learning description logic (DL) ontologies in Angluin et al.'s framework of exact learning via queries. We admit membership queries ("is a given subsumption entailed by the target ontology?") and equivalence queries ("is a given ontology equivalent to the target ontology?"). We present three main results: (1) ontologies formulated in (two relevant versions of) the descripti… ▽ More We study the problem of learning description logic (DL) ontologies in Angluin et al.'s framework of exact learning via queries. We admit membership queries ("is a given subsumption entailed by the target ontology?") and equivalence queries ("is a given ontology equivalent to the target ontology?"). We present three main results: (1) ontologies formulated in (two relevant versions of) the description logic DL-Lite can be learned with polynomially many queries of polynomial size; (2) this is not the case for ontologies formulated in the description logic EL, even when only acyclic ontologies are admitted; and (3) ontologies formulated in a fragment of EL related to the web ontology language OWL 2 RL can be learned in polynomial time. We also show that neither membership nor equivalence queries alone are sufficient in cases (1) and (3). △ Less

Submitted 20 September, 2017; originally announced September 2017.

Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators

Authors: Stanislav Kikot, Agi Kurucz, Yoshihito Tanaka, Frank Wolter, Michael Zakharyaschev

Abstract: Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structure… ▽ More Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic. △ Less

Submitted 22 March, 2019; v1 submitted 10 August, 2017; originally announced August 2017.

Journal ref: Journal of Symbolic Logic, 84 (2019), pp.533-588

Conservative Extensions in Guarded and Two-Variable Fragments

Authors: Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, Frank Wolter

Abstract: We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpT… ▽ More We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpTime-complete in the intersection GF$^2$ of FO$^2$ and GF. △ Less

Submitted 29 May, 2017; originally announced May 2017.

Comments: Full version of paper accepted at ICALP 2017

The Data Complexity of Description Logic Ontologies

Authors: Carsten Lutz, Frank Wolter

Abstract: We analyze the data complexity of ontology-mediated querying where the ontologies are formulated in a description logic (DL) of the ALC family and queries are conjunctive queries, positive existential queries, or acyclic conjunctive queries. Our approach is non-uniform in the sense that we aim to understand the complexity of each single ontology instead of for all ontologies formulated in a certai… ▽ More We analyze the data complexity of ontology-mediated querying where the ontologies are formulated in a description logic (DL) of the ALC family and queries are conjunctive queries, positive existential queries, or acyclic conjunctive queries. Our approach is non-uniform in the sense that we aim to understand the complexity of each single ontology instead of for all ontologies formulated in a certain language. While doing so, we quantify over the queries and are interested, for example, in the question whether all queries can be evaluated in polynomial time w.r.t. a given ontology. Our results include a PTime/coNP-dichotomy for ontologies of depth one in the description logic ALCFI, the same dichotomy for ALC- and ALCI-ontologies of unrestricted depth, and the non-existence of such a dichotomy for ALCF-ontologies. For the latter DL, we additionally show that it is undecidable whether a given ontology admits PTime query evaluation. We also consider the connection between PTime query evaluation and rewritability into (monadic) Datalog. △ Less

Submitted 10 November, 2017; v1 submitted 8 November, 2016; originally announced November 2016.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 4 (November 13, 2017) lmcs:2203

Query-Based Entailment and Inseparability for ALC Ontologies (Full Version)

Authors: Elena Botoeva, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Abstract: We investigate the problem whether two ALC knowledge bases are indistinguishable by queries over a given vocabulary. We give model-theoretic criteria in terms of (partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs) but 2EXPTIME-complete for UCQs (unions of CQs). The same results hold if CQs are replaced by rooted CQs. We also consider the pr… ▽ More We investigate the problem whether two ALC knowledge bases are indistinguishable by queries over a given vocabulary. We give model-theoretic criteria in terms of (partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs) but 2EXPTIME-complete for UCQs (unions of CQs). The same results hold if CQs are replaced by rooted CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query in a given vocabulary over all ABoxes, and show that for CQs this problem is undecidable, too, but becomes decidable and 2EXPTIME-complete in Horn-ALC, and even EXPTIME-complete in Horn-ALC when restricted to (unions of) rooted CQs. △ Less

Submitted 4 August, 2016; v1 submitted 14 April, 2016; originally announced April 2016.

Comments: The full version of the paper accepted at IJCAI 2016

The Logical Difference for the Lightweight Description Logic EL

Authors: Boris Konev, Michel Ludwig, Dirk Walther, Frank Wolter

Abstract: We study a logic-based approach to versioning of ontologies. Under this view, ontologies provide answers to queries about some vocabulary of interest. The difference between two versions of an ontology is given by the set of queries that receive different answers. We investigate this approach for terminologies given in the description logic EL extended with role inclusions and domain and range res… ▽ More We study a logic-based approach to versioning of ontologies. Under this view, ontologies provide answers to queries about some vocabulary of interest. The difference between two versions of an ontology is given by the set of queries that receive different answers. We investigate this approach for terminologies given in the description logic EL extended with role inclusions and domain and range restrictions for three distinct types of queries: subsumption, instance, and conjunctive queries. In all three cases, we present polynomial-time algorithms that decide whether two terminologies give the same answers to queries over a given vocabulary and compute a succinct representation of the difference if it is non- empty. We present an implementation, CEX2, of the developed algorithms for subsumption and instance queries and apply it to distinct versions of Snomed CT and the NCI ontology. △ Less

Submitted 22 January, 2014; originally announced January 2014.

Journal ref: Journal Of Artificial Intelligence Research, Volume 44, pages 633-708, 2012

The Complexity of Circumscription in DLs

Authors: Piero A. Bonatti, Carsten Lutz, Frank Wolter

Abstract: As fragments of first-order logic, Description logics (DLs) do not provide nonmonotonic features such as defeasible inheritance and default rules. Since many applications would benefit from the availability of such features, several families of nonmonotonic DLs have been developed that are mostly based on default logic and autoepistemic logic. In this paper, we consider circumscription as an inter… ▽ More As fragments of first-order logic, Description logics (DLs) do not provide nonmonotonic features such as defeasible inheritance and default rules. Since many applications would benefit from the availability of such features, several families of nonmonotonic DLs have been developed that are mostly based on default logic and autoepistemic logic. In this paper, we consider circumscription as an interesting alternative approach to nonmonotonic DLs that, in particular, supports defeasible inheritance in a natural way. We study DLs extended with circumscription under different language restrictions and under different constraints on the sets of minimized, fixed, and varying predicates, and pinpoint the exact computational complexity of reasoning for DLs ranging from ALC to ALCIO and ALCQO. When the minimized and fixed predicates include only concept names but no role names, then reasoning is complete for NExpTime^NP. It becomes complete for NP^NExpTime when the number of minimized and fixed predicates is bounded by a constant. If roles can be minimized or fixed, then complexity ranges from NExpTime^NP to undecidability. △ Less

Submitted 15 January, 2014; originally announced January 2014.

Journal ref: Journal Of Artificial Intelligence Research, Volume 35, pages 717-773, 2009

Temporal Description Logic for Ontology-Based Data Access (Extended Version)

Authors: Alessandro Artale, Roman Kontchakov, Frank Wolter, Michael Zakharyaschev

Abstract: Our aim is to investigate ontology-based data access over temporal data with validity time and ontologies capable of temporal conceptual modelling. To this end, we design a temporal description logic, TQL, that extends the standard ontology language OWL 2 QL, provides basic means for temporal conceptual modelling and ensures first-order rewritability of conjunctive queries for suitably defined dat… ▽ More Our aim is to investigate ontology-based data access over temporal data with validity time and ontologies capable of temporal conceptual modelling. To this end, we design a temporal description logic, TQL, that extends the standard ontology language OWL 2 QL, provides basic means for temporal conceptual modelling and ensures first-order rewritability of conjunctive queries for suitably defined data instances with validity time. △ Less

Submitted 30 April, 2013; v1 submitted 18 April, 2013; originally announced April 2013.

Comments: Full version of the IJCAI 2013 paper

Ontology-based Data Access: A Study through Disjunctive Datalog, CSP, and MMSNP

Authors: Meghyn Bienvenu, Balder ten Cate, Carsten Lutz, Frank Wolter

Abstract: Ontology-based data access is concerned with querying incomplete data sources in the presence of domain-specific knowledge provided by an ontology. A central notion in this setting is that of an ontology-mediated query, which is a database query coupled with an ontology. In this paper, we study several classes of ontology-mediated queries, where the database queries are given as some form of conju… ▽ More Ontology-based data access is concerned with querying incomplete data sources in the presence of domain-specific knowledge provided by an ontology. A central notion in this setting is that of an ontology-mediated query, which is a database query coupled with an ontology. In this paper, we study several classes of ontology-mediated queries, where the database queries are given as some form of conjunctive query and the ontologies are formulated in description logics or other relevant fragments of first-order logic, such as the guarded fragment and the unary-negation fragment. The contributions of the paper are three-fold. First, we characterize the expressive power of ontology-mediated queries in terms of fragments of disjunctive datalog. Second, we establish intimate connections between ontology-mediated queries and constraint satisfaction problems (CSPs) and their logical generalization, MMSNP formulas. Third, we exploit these connections to obtain new results regarding (i) first-order rewritability and datalog-rewritability of ontology-mediated queries, (ii) P/NP dichotomies for ontology-mediated queries, and (iii) the query containment problem for ontology-mediated queries. △ Less

Submitted 6 June, 2013; v1 submitted 28 January, 2013; originally announced January 2013.

Combining Spatial and Temporal Logics: Expressiveness vs. Complexity

Authors: D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev

Abstract: In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and computational realisability within the h… ▽ More In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and computational realisability within the hierarchy. We demonstrate how different combining principles as well as spatial and temporal primitives can produce NP-, PSPACE-, EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal logics out of components that are at most NP- or PSPACE-complete. △ Less

Submitted 12 October, 2011; originally announced October 2011.

Journal ref: Journal Of Artificial Intelligence Research, Volume 23, pages 167-243, 2005

Fusions of Description Logics and Abstract Description Systems

Authors: F. Baader, C. Lutz, H. Sturm, F. Wolter

Abstract: Fusions are a simple way of combining logics. For normal modal logics, fusions have been investigated in detail. In particular, it is known that, under certain conditions, decidability transfers from the component logics to their fusion. Though description logics are closely related to modal logics, they are not necessarily normal. In addition, ABox reasoning in description logics… ▽ More Fusions are a simple way of combining logics. For normal modal logics, fusions have been investigated in detail. In particular, it is known that, under certain conditions, decidability transfers from the component logics to their fusion. Though description logics are closely related to modal logics, they are not necessarily normal. In addition, ABox reasoning in description logics is not covered by the results from modal logics. In this paper, we extend the decidability transfer results from normal modal logics to a large class of description logics. To cover different description logics in a uniform way, we introduce abstract description systems, which can be seen as a common generalization of description and modal logics, and show the transfer results in this general setting. △ Less

Submitted 9 June, 2011; originally announced June 2011.

Journal ref: Journal Of Artificial Intelligence Research, Volume 16, pages 1-58, 2002

Description Logic TBoxes: Model-theoretic Characterizations and Rewritability

Authors: Carsten Lutz, Robert Piro, Frank Wolter

Abstract: We characterize the expressive power of description logic (DL) TBoxes, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. Our characterizations are relative to first-order logic, based on a wide range of semantic notions such as bisimulation, equisimulation, disjoint union, and direct product. We exemplify the use of the characterizations by a first study of… ▽ More We characterize the expressive power of description logic (DL) TBoxes, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. Our characterizations are relative to first-order logic, based on a wide range of semantic notions such as bisimulation, equisimulation, disjoint union, and direct product. We exemplify the use of the characterizations by a first study of the following novel family of decision problems: given a TBox T formulated in a DL L, decide whether T can be equivalently rewritten as a TBox in the fragment L' of L. △ Less

Submitted 15 April, 2011; v1 submitted 14 April, 2011; originally announced April 2011.

Comments: Submitted and accepted for IJCAI 2011

Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics

Authors: Carsten Lutz, Frank Wolter

Abstract: We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoreti… ▽ More We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoretic and automata-theoretic methods that, as a by-product, also provides characterizations of and decision procedures for conservative extensions. △ Less

Submitted 14 April, 2011; originally announced April 2011.

Spatial logics with connectedness predicates

Authors: Roman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, Michael Zakharyaschev

Abstract: We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, Exp… ▽ More We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, ExpTime and, if component counting is allowed, to NExpTime. △ Less

Submitted 18 October, 2010; v1 submitted 28 March, 2010; originally announced March 2010.

Comments: Some results of the paper were presented at LPAR 2008 and ECAI 2000

ACM Class: F.4.1, I.2.4

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 3 (August 18, 2010) lmcs:1229

Undecidability of the unification and admissibility problems for modal and description logics

Authors: Frank Wolter, Michael Zakharyaschev

Abstract: We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem for inference rules is undecidable for these logics as well. These are the first examples of standard decidable modal logics for which the unific… ▽ More We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem for inference rules is undecidable for these logics as well. These are the first examples of standard decidable modal logics for which the unification and admissibility problems are undecidable. We also prove undecidability of the unification and admissibility problems for K and K4 with at least two modal operators and nominals (instead of the universal modality), thereby showing that these problems are undecidable for basic hybrid logics. Recently, unification has been introduced as an important reasoning service for description logics. The undecidability proof for K with nominals can be used to show the undecidability of unification for boolean description logics with nominals (such as ALCO and SHIQO). The undecidability proof for K with the universal modality can be used to show that the unification problem relative to role boxes is undecidable for Boolean description logic with transitive roles, inverse roles, and role hierarchies (such as SHI and SHIQ). △ Less

Submitted 11 September, 2006; originally announced September 2006.

Modal Logics of Topological Relations

Authors: Carsten Lutz, Frank Wolter

Abstract: Logical formalisms for reasoning about relations between spatial regions play a fundamental role in geographical information systems, spatial and constraint databases, and spatial reasoning in AI. 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 Eg… ▽ More Logical formalisms for reasoning about relations between spatial regions play a fundamental role in geographical information systems, spatial and constraint databases, and spatial reasoning in AI. 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 Egenhofer-Franzosa (or RCC8) relations between regions in topological spaces such as the real plane. We investigate the expressive power and computational complexity of logics obtained in this way. It turns out that our modal logics have the same expressive power as the two-variable fragment of first-order logic, but are exponentially less succinct. The complexity ranges from (undecidable and) recursively enumerable to highly undecidable, where the recursively enumerable logics are obtained by considering substructures of structures induced by topological spaces. As our undecidability results also capture logics based on the real line, they improve upon undecidability results for interval temporal logics by Halpern and Shoham. We also analyze modal logics based on the five RCC5 relations, with similar results regarding the expressive power, but weaker results regarding the complexity. △ Less

Submitted 22 June, 2006; v1 submitted 15 May, 2006; originally announced May 2006.

ACM Class: F.4.1; H.2.8; I.2.4

Journal ref: Logical Methods in Computer Science, Volume 2, Issue 2 (June 22, 2006) lmcs:2253