Unification in the normal modal logic Alt1

ABSTRACT. In the ordinary modal language, the normal modal logic Alt1 is the least normal logic containing the formula <>x->[]x. It can also be defined as the normal modal logic determined by the class of all deterministic frames. The unification problem in Alt1 is to determine, given a formula F(x1,...,xn), whether there exists formulas G1,...,Gn such that F(G1,...,Gn) is in Alt1. We demonstrate that the unification problem in Alt1 is decidable in polynomial space.