Finite model reasoning over existential rules

TL;DR

This paper proves that finite controllability holds for all basic decidable Datalog+/- ontology fragments, including shy, by developing a general technique for establishing finite controllability.

Contribution

It extends finite controllability results to shy ontologies and introduces a general method for proving finite controllability of any ontological fragment.

Findings

Finite controllability holds for shy ontologies.

A new general technique for (dis)proving finite controllability.

Completes the understanding of finite controllability across all basic Datalog+/- classes.

Abstract

Ontology-based query answering (OBQA) asks whether a Boolean conjunctive query is satisfied by all models of a logical theory consisting of a relational database paired with an ontology. The introduction of existential rules (i.e., Datalog rules extended with existential quantifiers in rule-heads) as a means to specify the ontology gave birth to Datalog+/-, a framework that has received increasing attention in the last decade, with focus also on decidability and finite controllability to support effective reasoning. Five basic decidable fragments have been singled out: linear, weakly-acyclic, guarded, sticky, and shy. Moreover, for all these fragments, except shy, the important property of finite controllability has been proved, ensuring that a query is satisfied by all models of the theory iff it is satisfied by all its finite models. In this paper we complete the picture by demonstrating that finite controllability of OBQA holds also for shy ontologies, and it therefore applies to all basic decidable Datalog+/- classes. To make the demonstration, we devise a general technique to facilitate the process of (dis)proving finite controllability of an arbitrary ontological fragment. This paper is under consideration for acceptance in TPLP.