A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation .

We present a first result towards the use of entailment in- side relationaldual tableau-based decision procedures. To this end, we introduce a fragment ofRL(1) which admits a restricted form of composition, (R ; S) or (R ; 1), wherethe left subterm R of (R ; S) is only allowed to be either the constant 1, or aBoolean 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 relationalvariables and the operators of intersection and of union. We prove thedecidability of the fragment by defining a dual tableau- based decisionprocedure with a suitable blocking mechanism and where the rules to decomposecompositional formulae are modified so to deal with the constant 1 whilepreserving termination. The fragment properly includes the logics presented inprevious work and, therefore, it allows one to express, among others, themulti-modal logic K with union and intersection of accessibility relations, andthe description logic ALC with union and intersection of roles.