Общий метод доказательства разрешимости интуиционистских модальных логик
Article Sidebar
Опубликован:
16.01.2007
Main Article Content
Аннотация
В настоящей статье мы предлагаем новый общий метод доказательства разрешимости интуиционистских модальных логик. Этот метод опирается на доказываемое в настоящей работе обобщение результата Ганцингера, Мейера и Вианеса (см. [10]) о том, что двухпеременный монадический защищенный фрагмент $GF^{2}_{mon}$ классической первопорядковой логики, в котором на некоторое отношение, встречающееся в защитниках, наложено условие, выразимое как условие замкнутости, определимое в монадической второпорядковой логике, разрешим. Мы обобщаем этот результат на случай, когда условия упомянутого вида накладываются на более, чем одно отношение. Такое обобщение позволяет нам доказать разрешимость широкого класса интуиционистских модальных систем путем их погружения в этот разрешимый фрагмент.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Алёшина Н., Шкатов Д. Общий метод доказательства разрешимости интуиционистских модальных логик // Логические исследования / Logical Investigations. 2007. Т. 13. C. 5-23.
Выпуск
Раздел
Статьи
Литература
Alechina N., Mendler М., de Paiva V., Ritter E. Categorical and Kripke semantics for constructive modal logics // Proceedings of the 15th International Workshop Computer Science Logic, CSL 2001. Lecture Notes in Computer Science, vol. 2142. Springer, 2001. P. 292-307.
Andreka van Benthem J., Nemeti I. Modal Logics and Bounded Fragments of Predicate Logic // Journal of Philosophical Logic. 1998. Vol. 21. P. 217-274.
Bull R.A. A modal extension of intuitionistic modal logic // Notre Dame Journal of Formal Logic. 1965. Vol. VI. P. 142-146.
Bull R.A. Some modal calculi based on IC // Formal Systems and Recursive Functions. North Holland, 1965. P. 3-7.
Bull R.A. MIPC as the formalisation of an intuitionistic concept of modality // Journal of Symbolic Logic. 1966. Vol. 31. P. 609-616.
Dosen K. Models for stronger normal intuitionistic modal logics // Studia Logica. 1985. Vol. 44. P. 39-70.
Fairtlough M., Mendler M. Propositional lax logic // Information and Computation. 1997. Vol. 137. P. 1-33.
Fisher Servi G. On modal logics with intuitionistic base // Studia Logica. 1986. Vol. 27. P. 533-546.
Fitch F. B. Intuitionistic modal logic with quantifiers // Portugaliae Mathematicae. 1948. Vol. 7. P. 113-118.
Ganzinger H., Meyer Ch., Veanes M. The Two-Variable Guarded Fragment with Transitive Relations // Proceedings of 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999. P. 24-34.
Goldblatt R. Metamathematics of modal logic // Reports on Mathematical Logic. 1976. Vol. 6, 7. P. 31-42, 21-52.
Mendler M. Constrained Proofs: a Logic for Dealing with Behavioural Constrains in Formal Hardware Verification // Proceedings of Workshop on Designing Correct Circuits, Oxford 1990. Springer-Verlag, 1991.
Mints G. Some calculi of modal logic // Труды математического института им. В.А. Стеклова. Т. 98. М., 1968. С. 88-111.
Моggi Е. Notions of Computation and Monads // Information and Computation. 1991. Vol. 93. P. 55-92.
Ono H. On some intuitionistic modal logics // Publications of the Research Institute for Mathematical Science. Kyoto University. 1977. Vol. 13. P. 55-67.
Ono H., Suzuki N.-Y. Relations between intuitionistic modal logics and intermediate predicate logics // Reports on Mathematical Logic. 1988. Vol. 22. P. 65-87.
Pfenning F., Davies R. A judgmental reconstruction of modal logic // Mathematical Structures in Computer Science. 2001. Vol. 11. P. 511-540.
Plotkin G., Stirling C. A framework for intuitionistic modal logic // Theoretical Aspects of Reasoning about Knowledge. 1986. P. 399-406.
Prawitz D. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksell, 1965.
Simpson A. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis. University of Edinburgh. 1994.
Stirling C. Modal Logics for Communicating Systems // Theoretical Computer Science. 1987. Vol. 49. P. 311-347.
Wijesekera D. Constructive Modal Logic I // Annals of Pure and Applied Logic. 1990. Vol. 50. P. 271-301.
Wolter F., Zakharyaschev M. On the Relation between Intuitionistic and Classical Modal Logics // Algebra and Logic. 1997. Vol. 36. P. 121-155.
Wolter F., Zakharyaschev M. Intuitionistic modal logics // Logic and Foundations of Mathematics. Kluwer Academic Publishers, 1999. P. 227-238.
Wolter F., Zakharyaschev M. Intuitionistic modal logics as fragments of classical bimodal logics // Orlowska E. (ed.) Logic at Work. Springer-Verlag, 1999. P. 168- 186.
Zakharyaschev M., Wolter F., Chagrov A. Advanced Modal Logic // Gabbay D. et. al (eds.) Handbook of Philosophical Logic. Kluwer Academic Publishers, 2001. Vol. 3. P. 83-266.
Andreka van Benthem J., Nemeti I. Modal Logics and Bounded Fragments of Predicate Logic // Journal of Philosophical Logic. 1998. Vol. 21. P. 217-274.
Bull R.A. A modal extension of intuitionistic modal logic // Notre Dame Journal of Formal Logic. 1965. Vol. VI. P. 142-146.
Bull R.A. Some modal calculi based on IC // Formal Systems and Recursive Functions. North Holland, 1965. P. 3-7.
Bull R.A. MIPC as the formalisation of an intuitionistic concept of modality // Journal of Symbolic Logic. 1966. Vol. 31. P. 609-616.
Dosen K. Models for stronger normal intuitionistic modal logics // Studia Logica. 1985. Vol. 44. P. 39-70.
Fairtlough M., Mendler M. Propositional lax logic // Information and Computation. 1997. Vol. 137. P. 1-33.
Fisher Servi G. On modal logics with intuitionistic base // Studia Logica. 1986. Vol. 27. P. 533-546.
Fitch F. B. Intuitionistic modal logic with quantifiers // Portugaliae Mathematicae. 1948. Vol. 7. P. 113-118.
Ganzinger H., Meyer Ch., Veanes M. The Two-Variable Guarded Fragment with Transitive Relations // Proceedings of 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999. P. 24-34.
Goldblatt R. Metamathematics of modal logic // Reports on Mathematical Logic. 1976. Vol. 6, 7. P. 31-42, 21-52.
Mendler M. Constrained Proofs: a Logic for Dealing with Behavioural Constrains in Formal Hardware Verification // Proceedings of Workshop on Designing Correct Circuits, Oxford 1990. Springer-Verlag, 1991.
Mints G. Some calculi of modal logic // Труды математического института им. В.А. Стеклова. Т. 98. М., 1968. С. 88-111.
Моggi Е. Notions of Computation and Monads // Information and Computation. 1991. Vol. 93. P. 55-92.
Ono H. On some intuitionistic modal logics // Publications of the Research Institute for Mathematical Science. Kyoto University. 1977. Vol. 13. P. 55-67.
Ono H., Suzuki N.-Y. Relations between intuitionistic modal logics and intermediate predicate logics // Reports on Mathematical Logic. 1988. Vol. 22. P. 65-87.
Pfenning F., Davies R. A judgmental reconstruction of modal logic // Mathematical Structures in Computer Science. 2001. Vol. 11. P. 511-540.
Plotkin G., Stirling C. A framework for intuitionistic modal logic // Theoretical Aspects of Reasoning about Knowledge. 1986. P. 399-406.
Prawitz D. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksell, 1965.
Simpson A. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis. University of Edinburgh. 1994.
Stirling C. Modal Logics for Communicating Systems // Theoretical Computer Science. 1987. Vol. 49. P. 311-347.
Wijesekera D. Constructive Modal Logic I // Annals of Pure and Applied Logic. 1990. Vol. 50. P. 271-301.
Wolter F., Zakharyaschev M. On the Relation between Intuitionistic and Classical Modal Logics // Algebra and Logic. 1997. Vol. 36. P. 121-155.
Wolter F., Zakharyaschev M. Intuitionistic modal logics // Logic and Foundations of Mathematics. Kluwer Academic Publishers, 1999. P. 227-238.
Wolter F., Zakharyaschev M. Intuitionistic modal logics as fragments of classical bimodal logics // Orlowska E. (ed.) Logic at Work. Springer-Verlag, 1999. P. 168- 186.
Zakharyaschev M., Wolter F., Chagrov A. Advanced Modal Logic // Gabbay D. et. al (eds.) Handbook of Philosophical Logic. Kluwer Academic Publishers, 2001. Vol. 3. P. 83-266.