6533b852fe1ef96bd12aa486

RESEARCH PRODUCT

Finitary unification in locally tabular modal logics characterized

Wojciech DzikSławomir KostPiotr Wojtylak

subject

Locally tabular logicUnification typesLogicUnificationModal logicKripke model

description

We provide necessary and sufficient conditions for finitary unification in locally tabular modal logics, solely in terms of Kripke models. We apply the conditions to establish the unification types of logics determined by simple finite frames. In particular, we show that unification is finitary (or unitary) in the logic determined by the fork (frame F4, see Fig. 6), the rhombus (frame F5), inGL.3m,GrzBd2,S4Bd2and other logics; whereas it is nullary in the logic of F6, and of the pentagon FN5. In Appendix analogous results are given for superintuitionistic logics.

yearjournalcountryeditionlanguage
2022-04-01Annals of Pure and Applied Logic
10.1016/j.apal.2021.103072https://www.sciencedirect.com/science/article/pii/S0168007221001305?dgcid=rss_sd_all