Unification and inference rules in the multi-modal logic of knowledge and linear time LTK

Stepan I. Bashmakov

Žurnal Sibirskogo federalʹnogo universiteta. Matematika i fizika, Tome 9 (2016) no. 2, pp. 149-157.

Résumé

We study unification of formulas in multi-modal LTK logic and give a syntactic description of all formulas which are non-unificable in this logic. Passive inference rules are considered, it is shown that in LTK logic there is a finite basis for passive rules.

Détail

Keywords: modal temporal logic, passive inference rules.
Mots-clés : unification

Bibliographie

[1] A. Robinson, “A machine oriented logic based on the resolution principle”, J. of the ACM, 12:1 (1965), 23–41 | DOI | MR | Zbl

[2] D. Knuth, P. Bendix, Simple Word Problems in Universal Algebras, ed. J. Leech, Pergamon Press, New York, 1970, 263–297 | MR

[3] F. Baader, W. Snyder, “Unification theory”, Handbook of Automated Reasoning, v. I, eds. Robinson J. A., Voronkov A., Elsevier Science Publishers, 2001, 447–533

[4] F. Baader, S. Ghilardi, “Unification in modal and description logics”, Logic Jnl IGPL, 19:6 (2011), 705–730 | DOI | MR | Zbl

[5] F. Baader, B. Morawska, “Unification in the description logic EL”, Logical Methods in Computer Science, 6 (2010), 1–31 | DOI | MR

[6] F. Baader, P. Narendran, “Unification in a description logic with transitive closure of roles”, Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, 2250, Springer, 2001, 217–232 | MR | Zbl

[7] F. Baader, B. Morawska, “Unification of concept terms in description logics”, Journal of Symbolic Computation, 31 (2001), 277–305 | DOI | MR | Zbl

[8] V.V. Rybakov, “Problems of Substitution and Admissibility in the Modal System Grz and in Intuitionistic Propositional Calculus”, Annals of Pure and Applied Logic, 50:1 (1990), 71–106 | DOI | MR | Zbl

[9] V.V. Rybakov, “Rules of Inference with Parameters for Intuitionistic logic”, J. of Symbolic Logic, 57:3 (1992), 912–923 | DOI | MR | Zbl

[10] V. V. Rybakov, Admissible Logical Inference Rules, Studies in Logic and the Foundations of Mathematics, 136, Elsevier Sci. Publ., North-Holland, 1997 | MR

[11] S. Ghilardi, “Unification Through Projectivity”, J. of Logic and Computation, 7:6 (1997), 733–752 | DOI | MR | Zbl

[12] S. Ghilardi, “Unification, finite duality and projectivity in varieties of Heyting algebras”, Annals of Pure and Applied Logic, 127:1–3 (2004), 99–115 | DOI | MR | Zbl

[13] S. Ghilardi, “Unification in Intuitionistic logic”, Journal of Symbolic Logic, 64:2 (1999), 859–880 | DOI | MR | Zbl

[14] S. Ghilardi, “Best solving modal equations”, Annals of Pure and Applied Logic, 102 (2000), 183–198 | DOI | MR | Zbl

[15] S. Ghilardi, L. Sacchetti, “Filtering Unification and Most General Unifiers in Modal Logic”, Journal of Symbolic Logic, 69:3 (2004), 879–906 | DOI | MR | Zbl

[16] E. Jerabek, “Admissible rules of modal logics”, Journal of Logic and Computation, 15 (2005), 411–431 | DOI | MR | Zbl

[17] E. Jerabek, “Independent bases of admissible rules”, Logic Journal of the IGPL, 16 (2008), 249–267 | DOI | MR | Zbl

[18] E. Jerabek, Rules with parameters in modal logic I, 2013, arXiv: 1305.4912 | MR

[19] R. Iemhof, “On the admissible rules of intuitionistic propositional logic”, Journal of Symbolic Logic, 66 (2001), 281–294 | DOI | MR | Zbl

[20] R. Iemhof, G. Metcalfe, “Proof theory for admissible rules”, Annals of Pure and Applied Logic, 159 (2009), 171–186 | DOI | MR | Zbl

[21] D. M. Gabbay, I. M. Hodkinson, M. A. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, v. 1, Clarendon Press, Oxford, 1994 | MR

[22] D. M. Gabbay, I. M. Hodkinson, “An axiomatisation of the temporal logic with Until and Since over the real numbers”, Journal of Logic and Computation, 1 (1990), 229–260 | DOI | MR

[23] D. M. Gabbay, I. M. Hodkinson, “Temporal Logic in Context of Databases”, Logic and Reality, Essays on the legacy of Arthur Prior, ed. J. Copeland, Oxford University Press, 1995 | MR

[24] Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, v. 1, Springer, 1992 | MR

[25] Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety, v. 1, Springer, 1995

[26] M. Vardi, “An automata-theoretic approach to linear temporal logic”, Y. Banff Higher Order Workshop (1995), 238–266 http://citeseer.ist.psu.edu/vardi96automatatheoretic.html

[27] M. Y. Vardi, “Reasoning about the past with two-way automata”, ICALP, LNCS, 1443, eds. Larsen K. G., Skyum S., Winskel G., Springer, 1998, 628–641 | MR | Zbl

[28] V. V. Rybakov, “Linear temporal logic with until and next, logical consecutions”, Annals of Pure and Applied Logic, 155 (2008), 32–45 | DOI | MR | Zbl

[29] S. Babenyshev, V Rybakov, “Linear temporal logic LTL: basis for admissible rules”, Journal of Logic and Computation, 21 (2011), 157–177 | DOI | MR | Zbl

[30] V. V. Rybakov, “Logical Consecutions in Discrete Linear Temporal Logic”, J. of Symbolic Logic, 70:4 (2005), 1137–1149 | DOI | MR | Zbl

[31] V. V. Rybakov, “Writing out Unifiers in Linear Temporal Logic”, J. Logic Computation, 22:5 (2012), 1199–1206 | DOI | MR | Zbl

[32] V. V. Rybakov, “Projective formulas and unification in linear temporal logic LTLU”, Logic Journal of the IGPL, 22:4 (2014), 665–672 | DOI | MR | Zbl

[33] V. V. Rybakov, “Unifiers in transitive modal logics for formulas with coefficients (meta-variables)”, Logic Jnl IGPL, 21:2 (2013), 205–215 | DOI | MR | Zbl

[34] V. V. Rybakov, “Writing out unifiers for formulas with coefficients in intuitionistic logic”, Logic Jnl IGPL, 21:2 (2013), 187–198 | DOI | MR | Zbl

[35] W. Dzik, P. Wojtylak, “Projective unification in modal logic”, Logic Journal of IGPL, 20:1 (2012), 121–153 | DOI | MR | Zbl

[36] V. V. Rybakov, M. Terziler, C. Gencer, “An essay on unification and inference rules for modal logics”, Bulletin of the Section of Logic, 28:3 (1999), 145–157 | MR | Zbl