рус eng
«ИЗВЕСТИЯ ИРКУТСКОГО ГОСУДАРСТВЕННОГО УНИВЕРСИТЕТА». СЕРИЯ «МАТЕМАТИКА»
«IZVESTIYA IRKUTSKOGO GOSUDARSTVENNOGO UNIVERSITETA». SERIYA «MATEMATIKA»
«THE BULLETIN OF IRKUTSK STATE UNIVERSITY». SERIES «MATHEMATICS»
ISSN 1997-7670 (Print)
ISSN 2541-8785 (Online)

Список выпусков > Серия «Математика». 2023. Том 44

Проблема выполнимости в интервальной FP-логике

Автор(ы)
Н. А. Проценко1, В. В. Рыбаков1, В. В. Римацкий1

1Сибирский Федеральный университет, Красноярск, Российская Федерация

Аннотация

Исследуется интервальная модальная логика, в которой действие модального оператора ◊ ограничено границами интервала. Кроме того, язык модальной логики расширен оператором 𝐷(𝛼, 𝛽), истинность которого определяется качественно: он истиннен, только если число точек на отрезке [𝑐𝑖, 𝑐𝑖+1], в которых истинна формула 𝛼, строго меньше числа точек этого отрезка, в которых истинна формула 𝛽. Решается проблема выполнимости формул, и как следствие, разрешимость логики.

Об авторах

Проценко Никита Александрович, Институт математики, Сибирский федеральный университет, Красноярск, 660041, Российская Федерация, nikitaprotsenko2003@gmail.com

Рыбаков Владимир Владимирович, д-р физ.-мат. наук, проф., Институт математики, Сибирский федеральный университет, Красноярск, 660041, Российская Федерация, Rybakov@mail.ru

Римацкий Виталий Валентинович, канд. физ.-мат. наук, доц., Институт математики, Сибирский федеральный университет, Красноярск, 660041, Российская Федерация, Gemmeny@rambler.ru

Ссылка для цитирования
Protsenko N. A., Rybakiov V. V., Rimatskiy V.V. Satisfiability Problem in Interval FP-logic // Известия Иркутского государственного университета. Серия Математика. 2023. Т. 44. C. 98–107. https://doi.org/10.26516/1997-7670.2023.44.98
Ключевые слова
модальная логика, фрейм и модель Крипке, выполнимость формул, проблема выполнимости в логике, разрешимость логики
УДК
510.665, 510.643
MSC
03B45, 03H05
DOI
https://doi.org/10.26516/1997-7670.2023.44.98
Литература
  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.

Полная версия (english)