TY - GEN
T1 - A local system for linear logic
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002/1/1
Y1 - 2002/1/1
N2 - In this paper I will present a deductive system for linear logic, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. In order to achieve this, it is necessary to depart from the sequent calculus and use the calculus of structures, which is a generalization of the one-sided sequent calculus. In a rule, premise and conclusion are not sequents, but structures, which are expressions that share properties of formulae and sequents.
AB - In this paper I will present a deductive system for linear logic, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. In order to achieve this, it is necessary to depart from the sequent calculus and use the calculus of structures, which is a generalization of the one-sided sequent calculus. In a rule, premise and conclusion are not sequents, but structures, which are expressions that share properties of formulae and sequents.
M3 - Conference contribution
AN - SCOPUS:84954416508
SN - 3540000100
SN - 9783540000105
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 388
EP - 402
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR 2002, Proceedings
A2 - Voronkov, Andrei
A2 - Baaz, Matthias
PB - Springer Verlag
T2 - 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002
Y2 - 14 October 2002 through 18 October 2002
ER -