publication . Preprint . 2010

Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic

Gore, Rajeev; Postniece, Linda; Tiu, Alwen;
Open Access English
  • Published: 24 Jun 2010
Abstract
We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with typical inference rules for the modalities used in display logics. As it turns out, the resulting calculus, LBiKt, seems to be more basic than most intuitionistic tense or modal logics considered in the literature, in particular, those studied by Ewald and Simpson, as it does not assume any a priori relationship between the diamond and the box modal operators. We recover Ewald's intuitionistic tense logic and Simpson's intuitionist...
Subjects
acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Computer Science - Logic in Computer Science, F.4.1
Download from
24 references, page 1 of 2

[1] G. Amati and F. Pirri. A uniform tableau method for intuitionistic modal logics i. Studia Logica, 53(1):29-60, 1994.

[2] K Bru¨nnler and L Straßburger Modular Sequent Systems for Modal Logic In Proc. TABLEAUX, LNCS:5607;152-166. Springer, 2009. [OpenAIRE]

[3] M J Collinson, B. Hilken and D. Rydeheard. Semantics and proof theory of an intuitionistic modal sequent calculus. Technical report, University of Manchester, UK, 1999.

[4] T. Crolard. A formulae-as-types interpretation of Subtractive Logic. J. of Logic and Comput., 14(4):529-570, 2004.

[5] R. Davies and F. Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001.

[6] W. B. Ewald. Intuitionistic tense and modal logic. J. Symb. Log, 51(1):166-179, 1986.

[7] D. Galmiche and Y. Salhi. Calculi for an intuitionistic hybrid modal logic. In Proc. IMLA, 2008. [OpenAIRE]

[8] R. Gor´e. Substructural logics on display. Log. J of Interest Group in Pure and Applied Logic, 6(3):451- 504, 1998.

[9] R. Gor´e, L. Postniece, and A. Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Proc. AiML 7:43-66. College Publications, 2008. [OpenAIRE]

[10] R. Gor´e, L. Postniece, and A. Tiu. Taming displayed tense logics using nested sequents with deep inference. In Proc. TABLEAUX, LNCS:5607;189-204. Springer, 2009. [OpenAIRE]

[11] Y. Kakutani. Calculi for intuitionistic normal modal logic. In Proceedings of PPL 2007.

[12] R. Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53:119-135, 1994.

[13] A. Masini. 2-sequent calculus: Intuitionism and natural deduction. J. Log. Comput., 3(5):533-562, 1993.

[14] G Mints. On some calculi of modal logic. Proc. Steklov Inst. of Mathematics, 98:97-122, 1971.

[15] T. Murphy VII, K. Crary, R. Harper, and F. Pfenning. A symmetric modal lambda calculus for distributed computing. In LICS, pages 286-295, 2004.

24 references, page 1 of 2
Abstract
We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with typical inference rules for the modalities used in display logics. As it turns out, the resulting calculus, LBiKt, seems to be more basic than most intuitionistic tense or modal logics considered in the literature, in particular, those studied by Ewald and Simpson, as it does not assume any a priori relationship between the diamond and the box modal operators. We recover Ewald's intuitionistic tense logic and Simpson's intuitionist...
Subjects
acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Computer Science - Logic in Computer Science, F.4.1
Download from
24 references, page 1 of 2

[1] G. Amati and F. Pirri. A uniform tableau method for intuitionistic modal logics i. Studia Logica, 53(1):29-60, 1994.

[2] K Bru¨nnler and L Straßburger Modular Sequent Systems for Modal Logic In Proc. TABLEAUX, LNCS:5607;152-166. Springer, 2009. [OpenAIRE]

[3] M J Collinson, B. Hilken and D. Rydeheard. Semantics and proof theory of an intuitionistic modal sequent calculus. Technical report, University of Manchester, UK, 1999.

[4] T. Crolard. A formulae-as-types interpretation of Subtractive Logic. J. of Logic and Comput., 14(4):529-570, 2004.

[5] R. Davies and F. Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001.

[6] W. B. Ewald. Intuitionistic tense and modal logic. J. Symb. Log, 51(1):166-179, 1986.

[7] D. Galmiche and Y. Salhi. Calculi for an intuitionistic hybrid modal logic. In Proc. IMLA, 2008. [OpenAIRE]

[8] R. Gor´e. Substructural logics on display. Log. J of Interest Group in Pure and Applied Logic, 6(3):451- 504, 1998.

[9] R. Gor´e, L. Postniece, and A. Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Proc. AiML 7:43-66. College Publications, 2008. [OpenAIRE]

[10] R. Gor´e, L. Postniece, and A. Tiu. Taming displayed tense logics using nested sequents with deep inference. In Proc. TABLEAUX, LNCS:5607;189-204. Springer, 2009. [OpenAIRE]

[11] Y. Kakutani. Calculi for intuitionistic normal modal logic. In Proceedings of PPL 2007.

[12] R. Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53:119-135, 1994.

[13] A. Masini. 2-sequent calculus: Intuitionism and natural deduction. J. Log. Comput., 3(5):533-562, 1993.

[14] G Mints. On some calculi of modal logic. Proc. Steklov Inst. of Mathematics, 98:97-122, 1971.

[15] T. Murphy VII, K. Crary, R. Harper, and F. Pfenning. A symmetric modal lambda calculus for distributed computing. In LICS, pages 286-295, 2004.

24 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue