Abstract
We consider a general format for sequent rules for not necessarily normal modal logics based on classical or intuitionistic propositional logic and provide relatively simple local conditions ensuring cut elimination for such rule sets. The rule format encompasses e.g. rules for the boolean connectives and transitive modal logics such as S4 or its constructive version. We also adapt the method of constructing suitable rule sets by saturation to the intuitionistic setting and provide a criterium for translating axioms for intuitionistic modal logics into sequent rules. Examples include constructive modal logics and conditional logic \(\mathbb{VA}\).
Supported by EPSRC-Project EP/H016317/1.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M.: Variations in Access Control Logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 96–109. Springer, Heidelberg (2008)
Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 292–307. Springer, Heidelberg (2001)
Avron, A., Lahav, O.: Kripke Semantics for Basic Sequent Systems. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 43–57. Springer, Heidelberg (2011)
Bellin, G., de Paiva, V., Ritter, E.: Extended Curry-Howard correspondence for a basic contructive modal logic. In: Areces, C., de Rijke, M. (eds.) M4M-2. ILLC Amsterdam (2001)
Benton, P., Bierman, G., de Paiva, V.: Computational types from a logical perspective. J. Funct. Programming 8(2), 177–193 (1998)
Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: LICS 2008, pp. 229–240. IEEE Computer Society (2008)
Fairtlough, M., Mendler, M.: Propositional lax logic. Inform. and Comput. 137(1), 1–33 (1997)
Gentzen, G.: Untersuchungen über das logische Schließen. I. Math. Z. 39(2), 176–210 (1934)
Johansson, I.: Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compos. Math. 4, 119–136 (1937)
Lellmann, B., Pattinson, D.: Cut Elimination for Shallow Modal Logics. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 211–225. Springer, Heidelberg (2011)
Lellmann, B., Pattinson, D.: Sequent Systems for Lewis’ Conditional Logics. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol. 7519, pp. 320–332. Springer, Heidelberg (2012)
Lewis, D.: Counterfactuals. Blackwell (1973)
Mendler, M., Scheele, S.: Cut-free Gentzen calculus for multimodal CK. Inform. and Comput. 209, 1465–1490 (2011)
Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34, 507–544 (2005)
Negri, S., von Plato, J.: Structural proof theory. Cambridge University Press (2001)
Pattinson, D., Schröder, L.: Generic modal cut elimination applied to conditional logics. Log. Methods Comput. Sci. 7(1) (2011)
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Structures Comput. Sci. 11(4), 511–540 (2001)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts Theoret. Comput. Sci. Cambridge University Press (2000)
Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8. Springer (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lellmann, B., Pattinson, D. (2013). Constructing Cut Free Sequent Systems with Context Restrictions Based on Classical or Intuitionistic Logic. In: Lodaya, K. (eds) Logic and Its Applications. ICLA 2013. Lecture Notes in Computer Science, vol 7750. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36039-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-36039-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36038-1
Online ISBN: 978-3-642-36039-8
eBook Packages: Computer ScienceComputer Science (R0)