On the Dependencies of Logical Rules.
Lecture Notes in Computer Science(2015)
摘要
Many correctness criteria have been proposed since linear logic was introduced and it is not clear how they relate to each other. In this paper, we study proof-nets and their correctness criteria from the perspective of dependency, as introduced by Mogbil and Jacobe de Naurois. We introduce a new correctness criterion, called DepGraph, and show that together with Danos' contractibility criterion and Mogbil and Naurois criterion, they form the three faces of a notion of dependency which is crucial for correctness of proof-structures. Finally, we study the logical meaning of the dependency relation and show that it allows to recover and characterize some constraints on the ordering of inferences which are implicit in the proof-net.
更多查看译文
关键词
Linear logic,MLL,Proof nets,Correctness criterion,Contractibility,Mogbil-Naurois Criterion,Permutability of inferences
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络