Dominic J. D. Hughes
ABSTRACT
Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's extension to MLL1 (first-order MLL) fails to be canonical because of redundant existential witnesses, and present canonical MLL1 proof nets called unification nets without them. For example, while there are infinitely many cut-free Girard nets ∀x Px ⊢ ∃x Px, one per arbitrary witness for ∃x, there is a unique cut-free unification net, with no specified witness.
Cut elimination for unification nets is local and linear time, while Girard's is non-local and exponential time. Since some unification nets are exponentially smaller than corresponding Girard nets and sequent proofs, technical delicacy is required to ensure correctness is polynomial-time (quadratic).
These results transcend MLL1 via a methodological insight: for canonical quantifiers, the standard parallel/sequential dichotomy of proof nets is insufficient; an implicit/explicit witness dichotomy is needed. Current work extends unification nets to additives and uses them to extend combinatorial proofs [Proofs without syntax, Annals of Mathematics, 2006] to classical first-order logic.
- P. B. Andrews. 1981. Theorem Proving via General Matings. J. ACM 28 (1981). Google Scholar
Digital Library
- G. Bellin and J. van de Wiele. 1995. Subnets of proof-nets in MLL---. In Advances in Linear Logic. Cambridge University Press, Cambridge, U.K. Google ScholarDigital Library
- W. Bibel. 1981. On Matrices with Connections. J. ACM 28, 4 (1981). Google ScholarDigital Library
- A. Carbone. 2010. A New Mapping Between Combinatorial Proofs and Sequent Calculus Proofs Read out from Logical Flow Graphs. Inf. Comput. 208, 5 (2010). Google ScholarDigital Library
- S. A. Cook and R. A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symb. Logic 44 (1979), 36--50. Issue 1.Google ScholarCross Ref
- V. Danos. 1990. La logique linéaire appliquée à l'étude de divers processus de normal. et princip. du lambda calcul. Ph.D. Dissertation. Univ. de Paris.Google Scholar
- V. Danos and L. Regnier. 1989. The Structure of Multiplicatives. Archive for Mathematical Logic 28 (1989), 181--203.Google ScholarCross Ref
- J.-Y. Girard. 1987. Linear Logic. Theor. Comp. Sci. 50 (1987), 1--102. Google ScholarDigital Library
- J.-Y. Girard. 1988. Quantifiers in linear logic. In Temi e prospettive della logica e della filosofia della scienza contemporanee, Vol. 1. CLUEB, Bologna.Google Scholar
- J.-Y. Girard. 1991. Quantifiers in linear logic II. Nuovi problemi della logica e della filosofia della scienza 2 (1991).Google Scholar
- J.-Y. Girard. 1996. Proof-nets: the parallel syntax for proof theory. In Logic and Algebra. Lec. Notes In Pure and Applied Math., Vol. 180.Google Scholar
- J.-Y. Girard. 2011. The Blind Spot: Lectures on Logic. European Math. Soc.Google Scholar
- S. Guerrini. 1999. Correctness of Multiplicative Proof Nets Is Linear. In Proc. Logic in Computer Science '99. Google ScholarDigital Library
- W. Heijltjes. 2010. Classical proof forestry. Annals of Pure and Applied Logic 161, 11 (2010).Google ScholarCross Ref
- J. Herbrand. 1930. Recherches sur la théorie de la démonstration. Ph.D. Dissertation. Sorbonne, Paris.Google Scholar
- D. J. D. Hughes. 2006. Proofs without syntax. Annals of Mathematics 143 (2006), 1065--1076. Issue 3.Google ScholarCross Ref
- D. J. D. Hughes. 2006. Towards Hilbert's 24th Problem: Combinatorial Proof Invariants. In Proc. WOLLiC'06 (Lec. Notes in Comp. Sci), Vol. 165. Google ScholarDigital Library
- D. J. D. Hughes. 2014. First-order Proofs Without Syntax. (2014). Slides for the Berkeley Logic Colloquium, October 17, 2014. http://boole.stanford.edu/~dominic/papers/fopws-blc-2014.Google Scholar
- D. J. D. Hughes and R. J. van Glabbeek. 2003. Proof nets for unit-free multiplicative additive linear logic (Extended abstract). In Proc. Logic in Comp. Sci. '03. Google ScholarDigital Library
- D. J. D. Hughes and R. J. van Glabbeek. 2005. Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. Comput. Log. 6 (2005). Google ScholarDigital Library
- J.-L. Lassez, M. J. Maher, and K. Marriott. 1988. Unification revisited. In Foundations of deductive databases and logic programming. Google ScholarDigital Library
- A. Martelli and U. Montanari. 1976. Unification in linear time and space: a structured presentation. Technical Report B76-16. University of Pisa.Google Scholar
- R. McKinley. 2010. Expansion nets: Proof nets for for propositional classical logic. In LPAR 17 (Lec. Notes in Comp. Sci.), Vol. 6397. Google ScholarDigital Library
- D. A. Miller. 1984. Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. Lec. Notes in Comp. Sci. 170 (1984). Google ScholarDigital Library
- R. Moot. 2002. Proof nets for lingusitic analysis. Ph.D. Dissertation. Utrecht.Google Scholar
- D. Prawitz. 1970. A proof procedure with matrix reduction. Lecture Notes in Mathematics 125 (1970).Google ScholarCross Ref
- W. V Quine. 1955. A proof procedure for quantification theory. J. Symbolic Logic 20, 2 (1955).Google ScholarCross Ref
- J. A. Robinson. 1965. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12, 1 (1965). Google ScholarDigital Library
- L. Straßburger. 2009. Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic. In TLCA '09. Google ScholarDigital Library
- L. Straßburger. 2017. Combinatorial Flows and Their Normalisation. In Proc. FSCD 2017 (Leibniz Int. Proc. Informal), Vol. 84.Google Scholar
Recommendations
Conflict nets: Efficient locally canonical MALL proof nets
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceProof nets for MLL (unit-free multiplicative linear logic) and ALL (unit-free additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canonical (invariant under rule commutation). This paper ...
Intuitionistic differential nets and lambda-calculus
We define pure intuitionistic differential proof nets, extending Ehrhard and Regnier s differential interaction nets with the exponential box of Linear Logic. Normalization of the exponential reduction and confluence of the full one is proved. These ...
Proof nets for unit-free multiplicative-additive linear logic
A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential rule commutation. The only known extension to additives, based on monomial weights, fails to ...
Comments