Relative similarity logics are decidable: Reduction to FO2 with equality

Abstract

We show the decidability of the satisfiability problem for relative similarity logics that allow classification of objects in presence of incomplete information. As a side-effect, we obtain a finite model property for such similarity logics. The proof technique consists of reductions into the satisfiability problem for the decidable fragment FO2 with equality from classical logic. Although the reductions stem from the standard translation from modal logic into classical logic, our original approach (for instance handling nominals for atomic properties and decomposition in terms of components encoded in the reduction) can be generalized to a larger class of relative logics, opening ground for further investigations.