A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic

We give a graph theoretical criterion on multiplicative additive linear logic (MALL) cut-free proof structures that exactly characterizes those whose interpretation is a hyperclique in Ehrhard's hypercoherent spaces. This criterion is strictly weaker than the one given by Hughes and van Glabbeek characterizing proof nets (i.e. desequentialized sequent calculus proofs). We thus also give the first proof of semantical soundness of hypercoherent spaces with respect to proof nets entirely based on graph theoretical trips, in the style of Girard's proof of semantical soundness of coherent spaces for proof nets of the multiplicative fragment of linear logic.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Paolo Tranquilli
• Keywords: Automated Reasoning, CSL 2008, Cut-free Proof Structures, Proof Nets, Semantical Soundness