A New Linear Time Correctness Condition for Multiplicative Linear Logic

2019/02/26 by Satoshi Matsuoka, Matsuoka, Satoshi
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1902.09693

openalex publication_date 2019/02/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• The structure of multiplicatives
• Linear logic

Related

• Simple multiplicative proof nets with units
• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• Linear Realisability over nets: multiplicatives (long version)
• On the role of connectivity in Linear Logic proofs
• Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)