Допустимость и унификация в модальных логиках, близких к S4.2
Допустимость и унификация в модальных логиках, близких к $S4.2$
Аннотация:
Изучаются проблемы унифицируемости и допустимости правил вывода для бесконечного класса модальных логик. Логики предполагаются разрешимыми, полными по Крипке и порождаемыми классами фреймов с наибольшими кластерами (в частности, такие логики расширяют модальную логику $S4.2$). Для любой такой логики $L$ и для любой формулы $\alpha$, унифицируемой $L$, эффективно строится некоторый унификатор $\sigma$ для $\alpha$ в $L$, проверяющий допустимость в $L$ любого данного правила вывода $\alpha / \beta$ с переключаемой главной модальностью для заключения правила $\beta$ (т. е. $\sigma$ решает проблему допустимости для всех таких правил вывода).
Литература:
- Robinson A. A machine oriented logic based on the resolution principle // J. ACM. 1965. V. 12, N 1. P. 23–41.
- 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).
- Baader F., Snyder W. Unification theory // Handbook of automated reasoning. Berlin: Springer, 2001. P. 447–533.
- Baader F., Ghilardi S. Unification in modal and description logics // Logic J. IGPL. 2011. V. 19, N 6. P. 705–730.
- Baader F., Morawska B. Unification in the description logic $EL$ // Log. Methods Comput. Sci. 2010. V. 6. P. 1–31.
- 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).
- Baader F., Narendran P. Unification of concept terms in description logics // J. Symbol. Comput. 2001. V. 31. P. 277–305.
- 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.
- Rybakov V. V. Rules of inference with parameters for intuitionistic logic // J. Symbol Logic. 1992. V. 57, N 3. P. 912–923.
- Rybakov V. V. Admissible logical inference rules. Amsterdam: North-Holland, 1997. (Elsevier Sci. Publ.; V. 136).
- Ghilardi S. Unification through projectivity // J. Logic Comput. 1997. V. 7, N 6. P. 733–752.
- 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.
- Ghilardi S. Unification in intuitionistic logic // J. Symbol Logic. 1999. V. 64, N 2. P. 859 –880.
- Ghilardi S. Best solving modal equations // Ann. Pure Appl. Logic. 2000. V. 102. P. 183–198.
- Ghilardi S. Filtering unification and most general unifiers in modal logic // J. Symbol. Logic. 2004. V. 69, N 3. P. 879–906.
- Je$\check{r}$ábek E. Admissible rules of modal logics // J. Logic Comput. 2005. V. 15, N ?. P. 411–431.
- Je$\check{r}$ábek E. Independent bases of admissible rules // Logic J. IGPL. 2008. V. 16, N ?. P. 249–267.
- Je$\check{r}$ábek E. Rules with parameters in modal logic. I. 2013. CoRR abs/1305.4912.
- Iemhof R. On the admissible rules of intuitionistic propositional logic // J. Symbol. Logic. 2001. V. 66. P. 281–294.
- Iemhoff R., Metcalfe G. Proof theory for admissible rules // Ann. Pure Appl. Logic. 2009. V. 159. P. 171–186.
- 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.
- 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.
- 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.
- Gabbay D. M., Hodkinson I. M., Reynolds M. A. Temporal logic: Mathematical foundations and computational aspects. Oxford: Clarendon Press, 1994. V. 1.
- 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.
- 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).
- Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: Specification. New York: Springer-Verl., 1992.
- Manna Z., Pnueli A. Temporal verification of reactive systems: Safety. New York: Springer, 1995.
- 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).
- Rybakov V. V. Linear temporal logic with until and next, logical consecution // Ann. Pure Appl. Logic. 2008. V. 155. P. 32–45.
- Babenyshev S., Rybakov V. Linear temporal logic $LTL$: basis for admissible rules // J. Logic Comput. 2011. V. 21. P. 157–177.
- Rybakov V. V. Logical consecutions in discrete linear temporal logic // J. Symbol. Logic. 2005. V. 70, N 4. P. 1137 –1149.
- Rybakov V. Logics with universal modality and admissible consecutions // J. Appl. Non-Classical Logics. 2007. V. 17, N 3. P. 381–394.
- Rybakov Vladimir V. Writing out unifiers in linear temporal logic // J. Logic Comput. 2012. V. 22, N 5. P. 1199–1206.
- Rybakov V. Unifiers in transitive modal logics for formulas with coefficients (meta-variables) // Logic J. IGPL. 2013. V. 21, N 2. P. 205–215.
- Dzik W., Wojtylak P. Projective unification in modal logic // Logic J. IGPL. 2012. V. 20, N 1. P. 121–153.
- Wrónski A. Transparent unification problem // Rep. Math. Logic. 1995. V. 20. P. 105–107.
- Wrónski A. Transparent verifiers in intermediate logics // Abstracts of the 54th Conference in History of Mathematics. Cracow: The Jagiellonian University, 2008. P. 6.
- 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)
- Сибирский федеральный университет, институт математики и информатики,
пр. Свободный, 79, Красноярск 660041 - Институт систем информатики РАН,
пр. Академика Лаврентьева, 6, Новосибирск 630090
E-mail: Vladimir Rybakov@mail.ru
Статья поступила 12 апреля 2023 г.
После доработки — 8 октября 2023 г.
Принята к публикации 28 ноября 2023 г.