arXiv subjects

Michael Zakharyaschev

Publications and source records attributed to Michael Zakharyaschev.

At least 37 records · Page 2Linked to original sources

arXiv2019

Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)

We investigate the data complexity of answering queries mediated by metric temporal logic ontologies under the event-based semantics assuming that data instances are finite timed words timestamped with binary fractions. We identify classes of ontology-mediated queries answering which can be done in AC0, NC1, L, NL, P, and coNP for data complexity, provide their rewritings to first-order logic and its extensions with primitive recursion, transitive closure or datalog, and establish lower complexity bounds.

cs.LO↗

arXiv2019

Model Comparison Games for Horn Description Logics

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.

cs.LO↗

arXiv2019

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

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.

cs.LO↗

arXiv2019

Query Inseparability for ALC Ontologies

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.

cs.AI↗

arXiv2018

Querying Log Data with Metric Temporal Logic (Technical Report)

We propose a novel framework for ontology-based access to temporal log data using a datalog extension datalogMTL of a Horn fragment of the metric temporal logic MTL. We show that datalogMTL is ExpSpace-complete even with punctual intervals, in which case full MTL is known to be undecidable. We also prove that nonrecursive datalogMTL is PSpace-complete for combined complexity and in AC0 for data complexity. We demonstrate by two real-world use cases that nonrecursive datalogMTL programs can express complex temporal concepts from typical user queries and thereby facilitate access to temporal log data. Our experiments with Siemens turbine data and MesoWest weather data show that datalogMTL ontology-mediated queries are efficient and scale on large datasets.

cs.LO↗

arXiv2018

Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey

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.

cs.AI↗

arXiv2017

Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics, but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.

cs.LO↗

arXiv2017

Metric Temporal Logic for Ontology-Based Data Access over Log Data

We present a new metric temporal logic HornMTL over dense time and its datalog extension datalogMTL. The use of datalogMTL is demonstrated in the context of ontology-based data access over meteorological data. We show decidability of answering ontology-mediated queries for a practically relevant non-recursive fragment of datalogMTL. Finally, we discuss directions of the future work, including the potential use-cases in analyzing log data of engines and devices.

cs.LO↗

arXiv2016

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

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.

cs.LO↗

arXiv2016

Ontology-Mediated Queries: Combined Complexity and Succinctness of Rewritings via Circuit Complexity

We give solutions to two fundamental computational problems in ontology-based data access with the W3C standard ontology language OWL 2 QL: the succinctness problem for first-order rewritings of ontology-mediated queries (OMQs), and the complexity problem for OMQ answering. We classify OMQs according to the shape of their conjunctive queries (treewidth, the number of leaves) and the existential depth of their ontologies. For each of these classes, we determine the combined complexity of OMQ answering, and whether all OMQs in the class have polynomial-size first-order, positive existential, and nonrecursive datalog rewritings. We obtain the succinctness results using hypergraph programs, a new computational model for Boolean functions, which makes it possible to connect the size of OMQ rewritings and circuit complexity.

cs.DB↗

arXiv2016

Theoretically Optimal Datalog Rewritings for OWL 2 QL Ontology-Mediated Queries

We show that, for OWL 2 QL ontology-mediated queries with (i) ontologies of bounded depth and conjunctive queries of bounded treewidth, (ii) ontologies of bounded depth and bounded-leaf tree-shaped conjunctive queries, and (iii) arbitrary ontologies and bounded-leaf tree-shaped conjunctive queries, one can construct and evaluate nonrecursive datalog rewritings by, respectively, LOGCFL, NL and LOGCFL algorithms, which matches the optimal combined complexity.

cs.LO↗

arXiv2014

A Cookbook for Temporal Conceptual Data Modelling with Description Logics

We design temporal description logics suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based on DL-Lite logics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. In the temporal dimension, they capture future and past temporal operators on concepts, flexible and rigid roles, the operators `always' and `some time' on roles, data assertions for particular moments of time and global concept inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (Z,<), satisfying the constant domain assumption. We prove that the most expressive of our temporal description logics (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turn out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions we obtain logics whose complexity ranges between PSpace and NLogSpace. These positive results were obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.

cs.LO↗

arXiv2014

On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Shallow Chases

We investigate the size of first-order rewritings of conjunctive queries over OWL 2 QL ontologies of depth 1 and 2 by means of hypergraph programs computing Boolean functions. Both positive and negative results are obtained. Conjunctive queries over ontologies of depth 1 have polynomial-size nonrecursive datalog rewritings; tree-shaped queries have polynomial positive existential rewritings; however, in the worst case, positive existential rewritings can only be of superpolynomial size. Positive existential and nonrecursive datalog rewritings of queries over ontologies of depth 2 suffer an exponential blowup in the worst case, while first-order rewritings are superpolynomial unless $\text{NP} \subseteq \text{P}/\text{poly}$. We also analyse rewritings of tree-shaped queries over arbitrary ontologies and observe that the query entailment problem for such queries is fixed-parameter tractable.

cs.LO↗

arXiv2014

The DL-Lite Family and Relations

The recently introduced series of description logics under the common moniker DL-Lite has attracted attention of the description logic and semantic web communities due to the low computational complexity of inference, on the one hand, and the ability to represent conceptual modeling formalisms, on the other. The main aim of this article is to carry out a thorough and systematic investigation of inference in extensions of the original DL-Lite logics along five axes: by (i) adding the Boolean connectives and (ii) number restrictions to concept constructs, (iii) allowing role hierarchies, (iv) allowing role disjointness, symmetry, asymmetry, reflexivity, irreflexivity and transitivity constraints, and (v) adopting or dropping the unique same assumption. We analyze the combined complexity of satisfiability for the resulting logics, as well as the data complexity of instance checking and answering positive existential queries. Our approach is based on embedding DL-Lite logics in suitable fragments of the one-variable first-order logic, which provides useful insights into their properties and, in particular, computational behavior.

cs.LO↗

arXiv2013

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

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.

cs.LO↗

arXiv2012

Exponential Lower Bounds and Separation for Query Rewriting

We establish connections between the size of circuits and formulas computing monotone Boolean functions and the size of first-order and nonrecursive Datalog rewritings for conjunctive queries over OWL 2 QL ontologies. We use known lower bounds and separation results from circuit complexity to prove similar results for the size of rewritings that do not use non-signature constants. For example, we show that, in the worst case, positive existential and nonrecursive Datalog rewritings are exponentially longer than the original queries; nonrecursive Datalog rewritings are in general exponentially more succinct than positive existential rewritings; while first-order rewritings can be superpolynomially more succinct than positive existential rewritings.

cs.LO↗

arXiv2011

Topological Logics with Connectedness over Euclidean Spaces

We consider the quantifier-free languages, Bc and Bc0, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of n-dimensional Euclidean space (n greater than 1) and, additionally, over the regular closed polyhedral sets of n-dimensional Euclidean space. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric "Qualitative Spatial Reasoning." We prove that the satisfiability problem for Bc is undecidable over the regular closed polyhedra in all dimensions greater than 1, and that the satisfiability problem for both languages is undecidable over both the regular closed sets and the regular closed polyhedra in the Euclidean plane. However, we also prove that the satisfiability problem for Bc0 is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed polyhedra is ExpTime-complete. Our results show, in particular, that spatial reasoning over Euclidean spaces is much harder than reasoning over arbitrary topological spaces.

cs.LO↗

arXiv2011

On the Decidability of Connectedness Constraints in 2D and 3D Euclidean Spaces

We investigate (quantifier-free) spatial constraint languages with equality, contact and connectedness predicates as well as Boolean operations on regions, interpreted over low-dimensional Euclidean spaces. We show that the complexity of reasoning varies dramatically depending on the dimension of the space and on the type of regions considered. For example, the logic with the interior-connectedness predicate (and without contact) is undecidable over polygons or regular closed sets in the Euclidean plane, NP-complete over regular closed sets in three-dimensional Euclidean space, and ExpTime-complete over polyhedra in three-dimensional Euclidean space.

cs.LO↗