Linear Time Proof Verification on N-Graphs: A Graph Theoretic Approach.

This paper presents a linear time algorithm for proof verification on N-Graphs. This system, introduced by de Oliveira, incorporates the geometrical techniques from the theory of proof-nets to present a multiple-conclusion calculus for classical propositional logic. The soundness criterion is based on the one given by Danos and Regnier for Linear Logic. We use a DFS-like search to check the validity of the cycles in a proof graph, and some properties from trees to check the connectivity of every switching a concept similar to D-R graph. Since the soundness criterion in proof graphs is analogous to Danos-Regnier's procedure, the algorithm can also be extended to check proofs in the multiplicative linear logic without units MLL - with linear time complexity.