Dual Tableau-based Decision Procedures for Some Relational Logics.

Abstract

We consider fragments of the relational logic RL(1) obtained by imposing some constraints on the relational terms involving relations composition. Such fragments allow to express several non classical logics such as the multi-modal logic K and the description logic ALC with union and intersection of roles. We show how relational dual tableaux can be employed to define decision procedures for each of them.