Undecidability of the unification and admissibility problems for modal and description logics

Frank Wolter, Michael Zakharyaschev

We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extende…