Unification in some polymodal logics
by
Wojciech Dzik
Institute of Mathematics, Silesian University, Katowice, Poland

Unification type can be unitary (best: every unifiable formula has a most general unifier), finitary, infinitary or nullary (some unifiable formulas have no maximal unifiers). We show that usually unitary unification is not preserved under the fusion of uni-modal logics but often it is preserved under the Cartesian product. In particular, unification in the fusion S4.2 ⊕...⊕S4.2 is not unitary.
Let L be a k-transitive polymodal logic. Then: (i) if \Diamond^k \square^k x → \square^k \Diamond^k x (k-confluence) is in L, then unification in L is either unitary or nullary (a generalization to polymodal case of a part of the Ghilardi-Sacchetti result); (ii) if L has conjugate modal operators, then unification in L is unitary. In particular, unification in the product of uni-modal logics containing S4.2 is either unitary or nullary.
We provide examples of applied polymodal logics with unitary unification: Data Analysis logic with Local Agreement, DALLA, of S.Demri and E.Orlowska, and Multiagent Knowledge logics of hypercubes (of A.Lomuscio and M.Ryan). The unification problem is decidable for these logics (while F.Wolter and M. Zakharyaschev proved undecidability of this problem for K and K4 extended with the universal modality).
Apart from Boolean cases, we show that some k-potent hoops with dual normal operators, investigated by Blok and Pigozzi (as a generalization of the Jónsson and Tarski treatment of BAO's), have unitary unification.

PDF

Date received: May 14, 2007