Geodesic
Non-unifiability in linear temporal logic of knowledge with multi-agent relations
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 13 (2016), pp. 656-663.

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper is devoted to the study of the unification problem in the linear temporal logic of knowledge with multi-agent relations (denoted in the sequel as $LFPK$). This logic is based on frames (models) with time points represented by integer numbers from $Z$ and the information clusters $C^i$ for $i \in Z$ with multi-agent accessibility relations $R_i$. The first main result is a theorem describing a criterion for formulas to be not unifiable in $LFPK$. The second one is a construction of a basis for all inference rules passive in $LFPK$.
Keywords: modal temporal logic, passive inference rules.
Mots-clés : unification 
@article{SEMR_2016_13_a17,
     author = {S. I. Bashmakov and A. V. Kosheleva and V. Rybakov},
     title = {Non-unifiability in linear temporal logic of knowledge with multi-agent relations},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {656--663},
     publisher = {mathdoc},
     volume = {13},
     year = {2016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2016_13_a17/}
}
TY  - JOUR
AU  - S. I. Bashmakov
AU  - A. V. Kosheleva
AU  - V. Rybakov
TI  - Non-unifiability in linear temporal logic of knowledge with multi-agent relations
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2016
SP  - 656
EP  - 663
VL  - 13
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2016_13_a17/
LA  - en
ID  - SEMR_2016_13_a17
ER  - 
%0 Journal Article
%A S. I. Bashmakov
%A A. V. Kosheleva
%A V. Rybakov
%T Non-unifiability in linear temporal logic of knowledge with multi-agent relations
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2016
%P 656-663
%V 13
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2016_13_a17/
%G en
%F SEMR_2016_13_a17
S. I. Bashmakov; A. V. Kosheleva; V. Rybakov. Non-unifiability in linear temporal logic of knowledge with multi-agent relations. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 13 (2016), pp. 656-663. http://geodesic.mathdoc.fr/item/SEMR_2016_13_a17/

[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, J. Leech (ed.), Simple Word Problems in Universal Algebras, Pergamon Press, 1970, 263–297 | MR | Zbl

[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

[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 | Zbl

[6] F. Baader, P. Narendran, “Unification in a description logic with transitive closure of roles”, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001, 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 | Zbl

[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:3 (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, CoRR, arXiv: 1305.4912 [cs.LO] | MR

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

[20] R. Iemhoff, 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 | Zbl

[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 | Zbl

[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

[37] S. I. Bashmakov, “Unification and inference rules in the multi-modal logic of knowledge and linear time LTK”, Journal of Siberian Federal University. Mathematics and Physics, 9:2 (2016), 149–157