Reasoning with the Core Chase: the Case of SHACL Validation over ELHI Knowledge Bases

Abstract

Many approaches to query answering in Description Logics (DLs) adopt the certain answer semantics, which is natural for standard query languages without negation, but falls short when negation is involved. Since negation plays a crucial role in many applications, alternative semantics are needed. Core universal models are increasingly accepted as a means to give a semantics to queries with negation. In this paper, we consider the problem of evaluating (possibly recursive) SHACL expressions over the core universal model of an ℰℒℋℐ KB. SHACL, recently proposed as a standard constraint language for RDF data, is a natural and powerful query language, and the fragment we consider adds regular path navigation to semi-positive monadic Datalog with acyclic rule bodies. We first propose a construction of a finite representation of the core universal model, based on a novel calculus for ℰℒℋℐ that gives up the data-independence to avoid the best-case exponential behaviour of similar approaches, and which we believe can lead towards an efficient implementation. Then we leverage this finite representation to reduce validation in the presence of ontologies to plain SHACL validation, similarly to previous algorithms but avoiding their best-case exponential behaviour. Our algorithms yield tight data- and combined-complexity bounds for the studied SHACL validation problem, which coincide with plain consistency testing in ℰℒℋℐ.