Допустимость и унификация в модальных логиках, близких к S4.2

Допустимость и унификация в модальных логиках, близких к $S4.2$

Рыбаков В. В.
Сибирский математический журнал, 65, 1, 198-206 (2024)
Скачать статью

УДК 510.64+510.65+510.66 
DOI: 10.33048/smzh.2024.65.115

Аннотация:

Изучаются проблемы унифицируемости и допустимости правил вывода для бесконечного класса модальных логик. Логики предполагаются разрешимыми, полными по Крипке и порождаемыми классами фреймов с наибольшими кластерами (в частности, такие логики расширяют модальную логику $S4.2$). Для любой такой логики $L$ и для любой формулы $\alpha$, унифицируемой $L$, эффективно строится некоторый унификатор $\sigma$ для $\alpha$ в $L$, проверяющий допустимость в $L$ любого данного правила вывода $\alpha / \beta$ с переключаемой главной модальностью для заключения правила $\beta$ (т. е. $\sigma$ решает проблему допустимости для всех таких правил вывода).

Литература:
  1. Robinson A. A machine oriented logic based on the resolution principle // J. ACM. 1965. V. 12, N 1. P. 23–41.
     
  2. Knuth D. E., Bendix P. B. Simple word problems in universal algebras // Automation of Reasoning. J. H. Siekmann et al. (eds.). Berlin; Heidelberg, 1983. P. 342–376. (Symbolic Computations; V. 1064).
     
  3. Baader F., Snyder W. Unification theory // Handbook of automated reasoning. Berlin: Springer, 2001. P. 447–533.
     
  4. Baader F., Ghilardi S. Unification in modal and description logics // Logic J. IGPL. 2011. V. 19, N 6. P. 705–730. 
     
  5. Baader F., Morawska B. Unification in the description logic $EL$ // Log. Methods Comput. Sci. 2010. V. 6. P. 1–31.
     
  6. sl Baader F., Küsters R. Unification in a description logic with transitive closure of roles // Proceedings of the 8th international conference on logic for programming, artificial intelligence and reasoning (LPAR 2001). Springer, 2001. P. 217–232. (Lect. Notes Comp. Sci.; V. 2250).
     
  7. Baader F., Narendran P. Unification of concept terms in description logics // J. Symbol. Comput. 2001. V. 31. P. 277–305.
     
  8. Rybakov V. V. Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus // Ann. Pure Appl. Logic. 1990. V. 50, N 1. P. 71–106.
     
  9. Rybakov V. V. Rules of inference with parameters for intuitionistic logic // J. Symbol Logic. 1992. V. 57, N 3. P. 912–923.
     
  10. Rybakov V. V. Admissible logical inference rules. Amsterdam: North-Holland, 1997. (Elsevier Sci. Publ.; V. 136). 
     
  11. Ghilardi S. Unification through projectivity // J. Logic Comput. 1997. V. 7, N 6. P. 733–752.
     
  12. Ghilardi S. Unification, finite duality and projectivity in varieties of Heyting algebras // Ann. Pure Appl. Logic. 2004. V. 127, N 1–3. P. 99–115.
     
  13. Ghilardi S. Unification in intuitionistic logic // J. Symbol Logic. 1999. V. 64, N 2. P. 859 –880.
     
  14. Ghilardi S. Best solving modal equations // Ann. Pure Appl. Logic. 2000. V. 102. P. 183–198.
     
  15. Ghilardi S. Filtering unification and most general unifiers in modal logic // J. Symbol. Logic. 2004. V. 69, N 3. P. 879–906.
     
  16. Je$\check{r}$ábek E. Admissible rules of modal logics // J. Logic Comput. 2005. V. 15, N ?. P. 411–431.
     
  17. Je$\check{r}$ábek E. Independent bases of admissible rules // Logic J. IGPL. 2008. V. 16, N ?. P. 249–267.
     
  18. Je$\check{r}$ábek E. Rules with parameters in modal logic. I. 2013. CoRR abs/1305.4912.
     
  19. Iemhof R. On the admissible rules of intuitionistic propositional logic // J. Symbol. Logic. 2001. V. 66. P. 281–294.
     
  20. Iemhoff R., Metcalfe G. Proof theory for admissible rules // Ann. Pure Appl. Logic. 2009. V. 159. P. 171–186.
     
  21. Balbiani Ph., Mojtahedi M. Unification with parameters in the implication fragment of classical propositional logic // Logic J. IGPL. 2022. V. 30, N 3. P. 454–464.
     
  22. Balbiani Ph. Unification in modal logic // Indian conference on logic and its applications (ICLA), 1 March 2019. Delhi, India, 2019. DOI: https://doi.org/10.1007/978-3-662-58771-3- 1.
     
  23. Bashmakov S., Kosheleva A., Rybakov V. Non-unifiability in linear temporal logic of knowledge with multi-agent relations // Sib. Math. Rep. 2016. V. 13. P. 656–663.
     
  24. Gabbay D. M., Hodkinson I. M., Reynolds M. A. Temporal logic: Mathematical foundations and computational aspects. Oxford: Clarendon Press, 1994. V. 1.
     
  25. Gabbay D. M., Hodkinson I. M. An axiomatization of the temporal logic with Until and Since over the real numbers // J. Logic Comput. 1990. V. 1. P. 229–260.
     
  26. Gabbay D. M., Hodkinson I. M. Temporal logic in the context of databases. Oxford: Oxford University, 1995. (Logic and Reality: Essays on the Legacy of Arthur Prior).
     
  27. Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: Specification. New York: Springer-Verl., 1992.
     
  28. Manna Z., Pnueli A. Temporal verification of reactive systems: Safety. New York: Springer, 1995.
     
  29. Vardi M. Y. Reasoning about the past with two-way automata // International Colloquium on Automata, Languages and Programming. Berlin; Heidelberg: Springer-Verl., 1998. P. 628– 641. (Lect. Notes Comput. Sci.; V. 1443).
     
  30. Rybakov V. V. Linear temporal logic with until and next, logical consecution // Ann. Pure Appl. Logic. 2008. V. 155. P. 32–45.
     
  31. Babenyshev S., Rybakov V. Linear temporal logic $LTL$: basis for admissible rules // J. Logic Comput. 2011. V. 21. P. 157–177.
     
  32. Rybakov V. V. Logical consecutions in discrete linear temporal logic // J. Symbol. Logic. 2005. V. 70, N 4. P. 1137 –1149.
     
  33. Rybakov V. Logics with universal modality and admissible consecutions // J. Appl. Non-Classical Logics. 2007. V. 17, N 3. P. 381–394.
     
  34. Rybakov Vladimir V. Writing out unifiers in linear temporal logic // J. Logic Comput. 2012. V. 22, N 5. P. 1199–1206.
     
  35. Rybakov V. Unifiers in transitive modal logics for formulas with coefficients (meta-variables) // Logic J. IGPL. 2013. V. 21, N 2. P. 205–215.
     
  36. Dzik W., Wojtylak P. Projective unification in modal logic // Logic J. IGPL. 2012. V. 20, N 1. P. 121–153.
     
  37. Wrónski A. Transparent unification problem // Rep. Math. Logic. 1995. V. 20. P. 105–107.
     
  38. Wrónski A. Transparent verifiers in intermediate logics // Abstracts of the 54th Conference in History of Mathematics. Cracow: The Jagiellonian University, 2008. P. 6.
     
  39. Kroger F., Merz S. Temporal logic and state systems. Berlin; Heidelberg: Springer, 2008. (Texts in Theoretical Comput. Sci.).

Работа поддержана грантом РНС (проект No. 23-21-00213).

Рыбаков Владимир Владимирович (ORCID 0000-0002-6654-9712)
  1. Сибирский федеральный университет, институт математики и информатики, 
    пр. Свободный, 79, Красноярск 660041
  2. Институт систем информатики РАН, 
    пр. Академика Лаврентьева, 6, Новосибирск 630090

E-mail: Vladimir Rybakov@mail.ru

Статья поступила 12 апреля 2023 г.
После доработки — 8 октября 2023 г.
Принята к публикации 28 ноября 2023 г.