Fast verification of MLL proof nets via IMLL
Andrzej S. Murawski, C.-H. Luke Ong · ACM Transactions on Computational Logic · 2006
We consider the following decision problems:ProofNet: Is a given multiplicative linear logic (MLL) proof structure a proof net?EssNet: Is a given essential net (of an intuitionistic MLL sequent) correct?In this article we show how to obtain linear-time algorithms for EssNet. As a corollary, by showing that ProofNet is linear-time reducible to EssNet (by the Trip Translation), we obtain a linear-time algorithm for ProofNet.We show further that it is possible to optimize the verification so that each node of the input structure is visited at most once. Finally, we present linear-time algorithms for sequentializing proof nets and essential nets, that is, for finding derivations of the underlying sequents.