Finite materialisability of Datalog programs with metric temporal operators
<p>DatalogMTL is an extension of Datalog with metric temporal operators that has recently found applications in stream reasoning and temporal ontology-based data access. In contrast to plain Datalog, where materialisation (a.k.a. forward chaining) naturally terminates in finitely many steps, r...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Sprog: | English |
| Udgivet: |
AI Access Foundation
2023
|
| _version_ | 1826309392485580800 |
|---|---|
| author | Wałęga, PA Zawidzki, M Cuenca Grau, B |
| author_facet | Wałęga, PA Zawidzki, M Cuenca Grau, B |
| author_sort | Wałęga, PA |
| collection | OXFORD |
| description | <p>DatalogMTL is an extension of Datalog with metric temporal operators that has recently found applications in stream reasoning and temporal ontology-based data access. In contrast to plain Datalog, where materialisation (a.k.a. forward chaining) naturally terminates in finitely many steps, reaching a fixpoint in DatalogMTL may require infinitely many rounds of rule applications. As a result, existing reasoning systems resort to other approaches, such as constructing large Büchi automata, whose implementations turn out to be highly inefficient in practice.</p>
<p>In this paper, we propose and study finitely materialisable DatalogMTL programs, for which forward chaining reasoning is guaranteed to terminate. We consider a data-dependent notion of finite materialisability of a program, where termination is guaranteed for a given dataset, as well as a data-independent notion, where termination is guaranteed regardless of the dataset. We show that, for bounded programs (a natural DatalogMTL fragment for which reasoning is as hard as in the full language), checking data-dependent finite materialisability is ExpSpace-complete in combined complexity and PSpace-complete in data complexity; furthermore, we propose a practical materialisation-based decision procedure that works in doubly exponential time. We show that checking data-independent finite materialisability for bounded progams is computationally easier, namely ExpTime-complete; moreover, we propose sufficient conditions for data-indenpendent finite materialisability that can be efficiently checked. We provide also the complexity landscape of fact entailment for different classes of finitely materialisable programs; surprisingly, we could identify a large class of finitely materialisable programs, called MTL-acyclic programs, for which fact entailment has exactly the same data and combined complexity as in plain Datalog, which makes this fragment especially well suited for big-scale applications.</p> |
| first_indexed | 2024-03-07T07:33:29Z |
| format | Journal article |
| id | oxford-uuid:7f7f8e0d-016e-4b9e-bd1a-1d943b0df4c4 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:33:29Z |
| publishDate | 2023 |
| publisher | AI Access Foundation |
| record_format | dspace |
| spelling | oxford-uuid:7f7f8e0d-016e-4b9e-bd1a-1d943b0df4c42023-02-16T09:50:58ZFinite materialisability of Datalog programs with metric temporal operatorsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:7f7f8e0d-016e-4b9e-bd1a-1d943b0df4c4EnglishSymplectic ElementsAI Access Foundation2023Wałęga, PAZawidzki, MCuenca Grau, B<p>DatalogMTL is an extension of Datalog with metric temporal operators that has recently found applications in stream reasoning and temporal ontology-based data access. In contrast to plain Datalog, where materialisation (a.k.a. forward chaining) naturally terminates in finitely many steps, reaching a fixpoint in DatalogMTL may require infinitely many rounds of rule applications. As a result, existing reasoning systems resort to other approaches, such as constructing large Büchi automata, whose implementations turn out to be highly inefficient in practice.</p> <p>In this paper, we propose and study finitely materialisable DatalogMTL programs, for which forward chaining reasoning is guaranteed to terminate. We consider a data-dependent notion of finite materialisability of a program, where termination is guaranteed for a given dataset, as well as a data-independent notion, where termination is guaranteed regardless of the dataset. We show that, for bounded programs (a natural DatalogMTL fragment for which reasoning is as hard as in the full language), checking data-dependent finite materialisability is ExpSpace-complete in combined complexity and PSpace-complete in data complexity; furthermore, we propose a practical materialisation-based decision procedure that works in doubly exponential time. We show that checking data-independent finite materialisability for bounded progams is computationally easier, namely ExpTime-complete; moreover, we propose sufficient conditions for data-indenpendent finite materialisability that can be efficiently checked. We provide also the complexity landscape of fact entailment for different classes of finitely materialisable programs; surprisingly, we could identify a large class of finitely materialisable programs, called MTL-acyclic programs, for which fact entailment has exactly the same data and combined complexity as in plain Datalog, which makes this fragment especially well suited for big-scale applications.</p> |
| spellingShingle | Wałęga, PA Zawidzki, M Cuenca Grau, B Finite materialisability of Datalog programs with metric temporal operators |
| title | Finite materialisability of Datalog programs with metric temporal operators |
| title_full | Finite materialisability of Datalog programs with metric temporal operators |
| title_fullStr | Finite materialisability of Datalog programs with metric temporal operators |
| title_full_unstemmed | Finite materialisability of Datalog programs with metric temporal operators |
| title_short | Finite materialisability of Datalog programs with metric temporal operators |
| title_sort | finite materialisability of datalog programs with metric temporal operators |
| work_keys_str_mv | AT wałegapa finitematerialisabilityofdatalogprogramswithmetrictemporaloperators AT zawidzkim finitematerialisabilityofdatalogprogramswithmetrictemporaloperators AT cuencagraub finitematerialisabilityofdatalogprogramswithmetrictemporaloperators |