A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version

Details A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version

2007-04-13

arxiv.org/abs/0704.1707v2

Computer Science

Logic in Computer Science

Scientific paper

Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ``cut-free'' sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees. Our simple termination argument allows our calculus to be used for automated deduction, although this is not its main purpose.

Affiliated with

Also associated with

No associations

Rating

A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version 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 A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-678143