Finite-Model Reasoning for Graph Queries and Description Logics
摘要
The task of query entailment consists in determining if a given query holds in every extension of a given structure that satisfies a given set of constraints. In knowledge representation, traditionally, this includes both finite and infinite extensions. In many contexts, however, it is desirable to consider only finite extensions. In this tutorial we present a handful of techniques that can be used to move from the unrestricted to the finite case. We illustrate these techniques by proving a series of decidability results for various classes of queries, ultimately arriving at unions of conjunctive regular path queries, which are the theoretical core of practical graph query languages. For the constraint language we use description logics, which are popular ontology formalisms used in knowledge representation and are capable of expressing most constraints relevant in graph databases. The methods we discuss are applicable to various description logics, but for the simplicity of the exposition we work with the basic logic \(\mathcal {ALC} \) .