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 satisfiability and querying in fragments of first-order logic. Description logics play a central role in these considerations: On the one hand, they can serve as a simplified “testbed” inspiring decidability criteria which can then be generalized to higher arities. On the other hand, they mark a “sweet spot,” highlighting the fact that restricting to a binary setting allows for adding modeling features that would otherwise cause undecidability.

Back to Program