Abstract:
The unification problem in a propositional logic is to determine, given a formula phi, whether there exists a substitution sigma such that sigma(phi) is in that logic. In that case, sigma is a unifier of phi. When a unifiable formula has minimal complete sets of unifiers, it is either infinitary, finitary, or unitary, depending on the cardinality of its minimal complete sets of unifiers. Otherwise, it is nullary. In this paper, we prove that in modal logic K+square square perpendicular to, unifiable formulas are either finitary, or unitary.
