Linear time proof verification on n-graphs: A graph theoretic approach

Abstract

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. © 2013 Springer-Verlag Berlin Heidelberg.