Geodesic
Unification in linear modal logic on non-transitive time with the universal modality
Žurnal Sibirskogo federalʹnogo universiteta. Matematika i fizika, Tome 11 (2018) no. 1, pp. 3-9.

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

We investigate the question of unification in the linear modal logic on non-transitive time with the universal modality. The semantic construction of logic on linear non-transitive Kripke frames is proposed, effective definability and projectivity of the unifiable formulas are proved. An algorithm for construction the most general unifier is found.
Keywords: temporal modal logic, non-transitive Kripke frame, ground unifier, projective formulas.
Mots-clés : unification 
@article{JSFU_2018_11_1_a0,
     author = {Stepan I. Bashmakov},
     title = {Unification in linear modal logic on non-transitive time with the universal modality},
     journal = {\v{Z}urnal Sibirskogo federalʹnogo universiteta. Matematika i fizika},
     pages = {3--9},
     publisher = {mathdoc},
     volume = {11},
     number = {1},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/JSFU_2018_11_1_a0/}
}
TY  - JOUR
AU  - Stepan I. Bashmakov
TI  - Unification in linear modal logic on non-transitive time with the universal modality
JO  - Žurnal Sibirskogo federalʹnogo universiteta. Matematika i fizika
PY  - 2018
SP  - 3
EP  - 9
VL  - 11
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/JSFU_2018_11_1_a0/
LA  - en
ID  - JSFU_2018_11_1_a0
ER  - 
%0 Journal Article
%A Stepan I. Bashmakov
%T Unification in linear modal logic on non-transitive time with the universal modality
%J Žurnal Sibirskogo federalʹnogo universiteta. Matematika i fizika
%D 2018
%P 3-9
%V 11
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/JSFU_2018_11_1_a0/
%G en
%F JSFU_2018_11_1_a0
Stepan I. Bashmakov. Unification in linear modal logic on non-transitive time with the universal modality. Žurnal Sibirskogo federalʹnogo universiteta. Matematika i fizika, Tome 11 (2018) no. 1, pp. 3-9. http://geodesic.mathdoc.fr/item/JSFU_2018_11_1_a0/

[1] A. Prior, Time and Modality, Oxford University Press, 1957

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

[3] V. Rybakov, Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules, 2015, arXiv: 1503.08761 | MR

[4] S.P. Odintsov, V.V. Rybakov, “Unification Problem in Nelson's Logic N4”, Sib. Electronic Math. Reports, 11 (2014), 434–443 | MR

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

[6] 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

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

[8] S.I. Bashmakov, A.V. Kosheleva, V. Rybakov, “Non-unifiability in linear temporal logic of knowledge with multi-agent relations”, Sib. Electronic Math. Reports, 13 (2016), 923–929 | MR

[9] S. Ghilardi, “Unification Through Projectivity”, J. Logic Comput., 7:6 (1997), 733–752 | DOI | MR

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

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

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

[13] E. Jerábek, “Admissible rules of modal logics”, J. Logic Comput., 15 (2005), 411–431 | DOI | MR

[14] E. Jerábek, “Independent bases of admissible rules”, Logic J. IGPL, 16 (2008), 249–267 | DOI | MR

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

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

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

[18] S. Babenyshev, V. Rybakov, “Unification in linear temporal logic LTL”, Annals of Pure and Applied Logic, 162 (2011), 991–1000 | DOI | MR

[19] S.I. Bashmakov, A.V. Kosheleva, V. Rybakov, “Projective formulas and unification in linear discrete temporal multi-agent logics”, Sib. Electronic Math. Reports, 13 (2016), 923–929 | MR

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

[21] F. Baader, W. Snyder, “Unification theory”, Handbook of Automated Reasoning, v. I, eds. A. Robinson, A. Voronkov, Elsevier, 2001, 445–533 | DOI | MR

[22] W. Dzik, “Unitary Unification of S5 Modal Logic and its Extensions”, Bull. Section of Logic, 32:1–2 (2003), 19–26 | MR

[23] E. Jerábek, “Blending margins: the modal logic K has nullary unification type”, J. Logic Comput., 25 (2015), 1231–1240 | DOI | MR

[24] F. Wolter, M. Zakharyaschev, “Undecidability of the unification and admissibility problems for modal and description logics”, ACM Transactions on Comput. Logic, 9:4 (2008), 25 | DOI | MR

[25] W. A. Pogorzelski, P. Wojtylak, Completeness theory for propositional logics, Birkhäuser, Basel, 2008 | MR

[26] S.I. Bashmakov, A.V. Kosheleva, V. Rybakov, “Unification for multi-agent temporal logics with universal modality”, J. of Logics and their Application, 4:4 (2017), 939–954