This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2011 IEEE 26th Annual Symposium on Logic in Computer Science
Proof Nets for Additive Linear Logic with Units
Toronto, Ontario Canada
June 21-June 24
ISBN: 978-0-7695-4412-0
Additive linear logic, the fragment of linear logic concerning linear implication between strictly additive formulae, coincides with sum-product logic, the internal language of categories with free finite products and co products. Deciding equality of its proof terms, as imposed by the categorical laws, is complicated by the presence of the units (the initial and terminal objects of the category) and the fact that in a free setting products and co products do not distribute. The best known desicion algorithm, due to Cockett and Santocanale (CSL 2009), is highly involved, requiring an intricate case analysis on the syntax of terms. This paper provides canonical, graphical representations of the categorical morphisms, yielding a novel solution to this decision problem. Starting with (a modification of) existing proof nets, due to Hughes and Van Glabbeek, for additive linear logic without units, canonical forms are obtained by graph rewriting. The rewriting algorithm is remarkably simple. As a decision procedure for term equality it matches the known complexity of the problem. A main technical contribution of the paper is the substantial correctness proof of the algorithm.
Index Terms:
proof nets, linear logic, graph rewriting
Citation:
Willem Heijltjes, "Proof Nets for Additive Linear Logic with Units," lics, pp.207-216, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2011
Usage of this product signifies your acceptance of the Terms of Use.