Filtering unification and most general unifiers in modal logic. (English) Zbl 1069.03011

The paper introduces a syntactic and an algebraic characterization of the normal K\(4\) logics for which unification in an equational theory \(E\) is filtering (given two solutions to a unification problem, there is always another one which is more general than both of them). Firstly, it is proved that filtering unification in modal logic is characterized by the fact that finitely presented projective algebras are closed under binary products. Then, the case of normal extensions \(L\) of K\(4\) is studied, showing that \(L\) has filtering unification if and only if it extends the logic K\(4.2^+\) obtained from K\(4\) by adding to it the modal translation of the weak excluded middle principle. In the rest of the paper, the authors prove that unification is indeed unitary in K\(4.2^+\), and also in all extensions of it having the finite-model property and the 2-glueing property (this is a property of the finite frames, roughly saying that such frames are closed under disjoint union, adding a new root and identifying final clusters).


03B45 Modal logic (including the logic of norms)
03B35 Mechanization of proofs and logical operations
03G25 Other algebras related to logic
Full Text: DOI


[1] Algebra i Logika 18 pp 328– (1979)
[2] DOI: 10.1023/A:1005843212881 · Zbl 0883.06011
[3] Topology (1984)
[4] Logics containing K4. Part I 31 pp 31– (1974)
[5] Introduction to lattices and order (1990)
[6] Modal logic (1997) · Zbl 0871.03007
[7] Handbook of categorical algebra 3 (1994)
[8] Distributive lattices (1974) · Zbl 0321.06012
[9] Handbook of Automated Reasoning I pp 445– (2001)
[10] DOI: 10.1007/BF01195536 · Zbl 0853.03008
[11] DOI: 10.1006/jsco.2000.0426 · Zbl 0970.68166
[12] DOI: 10.1016/S0747-7171(89)80055-0 · Zbl 0689.68039
[13] Computer Science Logic 03 pp 255– (2003)
[14] Reports on Mathematical Logic 7 pp 21– (1976)
[15] Reports on Mathematical Logic 6 pp 41– (1976)
[16] DOI: 10.1016/j.apal.2003.11.010 · Zbl 1058.03020
[17] Sheaves, Games and Modal Completions (2002)
[18] Logic Journal of the IGPL. Interest Group in Pure and Applied Logics 10 pp 229– (2002)
[19] DOI: 10.1016/S0168-0072(99)00032-9 · Zbl 0949.03010
[20] Unification in intuitionistic logic 64 pp 859– (1999) · Zbl 0930.03009
[21] DOI: 10.1093/logcom/7.6.733 · Zbl 0894.08004
[22] Logics containing K4. Part II 31 pp 619– (1985)
[23] DOI: 10.1016/0168-0072(88)90021-8 · Zbl 0643.03014
[24] An algebraic approach to non-classical logics (1974) · Zbl 0299.02069
[25] DOI: 10.1007/3-540-52885-7_118
[26] Handbook of Automated Reasoning I pp 371– (2001)
[27] Categories for the working mathematician (1971) · Zbl 0232.18001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.