On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

Details On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

2011-03-28

arxiv.org/abs/1103.5286v2

LMCS 7 (2:8) 2011

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-7(2:8)2011

We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call "shallow calculi", where inference rules are only applied at the root node in a nested sequent. Our shallow calculi are extensions of Kashima's calculus for tense logic and share an essential characteristic with display calculi, namely, the presence of structural rules called "display postulates". Shallow calculi enjoy a simple cut elimination procedure, but are unsuitable for proof search due to the presence of display postulates and other structural rules. The second style of calculi uses deep-inference, whereby inference rules can be applied at any node in a nested sequent. We show that, for a range of extensions of tense logic, the two styles of calculi are equivalent, and there is a natural proof theoretic correspondence between display postulates and deep inference. The deep inference calculi enjoy the subformula property and have no display postulates or other structural rules, making them a better framework for proof search.

Affiliated with

Also associated with

No associations

Rating

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-706772