Projects per year

### Abstract

Proof nets for MLL (unit-free multiplicative linear logic) and (unit-free additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canoni- cal (invariant under rule commutation). This paper solves a three- decade open problem: are there efficient canonical proof nets for MALL (unit-free multiplicative-additive linear logic)?

Honouring MLL and ALL canonicity, in which all commutations are strictly local proof-tree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.

Honouring MLL and ALL canonicity, in which all commutations are strictly local proof-tree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.

Original language | English |
---|---|

Title of host publication | Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 |

Place of Publication | New York, U. S. A. |

Publisher | Association for Computing Machinery |

Pages | 437-446 |

Number of pages | 10 |

ISBN (Print) | 9781450343916 |

DOIs | |

Publication status | Published - 2 Jul 2016 |

Event | 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 - New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

Publisher | IEEE |

ISSN (Electronic) | 2575-5528 |

### Conference

Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 |
---|---|

Country | USA United States |

City | New York |

Period | 5/07/16 → 8/07/16 |

## Fingerprint Dive into the research topics of 'Conflict nets: efficient locally canonical MALL proof nets'. Together they form a unique fingerprint.

## Projects

- 2 Finished

### Efficient and Natural Proof Systems

Guglielmi, A., Bruscoli, P. & McCusker, G.

Engineering and Physical Sciences Research Council

1/02/13 → 12/05/16

Project: Research council

### COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Engineering and Physical Sciences Research Council

1/02/07 → 30/06/08

Project: Research council

## Profiles

## Cite this

Hughes, D., & Heijltjes, W. (2016). Conflict nets: efficient locally canonical MALL proof nets. In

*Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016*(pp. 437-446). (Proceedings - Symposium on Logic in Computer Science). Association for Computing Machinery. https://doi.org/10.1145/2933575.2934559