Best solving modal equations. (English) Zbl 0949.03010

Classical propositional calculus enjoys the following property: for every formula \(A\), if there is a substitution \(\sigma\), such that \(\sigma(A)\) is provable, then there is “the best” substitution with this property. But for other logical calculi, for some modal calculi in particular, this property is not valid.
However in many systems, like K4, S4, S4Grz, GL, etc., there are finitely many “best substitutions” for any formula admitting at least a unifier. In other words if an equation is solvable in the free algebra, then there are finitely many “best solutions”.
The author shows that such solutions can be effectively computed.
Reviewer: N.Zamov (Kazan’)


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


[1] Baader, F.; Siekmann, J.H., Unification theory, (), 41-125
[2] Fine, K., Logics containing K4, part I, J. symbolic logic, 34, 31-42, (1974) · Zbl 0287.02010
[3] Fine, K., Logics containing K4, part II, J. symbolic logic, 50, 619-651, (1985) · Zbl 0574.03008
[4] Ghilardi, S., Unification through projectivity, J. logic comput., 7, 6, 733-752, (1997) · Zbl 0894.08004
[5] Ghilardi, S., Unification in intuitionistic logic, J. symbolic logic, 69, 859-880, (1999) · Zbl 0930.03009
[6] S. Ghilardi, A resolution/tableaux algorithm for projective approximations in IPC, preprint 1998. · Zbl 1005.03504
[7] G.E. Hughes, M.J. Cresswell, A Companion to Modal Logic, Methuen, London, 1984. · Zbl 0625.03005
[8] Maksimova, L.L., A classification of modal logics, Algebra i logika, 18, 3, 328-340, (1979)
[9] U. Martin, T. Nipkow, Boolean unification – the story so far, J. Symbolic Comput. 7 1988, pp. 275-293. · Zbl 0682.68093
[10] H.J. Ohlbach, A resolution calculus for modal logic, Proceedings of the CADE, Lecture Notes in Computer Science, Springer, Berlin, 1988, pp. 500-516.
[11] Ohlbach, H.J., Semantics-based translation methods for modal logics, J. logic comput., 1, 5, 691-746, (1991) · Zbl 0746.03010
[12] Rybakov, V.V., Problems of substitution and admissibility in the modal system \(Grz\) and in intuitionistic propositional calculus, Ann. pure appl. logic, 50, 71-106, (1990) · Zbl 0709.03009
[13] Siekmann, J., Unification theory, J. symbolic comput., 7, 207-274, (1989) · Zbl 0678.68098
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.