Focusing and Polarization in Intuitionistic Logic

Details Focusing and Polarization in Intuitionistic Logic Focusing and Polarization in Intuitionistic Logic

2007-08-16

arxiv.org/abs/0708.2252v1

Dans Computer Science Logic (2007)

Computer Science

Logic in Computer Science

Scientific paper

A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.

Affiliated with

Also associated with

No associations

Rating

Focusing and Polarization in Intuitionistic Logic 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 Focusing and Polarization in Intuitionistic Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Focusing and Polarization in Intuitionistic Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-333028