Subnets of proof-nets in MLL -
Gianluigi Bellin, J. Van de Wiele · 1995
The paper studies the properties of the subnets of proof-nets. Very simple proofs are obtained of known results on proof-nets for MLL \\Gamma , Multiplicative Linear Logic without propositional constants. Contents 1 Preface 1 2 Proof Nets for Propositional MLL \\Gamma 3 2.1 Propositional Proof Structures and Proof Nets : : : : : : : : : : 3 2.2 Subnets : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 2.3 Empires and Kingdoms: Existence and Properties : : : : : : : : 8 2.4 Sequentialization Theorem : : : : : : : : : : : : : : : : : : : : : 12 2.5 Permutability of Inferences in the Sequent Calculus : : : : : : : 13 3 Proof Nets for First Order MLL \\Gamma 15 3.1 First-Order Proof-Structures : : : : : : : : : : : : : : : : : : : : 15 3.2 Subnets : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 18 3.3 Empires and Kingdoms: Existence and Properties : : : : : : : : 19 3.4 Sequentialization : : : : : : : : : : : : : : : : : : : : : : : : : : 21 3.5 Permutabi...