×

Best unifiers in transitive modal logics. (English) Zbl 1247.03029

The paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4.
There are two views on the origin of the term “unification”, though both views are very close to each other. Logical unification is the problem to solve whether, for two given formulas, there is a substitution, which makes these formulas equivalent. Unification in computer science is the problem of making two given terms semantically equal. In most cases the problem of term unification directly coincides with its logical unification counterpart.
The unification problem is in fact a particular case of a more complicated problem: the substitution problem. That is, the problem whether a formula can be made a theorem after replacing some of the variables by formulas.
Ghilardi studied unification in propositional modal logics with the aim of describing all possible unifiers. His approach is very useful in dealing with admissibility. In fact, when a computable finite set of best unifiers is constructed, a solution of the admissibility problem follows immediately. The results of Ghilardi on unification gave a computational ground to construct all unifiers. These techniques turned out to be effective tools to work with various problems.
In this paper the author answers positively to the following question: do his previous algorithms for deciding admissibility of inference rules work for the computation of best unifiers in modal transitive logics?
Reviewer: Nail Zamov (Kazan)

MSC:

03B45 Modal logic (including the logic of norms)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader F., Siekmann J.H.: ’Unification theory’. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds) Handbook of Logic in Artificial Intelligence and Logic Programming., pp. 41–125. Oxford University Press, Oxford (1994)
[2] Baader, F., and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998. · Zbl 0948.68098
[3] Baader, F., and R. Küsters, Unification in a Description Logic with Transitive Closure of Roles. LPAR 2001, pp. 217–232. · Zbl 1275.68134
[4] Baader F., Narendran P.: ’Unification of Concept Terms in Description Logics’. J. Symb. Comput. 31(3), 277–305 (2001) · Zbl 0970.68166 · doi:10.1006/jsco.2000.0426
[5] Baader, F., and W. Snyder, ’Unification Theory’. In J. A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, volume I. Elsevier Science Publishers, 2001, pp. 447–533. · Zbl 1011.68126
[6] Baader, F., D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider (eds.), The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. · Zbl 1058.68107
[7] Baader F., Morawska B.: ’Unification in the Description Logic EL’. Logical Methods in Computer Science 6(3), 1–31 (2010) · Zbl 1214.68379 · doi:10.2168/LMCS-6(3:17)2010
[8] Baader, F., and S. Ghilardy, ’Unification in modal and description logics’. Logic J. of IGPL 2010, doi: 10.1093/jigpal/jzq008 , First published online: April 29, 2010.
[9] Babenyshev, S., and V. Rybakov, ’Linear Temporal Logic LTL: Basis for Admissible Rules’, J. Logic Computation 2010, doi: 10.1093/logcom/exq020,21 . · Zbl 1233.03026
[10] Babenyshev, S., and V. Rybakov, ’Unification in Linear Temporal Logic LTL’, 2010, submitted. · Zbl 1241.03014
[11] Babenyshev, S., V. Vladimir, R. Schmidt, and D. Tishkovsky. ’A tableau method for checking rule admissibility in S4’. In Proc. of the 6th Workshop on Methods for Modalities (M4M-6), Copenhagen, 2009. · Zbl 1345.03033
[12] Blackburn, P., J. van Benthem, and F. Wolter (eds.), The Handbook of Modal Logic. Elsevier, 2006. · Zbl 1114.03001
[13] Gabbay D., Reyle U.: ’N-Prolog: - An extension of Prolog with hypothetical implications’. Journal of Logic Programming 1, 391–355 (1984) · Zbl 0576.68001
[14] Ghilardi S.: ’Unification Through Projectivity’. J. Log. Comput. 7(6), 733–752 (1997) · Zbl 0894.08004 · doi:10.1093/logcom/7.6.733
[15] Ghilardi S.: ’Unificationinintuitionisticlogic’. J.Symb. Log. 64(2), 859–880 (1999) · Zbl 0930.03009 · doi:10.2307/2586506
[16] Ghilardi S.: ’Best solving modal equations’. Ann. Pure Appl. Logic 102(3), 183–198 (2000) · Zbl 0949.03010 · doi:10.1016/S0168-0072(99)00032-9
[17] Ghilardi S.: ’Unification, finite duality and projectivity in varieties of Heyting algebras’. Ann. Pure Appl. Logic 127(1–3), 99–115 (2004) · Zbl 1058.03020 · doi:10.1016/j.apal.2003.11.010
[18] Iemhoff R.: ’On the admissible rules of intuitionistic propositional logic’. J. Symb. Log. 66(1), 281–294 (2001) · Zbl 0986.03013 · doi:10.2307/2694922
[19] Iemhoff R.: ’On The Admissible Rules of Intuitionistic Propositional Logic’. J. Symb. Log. 66(1), 281–294 (2001) · Zbl 0986.03013 · doi:10.2307/2694922
[20] Iemhoff, R., Towards a Proof System for Admissibility. CSL 2003, pp. 255–270. · Zbl 1116.03304
[21] Iemhoff R., Metcalfe G.: ’Proof theory for admissible rules’. Ann. Pure Appl. Logic 159(1–2), 171–186 (2009) · Zbl 1174.03024 · doi:10.1016/j.apal.2008.10.011
[22] Jerabek E.: ’Admissible rules of modal logics’. Journal of Logic and Computation 15(4), 411–431 (2005) · Zbl 1077.03011 · doi:10.1093/logcom/exi029
[23] Jerabek E.: ’Independent bases of admissible rules’. Logic Journal of the IGPL 16(3), 249–267 (2008) · Zbl 1146.03008 · doi:10.1093/jigpal/jzn004
[24] Jerabek E.: ’Admissible rules of Lukasiewicz logic’. Journal of Logic and Computation 20(2), 425–447 (2010) · Zbl 1216.03042 · doi:10.1093/logcom/exp078
[25] Knuth D. E., Bendix P. B.: ’Simple word problems in universal algebras’. In: Leech, J. (ed) Computational Problems in Abstract Algebra., Pergamon Press, Oxford (1970) · Zbl 0188.04902
[26] Kröger, F., and S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer Science. An EATCS Series, Springer, Berlin Heidelberg, 2008. · Zbl 1169.03001
[27] Levy, J., and M. Villaret, Nominal Unification from a Higher-Order Perspective. RTA 2008, pp. 246–260. · Zbl 1145.03311
[28] Oliart A., Snyder W.: ’Fast algorithms for uniform semi-unification’. J. Symb. Comput. 37(4), 455–484 (2004) · Zbl 1137.68630 · doi:10.1016/j.jsc.2003.03.002
[29] Robinson J. A.: ’A machine oriented logic based on the resolution principle. J. of the ACM 12(1), 23–41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[30] Rybakov V.V.: ’A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic’. Algebra and Logica 23(5), 369–384 (1984) · Zbl 0598.03013 · doi:10.1007/BF01982031
[31] Rybakov V.V.: ’Problems of Substitution and Admissibility in the Modal System Grz and in Intuitionistic Propositional Calculus’. Ann. Pure Appl. Logic 50(1), 71–106 (1990) · Zbl 0709.03009 · doi:10.1016/0168-0072(90)90055-7
[32] Rybakov V.V.: ’Rules of Inference with Parameters for Intuitionistic Logic’. J. Symb. Log. 57(3), 912–923 (1992) · Zbl 0788.03007 · doi:10.2307/2275439
[33] Rybakov V.V.: ’Logical equations and admissible rules of inference with parameters in modal provability logics’. Studia Logica 49(2), 215–239 (1990) · Zbl 0729.03012 · doi:10.1007/BF00935600
[34] Rybakov, V.V., Admissible Logical Inference Rules. Series: Studies in Logic and the Foundations of Mathematics, Vol. 136, Elsevier Sci. Publ., North-Holland, 1997.
[35] Rybakov V.V.: ’Logics with the universal modality and admissible consecutions’. Journal of Applied Non-Classical Logics 17(3), 383–396 (2007) · Zbl 1186.03047 · doi:10.3166/jancl.17.359-382
[36] Rybakov V.V.: ’Linear temporal logic with until and next, logical consecutions’. Ann. Pure Appl. Logic 155(1), 32–45 (2008) · Zbl 1147.03008 · doi:10.1016/j.apal.2008.03.001
[37] Rybakov V.V.: ’Multi-modal and Temporal Logics with Universal Formula – Reduction of Admissibility to Validity and Unification’. J. Log. Comput. 18(4), 509–519 (2008) · Zbl 1149.03017 · doi:10.1093/logcom/exm078
[38] Wójcicki R.: ’Theories, Theoretical Models, Truth, part I; Popperian and non- Popperian Theories in science’. Foundations of Science 1, 337–406 (1995/96)
[39] Wójcicki R.: ’Theories, Theoretical Models, Truth, part II: Tarski’s theory of truth and its relevance for the theory of science’. Foundations of Science 4, 471–516 (1995/96)
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.