Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
TIME Conference 2025 Conference Paper
The talk gives a survey of recent results on two types of problems for linear temporal logics: one is related to the existence of a Craig interpolant for a given implication in a temporal logic, the other to the existence of a temporal query separating two given sets of temporal data instances.
IJCAI Conference 2024 Conference Paper
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.
KR Conference 2024 Conference Paper
Algorithms for learning database queries from examples and unique characterisations of queries by examples are prominent starting points for developing automated support for query explanation and construction. 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.
JAIR Journal 2023 Journal Article
Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) formulated in linear temporal logic LTL over (Z,<) and deciding whether it is rewritable to an FO(<)-query, possibly with some extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC0, ACC0 and NC1 coincides with FO(<,≡)-rewritability using unary predicates x ≡ 0 (mod n), FO(<,MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We prove that, similarly to known PSᴘᴀᴄᴇ-completeness of recognising FO(<)-definability of regular languages, deciding FO(<,≡)- and FO(<,MOD)-definability is also PSᴘᴀᴄᴇ-complete (unless ACC0 = NC1). We then use this result to show that deciding FO(<)-, FO(<,≡)- and FO(<,MOD)-rewritability of LTL OMQs is ExᴘSᴘᴀᴄᴇ-complete, and that these problems become PSᴘᴀᴄᴇ-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<,≡)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSᴘᴀᴄᴇ-, Π2p- and coNP-complete.
KR Conference 2023 Conference Paper
We first consider two decidable fragments of quantified modal logic S5: the one-variable fragment and its extension S5ALC that combines S5 and the description logic ALC with the universal role. As neither of them enjoys Craig interpolation or projective Beth definability, the existence of interpolants and explicit definitions of predicates---which is crucial in many knowledge engineering tasks---does not directly reduce to entailment. Our concern therefore is the computational complexity of deciding whether (uniform) interpolants and definitions exist for given input formulas, signatures and ontologies. We prove that interpolant and definition existence in the one-variable fragment of quantified modal logic S5 and in S5ALC is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. Then we show that interpolant and definition existence in the one-variable fragment of quantified modal logic K is nonelementary decidable, while uniform interpolant existence is undecidable.
IJCAI Conference 2023 Conference Paper
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.
AIJ Journal 2022 Journal Article
Our concern is the problem of efficiently determining the data complexity of answering queries mediated by description logic ontologies and constructing their optimal rewritings to standard database queries. Originated in ontology-based data access and datalog optimisation, this problem is known to be computationally very complex in general, with no explicit syntactic characterisations available. In this article, aiming to understand the fundamental roots of this difficulty, we strip the problem to the bare bones and focus on Boolean conjunctive queries mediated by a simple covering axiom stating that one class is covered by the union of two other classes. We show that, on the one hand, these rudimentary ontology-mediated queries, called disjunctive sirups (or d-sirups), capture many features and difficulties of the general case. For example, answering d-sirups is Π 2 p -complete for combined complexity and can be in Image 1 or L-, NL-, P-, or coNP-complete for data complexity (with the problem of recognising FO-rewritability of d-sirups being 2ExpTime-hard); some d-sirups only have exponential-size resolution proofs, some only double-exponential-size positive existential FO-rewritings and single-exponential-size nonrecursive datalog rewritings. On the other hand, we prove a few partial sufficient and necessary conditions of FO- and (symmetric/linear-) datalog rewritability of d-sirups. Our main technical result is a complete and transparent syntactic Image 1 /NL/P/coNP tetrachotomy of d-sirups with disjoint covering classes and a path-shaped Boolean conjunctive query. To obtain this tetrachotomy, we develop new techniques for establishing P- and coNP-hardness of answering non-Horn ontology-mediated queries as well as showing that they can be answered in NL.
JAIR Journal 2022 Journal Article
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, 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FO( 0 and NC 1, 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.
IJCAI Conference 2022 Conference Paper
We argue that linear temporal logic LTL in tandem with monadic first-order logic can be used as a ba- sic language for ontology-based access to tempo- ral data and obtain a classification of the resulting ontology-mediated queries according to the type of standard first-order queries they can be rewritten to.
KR Conference 2022 Conference Paper
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 imposing a further restriction 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.
TIME Conference 2021 Conference Paper
Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL over (ℤ, <) and deciding whether it is rewritable to an FO(<)-query, possibly with extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC⁰, ACC⁰ and NC¹ coincides with FO(<, ≡)-rewritability using unary predicates x ≡ 0 (mod n), FO(<, MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We then show that deciding FO(<)-, FO(<, ≡)- and FO(<, MOD)-rewritability of LTL OMQs is ExpSpace-complete, and that these problems become PSpace-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<, ≡)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSpace-, Π₂^p- and coNP-complete.
AIJ Journal 2021 Journal Article
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 ( <, ≡ ), which extends FO ( < ) with the standard arithmetic predicates x ≡ 0 ( mod n ), for any fixed n > 1, or FO ( RPR ), which extends FO ( < ) with relational primitive recursion. In terms of circuit complexity, FO ( <, ≡ ) - and FO ( RPR ) -rewritability guarantee OMQ answering in uniform Image 1 and, respectively, Image 2. 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.
KR Conference 2020 Conference Paper
Aiming to understand the data complexity of answering conjunctive queries mediated by an axiom stating that a class is covered by the union of two other classes, we show that deciding their first-order rewritability is PSPACE-hard and obtain a number of sufficient conditions for membership in AC0, L, NL, and P. Our main result is a complete syntactic AC0/NL/P/CONP tetrachotomy of path queries under the assumption that the covering classes are disjoint.
KR Conference 2020 Conference Paper
Traditionally, description logic has focused on representing and reasoning about classes rather than relations (roles), which has been justified by the deterioration of the computational properties if expressive role inclusions are added. The situation is even worse in the temporalised setting, where monodicity is viewed as an almost necessary condition for decidability. We take a fresh look at the description logic DL-Lite with expressive role inclusions, both with and without a temporal dimension. While we confirm that full Boolean expressive power on roles leads to FO^2-like behaviour in the atemporal case and undecidability in the temporal case, we show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to much lower complexity in the atemporal case and to decidability (and ExpSpace-completeness) in the temporal case, even if one admits full Booleans on concepts. The latter result is one of very few instances breaking the monodicity barrier in temporal FO. This is also reflected on the data complexity level, where we obtain new rewritability results into FO with relational primitive recursion and FO with unary divisibility predicates.
IJCAI Conference 2019 Conference Paper
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.
AIJ Journal 2019 Journal Article
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.
TIME Conference 2019 Conference Paper
Motivated by two industrial use cases that involve detecting events of interest in (asynchronous) time series from sensors in manufacturing rigs and gas turbines, we design an expressive rule language DslD equipped with interval aggregate functions (such as weighted average over a time interval), Allen’s interval relations and various metric constructs. We demonstrate how to model events in the uses cases in terms of DslD programs. We show that answering DslD queries in our use cases can be reduced to evaluating SQL queries. Our experiments with the use cases, carried out on the Apache Spark system, show that such SQL queries scale well on large real-world datasets.
IJCAI Conference 2018 Conference Paper
We present the framework of ontology-based data access, a semantic paradigm for providing a convenient and user-friendly access to data repositories, which has been actively developed and studied in the past decade. Focusing on relational data sources, we discuss the main ingredients of ontology-based data access, key theoretical results, techniques, applications and future challenges.
JAIR Journal 2018 Journal Article
We propose a novel framework for ontology-based access to temporal log data using a datalog extension datalogMTL of the 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.
AAAI Conference 2017 Conference Paper
We advocate datalogMTL, a datalog extension of a Horn fragment of the metric temporal logic MTL, as a language for ontology-based access to temporal log data. We show that datalogMTL is EXPSPACE-complete even with punctual intervals, in which case MTL is known to be undecidable. Nonrecursive datalogMTL turns out to be 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 log data. Our experiments with Siemens turbine data and MesoWest weather data show that datalogMTL ontologymediated queries are efficient and scale on large datasets of up to 11GB.
TIME Conference 2017 Conference Paper
We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we analyse ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS_n, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.
IJCAI Conference 2016 Conference Paper
We investigate the problem of conservative rewritability of a TBox T in a description logic L into a TBox T' in a weaker description logic L'. We focus on model-conservative rewritability (T' entails T and all models of T are expandable to models of T'), subsumption-conservative rewritability (T' entails T and all subsumptions in the signature of T entailed by T' are entailed by T), and standard description logics between ALC and ALCQI. We give model-theoretic characterizations of conservative rewritability via bisimulations, inverse p-morphisms and generated subinterpretations, and use them to obtain a few rewriting algorithms and complexity results for deciding rewritability.
AIJ Journal 2016 Journal Article
We consider conjunctive query inseparability of description logic knowledge bases with respect to a given signature—a fundamental problem in knowledge base versioning, module extraction, forgetting and knowledge exchange. We give a uniform game-theoretic characterisation of knowledge base conjunctive query inseparability and develop worst-case optimal decision algorithms for fragments of Horn- ALCHI, including the description logics underpinning OWL 2 QL and OWL 2 EL. We also determine the data and combined complexity of deciding query inseparability. While query inseparability for all of these logics is P-complete for data complexity, the combined complexity ranges from P- to ExpTime- to 2ExpTime-completeness. We use these results to resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal conjunctive query solutions in knowledge exchange are both ExpTime-complete for combined complexity. Finally, we introduce a more flexible notion of inseparability which compares answers to conjunctive queries in a given signature over a given set of individuals. In this case, checking query inseparability becomes NP-complete for data complexity, but the ExpTime- and 2ExpTime-completeness combined complexity results are preserved.
IJCAI Conference 2016 Conference Paper
We design an extension datalogHS of datalog with hyperrectangle generalisations of Halpern-Shoham's modal operators on intervals and a corresponding query language. We prove that, over n-dimensional spaces comprised of Z and R, finding certain answers to datalogHS queries can be reduced to standard datalog query answering. We present experimental results showing the expressivity and efficiency of datalogHS on historical data.
IJCAI Conference 2015 Conference Paper
Aiming at ontology-based data access over temporal, in particular streaming data, we design a language of ontology-mediated queries by extending OWL 2 QL and SPARQL with temporal operators, and investigate rewritability of these queries into two-sorted first-order logic with < and PLUS over time.
AAAI Conference 2015 Conference Paper
We design a tractable Horn fragment of the Halpern-Shoham temporal logic and extend it to interval-based temporal description logics, instance checking in which is P-complete for both combined and data complexity.
IJCAI Conference 2015 Conference Paper
Deciding inseparability of description logic knowledge bases (KBs) with respect to conjunctive queries is fundamental for many KB engineering and maintenance tasks including versioning, module extraction, knowledge exchange and forgetting. We study the combined and data complexity of this inseparability problem for fragments of Horn-ALCHI, including the description logics underpinning OWL 2 QL and OWL 2 EL.
KR Conference 2014 Conference Paper
a signature consisting of concept and role names. We call KBs K1 and K2 Σ-query inseparable and write K1 ≡Σ K2 if any CQ formulated in Σ has the same answers over K1 and K2. Note that even for Σ containing all concept and role names, Σ-query inseparability does not necessarily imply logical equivalence. The relativisation to (smaller) signatures is crucial to support the tasks mentioned above: We investigate conjunctive query inseparability of description logic (DL) knowledge bases (KBs) with respect to a given signature, a fundamental problem for KB versioning, module extraction, forgetting and knowledge exchange. We study the data and combined complexity of deciding KB query inseparability for fragments of Horn-ALCHI, including the DLs underpinning OWL 2 QL and OWL 2 EL. While all of these DLs are P-complete for data complexity, the combined complexity ranges from P to E XP T IME and 2E XP T IME. We also resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal UCQ-solutions in knowledge exchange are both E XP T IME-complete for combined complexity. (versioning) When comparing two versions K1 and K2 of a KB with respect to their answers to CQs in a relevant signature Σ, the basic task is to check whether K1 ≡Σ K2. (modularisation) A Σ-module of a KB K is a KB K0 ⊆ K such that K0 ≡Σ K. If we are only interested in answering CQs in Σ over K, then we can achieve our aim by querying any Σ-module of K instead of K itself. (knowledge exchange) In knowledge exchange, we want to transform a KB K1 in a signature Σ1 to a new KB K2 in a disjoint signature Σ2 connected to Σ1 via a declarative mapping specification given by a TBox T12. Thus, the target KB K2 should satisfy the condition K1 ∪ T12 ≡Σ2 K2, in which case it is called a universal UCQ-solution (CQ and UCQ inseparabilities coincide for Horn DLs). (forgetting) A KB K0 results from forgetting a signature Σ in a KB K if K0 ≡sig(K)\Σ K and sig(K0) ⊆ sig(K) \ Σ. Thus, the result of forgetting Σ does not use Σ and gives the same answers to CQs without symbols in Σ as K.
AIJ Journal 2014 Journal Article
The language RCC 8 is a widely-studied formalism for describing topological arrangements of spatial regions. The variables of this language range over the collection of non-empty, regular closed sets of n-dimensional Euclidean space, here denoted RC + ( R n ), and its non-logical primitives allow us to specify how the interiors, exteriors and boundaries of these sets intersect. The key question is the satisfiability problem: given a finite set of atomic RCC 8 -constraints in m variables, determine whether there exists an m-tuple of elements of RC + ( R n ) satisfying them. These problems are known to coincide for all n ≥ 1, so that RCC 8 -satisfiability is independent of dimension. This common satisfiability problem is NLogSpace-complete. Unfortunately, RCC 8 lacks the means to say that a spatial region comprises a ‘single piece’, and the present article investigates what happens when this facility is added. We consider two extensions of RCC 8: RCC 8 c, in which we can state that a region is connected, and RCC 8 c ∘, in which we can instead state that a region has a connected interior. The satisfiability problems for both these languages are easily seen to depend on the dimension n, for n ≤ 3. Furthermore, in the case of RCC 8 c ∘, we show that there exist finite sets of constraints that are satisfiable over RC + ( R 2 ), but only by ‘wild’ regions having no possible physical meaning. This prompts us to consider interpretations over the more restrictive domain of non-empty, regular closed, polyhedral sets, RCP + ( R n ). We show that (a) the satisfiability problems for RCC 8 c (equivalently, RCC 8 c ∘ ) over RC + ( R ) and RCP + ( R ) are distinct and both NP-complete; (b) the satisfiability problems for RCC 8 c over RC + ( R 2 ) and RCP + ( R 2 ) are identical and NP-complete; (c) the satisfiability problems for RCC 8 c ∘ over RC + ( R 2 ) and RCP + ( R 2 ) are distinct, and the latter is NP-complete. Decidability of the satisfiability problem for RCC 8 c ∘ over RC + ( R 2 ) is open. For n ≥ 3, RCC 8 c and RCC 8 c ∘ are not interestingly different from RCC 8. We finish by answering the following question: given that a set of RCC 8 c - or RCC 8 c ∘ -constraints is satisfiable over RC + ( R n ) or RCP + ( R n ), how complex is the simplest satisfying assignment? In particular, we exhibit, for both languages, a sequence of constraints Φ n, satisfiable over RCP + ( R 2 ), such that the size of Φ n grows polynomially in n, while the smallest configuration of polygons satisfying Φ n cuts the plane into a number of pieces that grows exponentially. We further show that, over RC + ( R 2 ), RCC 8 c again requires exponentially large satisfying diagrams, while RCC 8 c ∘ can force regions in satisfying configurations to have infinitely many components.
AIJ Journal 2014 Journal Article
We give a solution to the succinctness problem for the size of first-order rewritings of conjunctive queries in ontology-based data access with ontology languages such as OWL 2 QL, linear Datalog ± and sticky Datalog ±. We show that positive existential and nonrecursive datalog rewritings, which do not use extra non-logical symbols (except for intensional predicates in the case of datalog rewritings), suffer an exponential blowup in the worst case, while first-order rewritings can grow superpolynomially unless NP ⊆ P / poly. We also prove that 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. On the other hand, we construct polynomial-size positive existential and nonrecursive datalog rewritings under the assumption that any data instance contains two fixed constants.
IJCAI Conference 2013 Conference Paper
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 firstorder rewritability of conjunctive queries for suitably defined data instances with validity time.
LPAR Conference 2013 Conference Paper
Abstract We introduce and investigate a number of fragments of propositional temporal logic LTL over the flow of time (ℤ, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of the temporal formulas. We determine the computational complexity of the satisfiability problem for each of the fragments, which ranges from NLogSpace to PTime, NP and PSpace.
KR Conference 2012 Conference Paper
tional constants and predicates. Optimised (but still exponential) pure rewritings to nonrecursive Datalog were suggested by Rosati and Almatelli (2010) and Gottlob, Orsi, and Pieris (2011). The combined approach of Kontchakov et al. (2010) was developed for OWL 2 QL without role inclusions; it uses a simple polynomial rewriting over the data expanded by applying the ontology axioms and introducing a small number of new individuals. The diversity of approaches to query rewriting prompts another question: what is the type/shape/size of rewritings we should aim at to make OBDA with OWL 2 QL efficient? When trying to answer this question, we should bear in mind that (i) the OBDA paradigm relies on the proven efficiency of RDBMSs, but (ii) database query answering is not tractable in the size of queries (PS PACE-complete for FO queries and NP-complete for CQs). High efficiency of RDBMSs in practice appears to indicate only that answering real-world queries over real-world databases turns out to be tractable. As rewritings can turn a standard query to something ‘out of this world, ’ a first rule of thumb could be as follows: the rewritten query should look similar to the original one. In this respect, as Gottlob and Schwentick (2011) remark, their polynomial rewriting is of rather ‘theoretical nature’ (it uses the extra constants, predicates and existentially quantified variables to encode, by making nondeterministic guesses, a relevant part of the chase, aka the canonical model; see the discussion in Conclusions for more details). The aim of this paper is to investigate what causes exponentially long pure rewritings of CQs over OWL 2 QL ontologies and to check experimentally whether those ‘bad guys’ occur in real-world queries and ontologies. As a result of this analysis, we suggest some short (polynomial-size) rewritings that cover most, if not all, practical cases. We think of a CQ as a labelled directed multigraph. For example, the query ‘find x1, x2, x3 for which We present a novel rewriting technique for conjunctive query answering over OWL 2 QL ontologies. In general, the obtained rewritings are not necessarily correct and can be of exponential size in the length of the query. We argue, however, that in most, if not all, practical cases the rewritings are correct and of polynomial size. Moreover, we prove some sufficient conditions, imposed on queries and ontologies, that guarantee correctness and succinctness. We also support our claim by experimental results.
AAAI Conference 2011 Conference Paper
The OWL 2 profile OWL 2 QL, based on the DL-Lite family of description logics, is emerging as a major language for developing new ontologies and approximating the existing ones. Its main application is ontology-based data access, where ontologies are used to provide background knowledge for answering queries over data. We investigate the corresponding notion of query inseparability (or equivalence) for OWL 2 QL ontologies and show that deciding query inseparability is PSPACE-hard and in EXPTIME. We give polynomial time (incomplete) algorithms and demonstrate by experiments that they can be used for practical module extraction.
IJCAI Conference 2011 Conference Paper
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.
IJCAI Conference 2011 Conference Paper
The use of ontologies for accessing data is one of the most exciting new applications of description logic in databases and other information systems. A realistic way of realising sufficiently scalable ontology- based data access in practice is by reduction to querying relational databases. In this paper, we describe the 'combined approach, ' which incorporates the information given by the ontology into the data and employs query rewriting to eliminate spurious answers. We illustrate this approach for ontologies given in the DL-Lite family of description logics and briefly discuss the results obtained for the EL family.
KR Conference 2010 Conference Paper
Topological logics are a family of languages for representing and reasoning about topological data. In this paper, we consider propositional topological logics able to express the property of connectedness. The satisfiability problem for such logics is shown to depend not only on the spaces they are interpreted in, but also on the subsets of those spaces over which their variables are allowed to range. We identify the crucial notion of tameness, and chart the surprising patterns of sensitivity to the presence of non-tame regions exhibited by a range of topological logics in low-dimensional Euclidean spaces. We referred to r1, r2 and r3 above as ‘regions, ’ and depicted them as discs in the plane. But a moment’s thought shows that the set of valid formulas of any topological logic depends on the precise collection of regions we have in mind. For instance, there are RCC8-formulas that are valid as long as regions are taken to be discs in the plane, but invalid when regions are allowed to be disconnected (i. e. to consist of more than one ‘piece’). Thus, an important semantic issue for a topological logic like RCC8 is to identify the intended models. In this paper, we consider propositional topological logics with connectedness, i. e. topological logics in which the only logical connectives are the usual Boolean operators, but where there is a non-logical primitive expressing the property of topological connectedness (or a variant thereof). We show that such topological logics are typically sensitive both to the spaces they are interpreted over and—more particularly—to the subsets of those spaces over which their variables are allowed to range. We identify the crucial notion of tameness, and chart the surprising patterns of sensitivity to the presence of non-tame regions exhibited by a range of topological logics in low-dimensional Euclidean spaces.
AIJ Journal 2010 Journal Article
We develop a formal framework for comparing different versions of ontologies, and apply it to ontologies formulated in terms of DL-Lite, a family of ‘lightweight’ description logics designed for data-intensive applications. The main feature of our approach is that we take into account the vocabulary ( = signature ) with respect to which one wants to compare ontologies. Five variants of difference and inseparability relations between ontologies are introduced and their respective applications for ontology development and maintenance discussed. These variants are obtained by generalising the notion of conservative extension from mathematical logic and by distinguishing between differences that can be observed among concept inclusions, answers to queries over ABoxes, by taking into account additional context ontologies, and by considering a model-theoretic, language-independent notion of difference. We compare these variants, study their meta-properties, determine the computational complexity of the corresponding reasoning tasks, and present decision algorithms. Moreover, we show that checking inseparability can be automated by means of encoding into QBF satisfiability and using off-the-shelf general purpose QBF solvers. Inseparability relations between ontologies are then used to develop a formal framework for (minimal) module extraction. We demonstrate that different types of minimal modules induced by these inseparability relations can be automatically extracted from real-world medium-size DL-Lite ontologies by composing the known tractable syntactic locality-based module extraction algorithm with our non-tractable extraction algorithms and using the multi-engine QBF solver aqme. Finally, we explore the relationship between uniform interpolation (or forgetting) and inseparability.
AAAI Conference 2010 Conference Paper
We design minimal temporal description logics that are capable of expressing various aspects of temporal conceptual data models and investigate their computational complexity. We show that, depending on the required types of temporal and atemporal constraints, the satisfiability problem for temporal knowledge bases in the resulting logics can be NLOGSPACE-, NP- and PSPACE-complete, as well as undecidable.
KR Conference 2010 Conference Paper
Databases and related information systems can benefit from the use of ontologies to enrich the data with general background knowledge. The DL-Lite family of ontology languages was specifically tailored towards such ontology-based data access, enabling an implementation in a relational database management system (RDBMS) based on a query rewriting approach. In this paper, we propose an alternative approach to implementing ontology-based data access in DL-Lite. The distinguishing feature of our approach is to allow rewriting of both the query and the data. We show that, in contrast to the existing approaches, no exponential blowup is produced by the rewritings. Based on experiments with a number of real-world ontologies, we demonstrate that query execution in the proposed approach is often more efficient than in existing approaches, especially for large ontologies. We also show how to seamlessly integrate the data rewriting step of our approach into an RDBMS using views (which solves the update problem) and make an interesting observation regarding the succinctness of queries in the original query rewriting approach.
IJCAI Conference 2009 Conference Paper
We present a formal framework for (minimal) module extraction based on an abstract notion of inseparability w. r. t. a signature between ontologies. Two instances of this framework are discussed in detail for DL-Lite ontologies: concept inseparability, when ontologies imply the same complex concept inclusions over the signature, and query inseparability, when they give the same answers to existential queries for any instance data over the signature. We demonstrate that different types of corresponding minimal modules for these inseparability relations can be automatically extracted from large-scale DL-Lite ontologies by composing the tractable syntactic locality-based module extraction algorithm with intractable extraction algorithms using the multi-engine QBF solver AQME. The extracted minimal modules are compared with those obtained using non-logic-based approaches.
LPAR Conference 2008 Conference Paper
Abstract We investigate the computational complexity of spatial logics extended with the means to represent topological connectedness and restrict the number of connected components. In particular, we show that the connectedness constraints can increase complexity from NP to PSpace, ExpTime and, if component counting is allowed, to NExpTime.
TIME Conference 2008 Invited Paper
We survey temporal description logics that are based on standard temporal logics such as LTL and CTL. In particular, we concentrate on the computational complexity of the satisfiability problem and algorithms for deciding it.
TIME Conference 2007 Conference Paper
It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of 'weak' description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable.
JELIA Conference 2006 Conference Paper
Abstract In this paper we compare two approaches to automated reasoning about metric and topology in the framework of the logic \(\mathcal{MT}\) introduced in [10]. \(\mathcal{MT}\) - formulas are built from set variablesp 1, p 2, .. . (for arbitrary subsets of a metric space) using the Booleans ∧, ∨, →, and ¬, the distance operators ∃ < a and ∃ ≤ a, for \(a\in {\mathbb Q}^{> 0}\), and the topological interior and closure operators I and C. Intended models for this logic are of the form \(\mathfrak I=(\Delta, d, p_{1}^{\mathfrak I}, p_{2}^{\mathfrak I}, \dots)\) where (Δ, d ) is a metric space and \(p_{i}^{\mathfrak I} \subseteq \Delta\). The extension \(\varphi^{\mathfrak I} \subseteq \Delta\) of an \(\mathcal{MT}\) -formula ϕ in \(\mathfrak I\) is defined inductively in the usual way, with I and C being interpreted as the interior and closure operators induced by the metric, and \((\exists^{<a}\varphi)^{\mathfrak I} = \{ x \in \Delta \mid \exists y\in \varphi^{\mathfrak I}\ d(x, y)<a \}\). In other words, \((\mathbf{I}\varphi)^{\mathfrak I}\) is the interior of \(\varphi^{\mathfrak I}\), \((\exists^{<a}\varphi)^{\mathfrak I}\) is the open a -neighbourhood of \(\varphi^{\mathfrak I}\), and \((\exists^{\le a}\varphi)^{\mathfrak I}\) is the closed one. A formula ϕ is satisfiable if there is a model \({\mathfrak I}\) such that \(\varphi^{\mathfrak I} \ne \emptyset\); ϕ is valid if ¬ ϕ is not satisfiable.
LPAR Conference 2005 Conference Paper
Abstract The notion of comparative similarity ‘ X is more similar or closer to Y than to Z ’ has been investigated in both foundational and applied areas of knowledge representation and reasoning, e. g. , in concept formation, similarity-based reasoning and areas of bioinformatics such as protein sequence alignment. In this paper we analyse the computational behaviour of the ‘propositional’ logic with the binary operator ‘closer to a set τ 1 than to a set τ 2 ’ and nominals interpreted over various classes of distance (or similarity) spaces. In particular, using a reduction to the emptiness problem for certain tree automata, we show that the satisfiability problem for this logic is ExpTime-complete for the classes of all finite symmetric and all finite (possibly non-symmetric) distance spaces. For finite subspaces of the real line (and higher dimensional Euclidean spaces) we prove the undecidability of satisfiability by a reduction of the solvability problem for Diophantine equations. As our ‘closer’ operator has the same expressive power as the standard operator > of conditional logic, these results may have interesting implications for conditional logic as well.
AIJ Journal 2004 Journal Article
Combining knowledge representation and reasoning formalisms is an important and challenging task. It is important because non-trivial AI applications often comprise different aspects of the world, thus requiring suitable combinations of available formalisms modeling each of these aspects. It is challenging because the computational behavior of the resulting hybrids is often much worse than the behavior of their components. In this paper, we propose a new combination method which is computationally robust in the sense that the combination of decidable formalisms is again decidable, and which, nonetheless, allows non-trivial interactions between the combined components. The new method, called E -connection, is defined in terms of abstract description systems (ADSs), a common generalization of description logics, many logics of time and space, as well as modal and epistemic logics. The basic idea of E -connections is that the interpretation domains of n combined systems are disjoint, and that these domains are connected by means of n-ary ‘link relations’. We define several natural variants of E -connections and study in-depth the transfer of decidability from the component systems to their E -connections.
TIME Conference 2003 Conference Paper
We study the complexity of some fragments of first-order temporal logic over natural numbers time. The one-variable fragment of linear first-order temporal logic even with sole temporal operator /spl square/ is EXPSPACE-complete (this solves an open problem of J. Halpern and M. Vardi (1989)). So are the one-variable, two-variable and monadic monodic fragments with Until and Since. If we add the operators O/sup n/, with n given in binary, the fragment becomes 2EXPSPACE-complete. The packed monodic fragment has the same complexity as its pure first-order part - 2EXPTIME-complete. Over any class of flows of time containing one with an infinite ascending sequence - e. g. , rationals and real numbers time, and arbitrary strict linear orders - we obtain EXPSPACE lower bounds (which solves an open problem of M. Reynolds (1997)). Our results continue to hold if we restrict to models with finite first-order domains.
IJCAI Conference 2003 Conference Paper
The paper presents a novel expressive logic-based formalism intended for reasoning about numerical distances. We investigate its computational properties (in particular, show that it is EXPTIMEcomplete) and devise a tableau-based satisfiabilitychecking algorithm. To be able to express knowledge about implicit or unknown distances, we then extend the language with variables ranging over distances and prove that the resulting logic is decidable as well.
JELIA Conference 2002 Conference Paper
Abstract This paper introduces a new logical formalism, intended for temporal conceptual modelling, as a natural combination of the well-known description logic \( \mathcal{D}\mathcal{L}\mathcal{R} \) and point-based linear temporal logic with Since and Until. We define a query language (where queries are non-recursive Datalog programs and atoms are complex \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) expressions) and investigate the problem of checking query containment under the constraints defined by \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) conceptual schemas—i. e. , \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) knowledge bases—as well as the problems of schema satisfiability and logical implication.
KR Conference 2002 Conference Paper
TIME Conference 2002 Conference Paper
We prove decidability of 'non local' propositional CTL*, where truth values of atoms may depend on the branch of evaluation. This result is then used to show decidability of the 'weak' one-variable fragment of first-order (local) CTL*, in which all temporal operators and path quantifiers except 'tomorrow' are applicable only to sentences. Various spatio-temporal logics based on combinations of CTL* and RCC-8 can be embedded into this fragment, and so are decidable.
LPAR Conference 2001 Invited Paper
Abstract The aim of this paper is to summarize and analyze some results obtained in 2000–2001 about decidable and undecidable fragments of various first-order temporal logics, give some applications in the field of knowledge representation and reasoning, and attract the attention of the ‘temporal community’ to a number of interesting open problems.
JELIA Conference 2000 Conference Paper
Abstract We consider the monodic formulas of common knowledge predicate logic, which allow applications of epistemic operators to formulas with at most one free variable. We provide finite axiomatizations of the monodic fragment of the most important common knowledge predicate logics (the full logics are known to be not recursively enumerable) and single out a number of their decidable fragments. On the other hand, it is proved that the addition of the equality symbol to the monodic fragment makes it not recursively enumerable.
JELIA Conference 2000 Invited Paper
Abstract We introduce a family of languages intended for representing knowledge and reasoning about metric (and more general distance) spaces. While the simplest language can speak only about distances between individual objects and Boolean relations between sets, the more expressive ones are capable of capturing notions such as ‘somewhere in (or somewhere out of) the sphere of a certain radius’, ‘everywhere in a certain ring’, etc. The computational complexity of the satisfiability problem for formulas in our languages ranges from NP-completeness to undecidability and depends on the class of distance spaces in which they are interpreted. Besides the class of all metric spaces, we consider, for example, the spaces ℝ × ℝ and ℕ × ℕ with their natural metrics.
ECAI Conference 2000 Conference Paper
IJCAI Conference 1999 Conference Paper
In this paper, we construct a new concept description language intended for representing dynamic and intensional knowledge. The most important feature distinguishing this language from its predecessors in the literature is that it allows applications of modal operators to all kinds of syntactic terms: concepts, roles and formulas. Moreover, the language may contain both local (i. e. , state-dependent) and global (i. e. , state-independent) concepts, roles and ob jects. All this provides us with the most com plete and natural means for reflecting the dy namic and intensional behaviour of application domains. We construct a satisfiability check ing (mosaic-type) algorithm for this language (based on in (i) arbitrary multimodal frames, (ii) frames with universal accessibility relations (for knowledge) and (iii) frames with transitive, symmetrical and euclidean relations (for beliefs). On the other hand, it is shown that the satisfaction problem becomes undecidable if the underlying frames are arbitrary linear orders or the language contains the com mon knowledge operator for 2 agents.