Least and Greatest Fixed Points in Linear Logic

Details Least and Greatest Fixed Points in Linear Logic Least and Greatest Fixed Points in Linear Logic

2009-10-19

arxiv.org/abs/0910.3383v4

Computer Science

Logic in Computer Science

Accepted for publication at the ACM Transactions on Computational Logic

Scientific paper

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call muMALL, satisfies two fundamental proof theoretic properties: we establish weak normalization for it, and we design a focused proof system that we prove complete. That second result provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We show how these foundations can be applied to intuitionistic logic.

Affiliated with

Also associated with

No associations

Rating

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

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-715928