A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation (Extended Version)

TL;DR

This paper introduces a new decidable fragment of relational logic with a dual tableau decision procedure, enabling reasoning about complex relational structures including multi-modal and description logics.

Contribution

It defines a novel fragment of RL(1) with restricted composition, proves its decidability using a dual tableau method with blocking, and extends previous work to include more expressive logics.

Findings

Decidability of the new fragment established.

The tableau procedure handles composition with constant 1.

Includes expressive logics like multi-modal K and ALC.

Abstract

We present a first result towards the use of entailment in- side relational dual tableau-based decision procedures. To this end, we introduce a fragment of RL(1) which admits a restricted form of composition, (R ; S) or (R ; 1), where the left subterm R of (R ; S) is only allowed to be either the constant 1, or a Boolean term neither containing the complement operator nor the constant 1, while in the case of (R ; 1), R can only be a Boolean term involving relational variables and the operators of intersection and of union. We prove the decidability of the fragment by defining a dual tableau- based decision procedure with a suitable blocking mechanism and where the rules to decompose compositional formulae are modified so to deal with the constant 1 while preserving termination. The fragment properly includes the logics presented in previous work and, therefore, it allows one to express, among others, the multi-modal logic K with union and intersection of accessibility relations, and the description logic ALC with union and intersection of roles.