Decidability of inferencing is commonly considered a very important property
of logic-based knowledge representation formalisms, required for the
algorithmization and automation of reasoning. Yet, oftentimes, the
corresponding (un)decidability arguments are idiosyncratic and do not shed
much light on the underlying principles governing the divide.
In my talk, I will review generic model- and proof-theoretic criteria for
decidability of querying in fragments of first-order logic. Description
logics play a central role in these considerations: They can serve as a
simplified “testbed” inspiring decidability criteria which can then be
generalized to higher arities.
On the model-theoretic side, I will describe a general framework by means of
which decidability of query entailment can be established based on the
existence of countermodels with certain structural properties. These
properties depend on the ontology and query language used and range from
finite domain over forest-like shape to width-finiteness employing width
notions like treewidth and cliquewidth.
On the proof-theoretic side, I will report on a recent result according to
which decidable homomorphism-closed queries can be captured by a rather
restricted ontology-mediated querying framework based on existential rules
with certain chase termination guarantees.
Back to Program