A New Linear Time Correctness Condition for Multiplicative Linear Logic
Logic in Computer Science
2020-11-24 v4
Abstract
In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared with previous linear time correctness conditions, our system is surprisingly simple and intuitively appealing.
Keywords
Cite
@article{arxiv.1902.09693,
title = {A New Linear Time Correctness Condition for Multiplicative Linear Logic},
author = {Satoshi Matsuoka},
journal= {arXiv preprint arXiv:1902.09693},
year = {2020}
}
Comments
Found an bug in the proof of the linear time claim in the second version. Adapted the algorithm in order to guarantee the linear time termination. Added an additional example