# 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.

## Key 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.