рус eng
«THE BULLETIN OF IRKUTSK STATE UNIVERSITY». SERIES «MATHEMATICS»
«IZVESTIYA IRKUTSKOGO GOSUDARSTVENNOGO UNIVERSITETA». SERIYA «MATEMATIKA»
ISSN 1997-7670 (Print)
ISSN 2541-8785 (Online)

List of issues > Series «Mathematics». 2023. Vol 44

Satisfiability Problem in Interval FP-logic

Author(s)
Nikita A. Protsenko1, Vladimir V. Rybakov1, Vitaliy V. Rimatskiy1

1Siberian Federal University, Krasnoyarsk, Russian Federation

Abstract
The article investigates the interval modal logic, in which an action of the modal operator ◊ is limited by the boundaries of an interval. In addition, the language of modal logic is extended by the operator 𝐷(𝛼, 𝛽), the truth of which is determined qualitatively: it is true only if the number of points on the interval [𝑐𝑖, 𝑐𝑖+1] where the formula 𝛼 is true is strictly less than the number of points in this segment where the formula 𝛽 is true. The problem of satisfiability of formulas is solved, and as a consequence, the decidability of logic.
About the Authors

Nikita A. Protsenko, Siberian Federal University, Krasnoyarsk, 660041, Russian Federation, nikitaprotsenko2003@gmail.com

Vladimir V. Rybakov, Dr. Sci. (Phys.–Math.), Prof., Siberian Federal University, Krasnoyarsk, 660041, Russian Federation, Rybakov@mail.ru

Vitaliy V. Rimatskiy, Cand. Sci. (Phys. -Math), Assoc. Prof., Siberian Federal University, Krasnoyarsk, 660041, Russian Federation, Gemmeny@rambler.ru

For citation
Protsenko N.A., Rybakiov V.V., Rimatskiy V.V. Satisfiability Problem in Interval FP-logic. The Bulletin of Irkutsk State University. Series Mathematics, 2023, vol. 44, pp. 98–107. https://doi.org/10.26516/1997-7670.2023.44.98
Keywords
modal logic, frame and model Kripke, satisfiability problem
UDC
510.665, 510.643
MSC
03B45, 03H05
DOI
https://doi.org/10.26516/1997-7670.2023.44.98
References
  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, 2008, vol. 5028/2008, pp. 32–41.
  2. Babenyshev S., Rybakov V. Logic of Discovery and Knowledge: Decision Algorithm. KES (2), Lecture Notes in Computer Science, 2008, vol. 5178/2008, pp. 711–718.
  3. Babenyshev S., Rybakov V. Describing Evolutions of Multi-Agent Systems. KES (1) Lecture Notes in Computer Science, 2009, vol. 57, 1/2009, pp. 38–45.
  4. Babenyshev S., Rybakov V. Linear Temporal Logic LTL: Basis for Admissible Rules. J. Logic Computation, 2011, vol. 21, no. 2, pp. 157–177.
  5. Babenyshev S., Rybakov V. Unification in Linear Temporal Logic LTL. Annals for Pure and Applied Logic, 2011, vol. 162, no.12, pp. 991–1000.
  6. Baader F., Sattler U. Expressive Number Restrictions in Description Logics. J. Log. Comput, 1999, vol. 9, no. 3, pp. 319–350.
  7. Baader F., K¨usters R. Unification in a Description Logic with Transitive Closure of Roles. In: Robert Nieuwenhuis, Andrei Voronkov (Eds.). Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, 2001, LNCS, vol. 2250, Springer, pp. 217–232.
  8. Baader F., Morawska B. Unification in the Description Logic EL. Logical Methods in Computer Science, 2010, vol. 6, no. 3, pp. 1–31.
  9. Belardinelli F., Lomuscio A. Interactions between Knowledge and Time in a FirstOrder Logic for Multi-Agent Systems. Completeness Results, Journal of Artificial Intelligence Research, 2012, vol. 45, pp. 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, 1990, vol. 1, pp. 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, pp. 46–57.
  13. Horrocks I., Giese M. , Kharlamov E., Waaler A. Using Semantic Technology to Tame the Data Variety Challenge. IEEE Internet Computing, 2016, vol. 20, no. 6, pp. 62–66.
  14. Rybakov V.V. Linear temporal logic with until and next, logical consecutions, Ann. Pure Appl. Logic, 2008, vol. 155, no. 1, pp. 32–45.
  15. Rybakov V.V. Non-transitive linear temporal logic and logical knowledge operations. J. Logic and Computation, Oxford Press, 2016, vol. 26, no. 3, pp. 945–958.
  16. Rybakov V.V. Temporal logic with overlap temporal relations generated by time states themselves. Siberian Mathematical Reports, 2020, vol. 17, pp. 923–932.
  17. Rybakov V.V. Multi-agent temporal nontransitive linear logics and the admissibility problem. Algebra and Logic, 2020, no. 59, pp. 87–100. https://doi.org/10.33048/alglog.2020.59.108
  18. Rybakov V.V. Branching Time Logics with Multiagent Temporal Accessibility Relations . Siberian Mathematical Journal, 2021, vol. 62, no. 3, pp. 503–510. https://doi.org/10.33048/smzh.2021.62.313
  19. Vardi M. An automata-theoretic approach to linear temporal logic. Y.Banff Higher Order Workshop, 1995, pp. 238–266.
  20. Vardi M.Y. Reasoning about the past with two-way automata. ICALP, LNCS, Springer, 1443, 1998, pp. 628–641.
  21. Wooldridge M., Lomuscio A. Multi-Agent VSK Logic. Proceedings of the Seventh European Workshop on Logics in Artificial Intelligence (JELIAI-2000), 2000, Springer-Verlag, September, 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.

Full text (english)