Ghilardi, Silvio Best solving modal equations. (English) Zbl 0949.03010 Ann. Pure Appl. Logic 102, No. 3, 183-198 (2000). 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’) Cited in 5 ReviewsCited in 46 Documents MSC: 03B35 Mechanization of proofs and logical operations 03B45 Modal logic (including the logic of norms) 03G25 Other algebras related to logic 08B20 Free algebras Keywords:modal logic; \(E\)-unification; equations in free algebras PDFBibTeX XMLCite \textit{S. Ghilardi}, Ann. Pure Appl. Logic 102, No. 3, 183--198 (2000; Zbl 0949.03010) Full Text: DOI References: [1] Baader, F.; Siekmann, J. H., Unification theory, (Gabbay, D. M.; Hogger, C. J.; Robinson, J. A., Handbook of Logic in Artificial Intelligence and Logic Programming (1993), Oxford University Press: Oxford University Press Oxford), 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.; 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.; 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.; 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.; 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.