Geodesic
Satisfiability problem in interval FP-logic
The Bulletin of Irkutsk State University. Series Mathematics, Tome 44 (2023), pp. 98-107 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

The article investigates the interval modal logic, in which an action of the modal operator $\Diamond$ is limited by the boundaries of an interval. In addition, the language of modal logic is extended by the operator $D (\alpha, \beta)$, the truth of which is determined qualitatively: it is true only if the number of points on the interval $[c_i ; c_{i+1}]$ where the formula $\alpha $ is true is strictly less than the number of points in this segment where the formula $\beta $ is true. The problem of satisfiability of formulas is solved, and as a consequence, the decidability of logic.
Keywords: modal logic, frame and model Kripke, satisfiability problem. 
@article{IIGUM_2023_44_a7,
     author = {Nikita A. Protsenko and Vladimir V. Rybakov and Vitaliy V. Rimatskiy},
     title = {Satisfiability problem in interval {FP-logic}},
     journal = {The Bulletin of Irkutsk State University. Series Mathematics},
     pages = {98--107},
     year = {2023},
     volume = {44},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IIGUM_2023_44_a7/}
}
TY  - JOUR
AU  - Nikita A. Protsenko
AU  - Vladimir V. Rybakov
AU  - Vitaliy V. Rimatskiy
TI  - Satisfiability problem in interval FP-logic
JO  - The Bulletin of Irkutsk State University. Series Mathematics
PY  - 2023
SP  - 98
EP  - 107
VL  - 44
UR  - http://geodesic.mathdoc.fr/item/IIGUM_2023_44_a7/
LA  - en
ID  - IIGUM_2023_44_a7
ER  - 
%0 Journal Article
%A Nikita A. Protsenko
%A Vladimir V. Rybakov
%A Vitaliy V. Rimatskiy
%T Satisfiability problem in interval FP-logic
%J The Bulletin of Irkutsk State University. Series Mathematics
%D 2023
%P 98-107
%V 44
%U http://geodesic.mathdoc.fr/item/IIGUM_2023_44_a7/
%G en
%F IIGUM_2023_44_a7
Nikita A. Protsenko; Vladimir V. Rybakov; Vitaliy V. Rimatskiy. Satisfiability problem in interval FP-logic. The Bulletin of Irkutsk State University. Series Mathematics, Tome 44 (2023), pp. 98-107. http://geodesic.mathdoc.fr/item/IIGUM_2023_44_a7/

[1] Babenyshev S., Rybakov V., “Decidability of Hybrid Logic with Local Common Knowledge Based on Linear Temporal Logic LTL”, CiE 2008, Lecture Notes in Computer Science, 5028, 2008, 32–41

[2] Babenyshev S., Rybakov V., “Logic of Discovery and Knowledge: Decision Algorithm”, KES (2), Lecture Notes in Computer Science, 5178, 2008, 711–718

[3] Babenyshev S., Rybakov V., “Describing Evolutions of Multi-Agent Systems”, KES (1), Lecture Notes in Computer Science, 57, 2009, 38–45

[4] Babenyshev S., Rybakov V., “Linear Temporal Logic LTL: Basis for Admissible Rules”, J. Logic Computation, 21:2 (2011), 157–177

[5] Babenyshev S., Rybakov V., “Unification in Linear Temporal Logic LTL”, Annals for Pure and Applied Logic, 162:12 (2011), 991–1000

[6] Baader F., Sattler U., “Expressive Number Restrictions in Description Logics”, J. Log. Comput., 9:3 (1999), 319–350

[7] Baader F., Küsters R., “Unification in a Description Logic with Transitive Closure of Roles”, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001, LNCS, 2250, eds. Robert Nieuwenhuis, Andrei Voronkov, Springer, 2001, 217–232

[8] Baader F., Morawska B., “Unification in the Description Logic EL”, Logical Methods in Computer Science, 6:3 (2010), 1–31

[9] Belardinelli F., Lomuscio A., “Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems. Completeness Results”, Journal of Artificial Intelligence Research, 45 (2012), 1–45

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

[11] Horrocks I., Sattler U., “A Description Logic with Transitive and Inverse Roles and Role Hierarchies”, Description Logics, 1998

[12] Pnueli A., “The temporal logic of programs”, Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57

[13] Horrocks I., Giese M., “Using Semantic Technology to Tame the Data Variety Challenge”, Kharlamov E., Waaler A., 20:6 (2016), 62–66

[14] Rybakov V.V., “Linear temporal logic with until and next, logical consecutions”, Ann. Pure Appl. Logic, 155:1 (2008), 32–45

[15] Rybakov V.V., “Non-transitive linear temporal logic and logical knowledge operations”, J. Logic and Computation, 26:3 (2016), 945–958

[16] Rybakov V.V., “Temporal logic with overlap temporal relations generated by time states themselves”, Siberian Mathematical Reports, 17 (2020), 923–932

[17] Rybakov V.V., “Multi-agent temporal nontransitive linear logics and the admissibility problem”, Algebra and Logic, 2020, no. 59, 87–100 | DOI

[18] Rybakov V.V., “Branching Time Logics with Multiagent Temporal Accessibility Relations”, Siberian Mathematical Journal, 62:3 (2021), 503–510 | DOI

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

[20] Vardi M.Y., “Reasoning about the past with two-way automata”, ICALP, LNCS, 1443, Springer, 1998, 628–641

[21] Wooldridge M., Lomuscio A., “Multi-Agent VSK Logic”, Proceedings of the Seventh European Workshop on Logics in Artificial Intelligence, JELIAI-2000, Springer-Verlag, 2000

[22] Wooldridge M., “An Automata-theoretic approach to multi-agent planning”, Proceedings of the First European Workshop on Multi-agent Systems (EUMAS), Oxford University, 2003