Общий метод доказательства разрешимости интуиционистских модальных логик
##plugins.themes.bootstrap3.article.sidebar##
Published:
16.01.2007
##plugins.themes.bootstrap3.article.main##
Abstract
We generalise the result of [10] on decidability of the two variable monadic guarded fragmet of first order logic with constraints on the guard relations expressible in monadic second order logic. In [10] such constraints apply to one relation at a time. We modify their proof to obtain decidability for constraint involving several relations. Now we can use this result to prove decidability of multi-modal logics where conditions on accessibility relations involve more than one relation. Our main application is intuitionistic modal logic, where the intuitionistic and modal accessibility relations usually interact in a non-trivial way.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Alechina N., Shkatov D. Общий метод доказательства разрешимости интуиционистских модальных логик // Logicheskie Issledovaniya / Logical Investigations. 2007. VOL. 13. C. 5-23.
Issue
Section
Papers
References
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.