hide
Free keywords:
-
Abstract:
In this paper we analyze some fragments of the universal theory
of distributive lattices with many sorted bridging operators.
Our interest in such algebras
is motivated by the fact that, in description logics,
numerical features are often expressed by using maps that
associate numerical values to sets (more generally,
to lattice elements).
We first establish a link between satisfiability
of universal sentences
with respect to algebraic models and satisfiability with respect to
certain classes of relational structures.
We use these results for giving a method for
translation to clause form of universal sentences,
and provide some decidability results based on the use of
resolution or hyperresolution.
Links between hyperresolution and tableau methods are also
discussed, and a tableau procedure for checking satisfiability
of formulae of type $t_1 \leq t_2$ is obtained by using a
hyperresolution calculus.