×

zbMATH — the first resource for mathematics

Unification and inference rules in the multi-modal logic of knowledge and linear time LTK. (English) Zbl 07325268
Summary: 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.
MSC:
68 Computer science
03 Mathematical logic and foundations
PDF BibTeX XML Cite
Full Text: DOI MNR
References:
[1] A. Robinson, “A machine oriented logic based on the resolution principle”, J. of the ACM, 12:1 (1965), 23-41 · Zbl 0139.12303
[2] D. Knuth, P. Bendix, Simple Word Problems in Universal Algebras, ed. J. Leech, Pergamon Press, New York, 1970, 263-297 · Zbl 0188.04902
[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 · Zbl 1011.68126
[4] F. Baader, S. Ghilardi, “Unification in modal and description logics”, Logic Jnl IGPL, 19:6 (2011), 705-730 · Zbl 1258.03018
[5] F. Baader, B. Morawska, “Unification in the description logic EL”, Logical Methods in Computer Science, 6 (2010), 1-31 · Zbl 1214.68379
[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 · Zbl 1275.68134
[7] F. Baader, B. Morawska, “Unification of concept terms in description logics”, Journal of Symbolic Computation, 31 (2001), 277-305 · Zbl 0970.68166
[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 · Zbl 0709.03009
[9] V.V. Rybakov, “Rules of Inference with Parameters for Intuitionistic logic”, J. of Symbolic Logic, 57:3 (1992), 912-923 · Zbl 0788.03007
[10] V. V. Rybakov, Admissible Logical Inference Rules, Studies in Logic and the Foundations of Mathematics, 136, Elsevier Sci. Publ., North-Holland, 1997 · Zbl 0872.03002
[11] S. Ghilardi, “Unification Through Projectivity”, J. of Logic and Computation, 7:6 (1997), 733-752 · Zbl 0894.08004
[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 · Zbl 1058.03020
[13] S. Ghilardi, “Unification in Intuitionistic logic”, Journal of Symbolic Logic, 64:2 (1999), 859-880 · Zbl 0930.03009
[14] S. Ghilardi, “Best solving modal equations”, Annals of Pure and Applied Logic, 102 (2000), 183-198 · Zbl 0949.03010
[15] S. Ghilardi, L. Sacchetti, “Filtering Unification and Most General Unifiers in Modal Logic”, Journal of Symbolic Logic, 69:3 (2004), 879-906 · Zbl 1069.03011
[16] E. Jerabek, “Admissible rules of modal logics”, Journal of Logic and Computation, 15 (2005), 411-431 · Zbl 1077.03011
[17] E. Jerabek, “Independent bases of admissible rules”, Logic Journal of the IGPL, 16 (2008), 249-267 · Zbl 1146.03008
[18] E. Jerabek, Rules with parameters in modal logic I, 2013, arXiv: · Zbl 1408.03015
[19] R. Iemhof, “On the admissible rules of intuitionistic propositional logic”, Journal of Symbolic Logic, 66 (2001), 281-294 · Zbl 0986.03013
[20] R. Iemhof, G. Metcalfe, “Proof theory for admissible rules”, Annals of Pure and Applied Logic, 159 (2009), 171-186 · Zbl 1174.03024
[21] D. M. Gabbay, I. M. Hodkinson, M. A. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, v. 1, Clarendon Press, Oxford, 1994 · Zbl 0921.03023
[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 · Zbl 0744.03018
[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
[24] Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, v. 1, Springer, 1992 · Zbl 0753.68003
[25] Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety, v. 1, Springer, 1995 · Zbl 1288.68169
[26] M. Vardi, “An automata-theoretic approach to linear temporal logic”, Y. Banff Higher Order Workshop (1995), 238-266
[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 · Zbl 0909.03019
[28] V. V. Rybakov, “Linear temporal logic with until and next, logical consecutions”, Annals of Pure and Applied Logic, 155 (2008), 32-45 · Zbl 1147.03008
[29] S. Babenyshev, V Rybakov, “Linear temporal logic LTL: basis for admissible rules”, Journal of Logic and Computation, 21 (2011), 157-177 · Zbl 1233.03026
[30] V. V. Rybakov, “Logical Consecutions in Discrete Linear Temporal Logic”, J. of Symbolic Logic, 70:4 (2005), 1137-1149 · Zbl 1110.03010
[31] V. V. Rybakov, “Writing out Unifiers in Linear Temporal Logic”, J. Logic Computation, 22:5 (2012), 1199-1206 · Zbl 1259.03029
[32] V. V. Rybakov, “Projective formulas and unification in linear temporal logic LTLU”, Logic Journal of the IGPL, 22:4 (2014), 665-672 · Zbl 1342.03017
[33] V. V. Rybakov, “Unifiers in transitive modal logics for formulas with coefficients (meta-variables)”, Logic Jnl IGPL, 21:2 (2013), 205-215 · Zbl 1278.03050
[34] V. V. Rybakov, “Writing out unifiers for formulas with coefficients in intuitionistic logic”, Logic Jnl IGPL, 21:2 (2013), 187-198 · Zbl 1277.03004
[35] W. Dzik, P. Wojtylak, “Projective unification in modal logic”, Logic Journal of IGPL, 20:1 (2012), 121-153 · Zbl 1260.03041
[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 · Zbl 0952.03019
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.