First-order rewritability of ontology-mediated queries in linear temporal logic
Autor: | Vladislav Ryzhikov, Alessandro Artale, Michael Zakharyaschev, Frank Wolter, Roman Kontchakov, Alisa Kovtunova |
---|---|
Jazyk: | angličtina |
Rok vydání: | 2021 |
Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Linguistics and Language Hierarchy Theoretical computer science csis Computer science 02 engineering and technology Ontology (information science) Language and Linguistics Temporal database Logic in Computer Science (cs.LO) Monotone polygon TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Description logic Linear temporal logic Artificial Intelligence 020204 information systems Computer Science::Logic in Computer Science Core (graph theory) 0202 electrical engineering electronic engineering information engineering Primitive recursive function 020201 artificial intelligence & image processing Circuit complexity |
Zdroj: | Artificial Intelligence |
ISSN: | 0004-3702 |
Popis: | 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 and, respectively, . 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. |
Databáze: | OpenAIRE |
Externí odkaz: |