|
|
 |
 |
 |
|
 |
|
A Uniform Calculus for Linear Logic
A uniform calculus for linear logic is presented.
The calculus has the form of a natural deduction in sequent calculus style
with general introduction and elimination rules. General elimination rules
are motivated through an inversion principle, the dual form of which gives the
general introduction rules.
By restricting all the rules to their single-succedent versions, a uniform
calculus for intuitionistic linear logic is obtained.
The calculus encompasses both natural deduction
and sequent calculus that are obtained as special instances from the
uniform calculus. Other instances give all the invertibilities and partial
invertibilities for the sequent calculus rules of linear logic.
The calculus is normalizing and satisfies the subformula property for
normal derivations.
|
|
|
|
 |
|
 |