Best solving modal equations (Q1971794)

Classical propositional calculus enjoys the following property: for every formula \(A\), if there is a substitution \(\sigma\), such that \(\sigma(A)\) is provable, then there is ``the best'' substitution with this property. But for other logical calculi, for some modal calculi in particular, this property is not valid. However in many systems, like K4, S4, S4Grz, GL, etc., there are finitely many ``best substitutions'' for any formula admitting at least a unifier. In other words if an equation is solvable in the free algebra, then there are finitely many ``best solutions''. The author shows that such solutions can be effectively computed.