A Syntactic Approach to Unification in Transitive Reflexive Modal Logics
Rosalie Iemhoff · Notre Dame Journal of Formal Logic · 2016
This paper contains a proof-theoretic account of unification in transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are presented and these results are extended to negationless fragments. In particular, a syntactic proof of Ghilardi’s result that S4 has finitary unification is provided. In this approach the relation between classical valuations, projective unifiers, and admissible rules is clarified.