Document Open Access Logo

Combinatorial Flows and Their Normalisation

Author Lutz Straßburger

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.31.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • proof equivalence
  • cut elimination
  • substitution
  • deep inference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

This paper introduces combinatorial flows that generalize combinatorial proofs such that they also include cut and substitution as methods of proof compression. We show a normalization procedure for combinatorial flows, and how syntactic proofs are translated into combinatorial flows and vice versa.

Cite As Get BibTex

Lutz Straßburger. Combinatorial Flows and Their Normalisation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.31

Author Details

Lutz Straßburger

References

  1. Peter B. Andrews. Refutations by matings. IEEE Transactions on Computers, C-25:801-807, 1976. Google Scholar
  2. Gianluigi Bellin and Jacques van de Wiele. Subnets of proof-nets in MLL^-. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes, pages 249-270. Cambridge University Press, 1995. Google Scholar
  3. Wolfgang Bibel. On matrices with connections. Journal of the ACM, 28:633-645, 1981. Google Scholar
  4. Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001, volume 2250 of LNAI, pages 347-361. Springer, 2001. Google Scholar
  5. Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10(2):1-34, 2009. Article 14. Google Scholar
  6. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  7. Pierre-Louis Curien. Categorical combinators. Information and Control, 69(1-3):188-254, 1986. URL: http://dx.doi.org/10.1016/S0019-9958(86)80047-X.
  8. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Annals of Mathematical Logic, 28:181-203, 1989. Google Scholar
  9. Anupam Das. Rewriting with linear inferences in propositional logic. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications (RTA), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 158-173. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  10. R. J. Duffin. Topology of series-parallel networks. Journal of Mathematical Analysis and Applications, 10(2):303-318, 1965. Google Scholar
  11. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  12. Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1:9):1-36, 2008. URL: http://arxiv.org/abs/0709.1205.
  13. Alessio Guglielmi, Tom Gundersen, and Lutz Straßburger. Breaking paths in atomic flows for classical logic. In LICS 2010, 2010. Google Scholar
  14. Willem Heijltjes and Lutz Straßburger. Proof nets and semi-star-autonomous categories. Mathematical Structures in Computer Science, 26(5):789-828, 2016. URL: http://dx.doi.org/10.1017/S0960129514000395.
  15. Dominic Hughes. Simple multiplicative proof nets with units. Preprint, 2005. URL: http://arxiv.org/abs/math.CT/0507003.
  16. Dominic Hughes. Proofs Without Syntax. Annals of Mathematics, 164(3):1065-1076, 2006. Google Scholar
  17. Dominic Hughes. Towards Hilbert’s 24^th problem: Combinatorial proof invariants: (preliminary version). Electr. Notes Theor. Comput. Sci., 165:37-63, 2006. Google Scholar
  18. Dominic Hughes. First-order proofs without syntax. Berkeley Logic Colloquium, 2014. Google Scholar
  19. Gregory Maxwell Kelly and Saunders Mac Lane. Coherence in closed categories. J. of Pure and Applied Algebra, 1:97-140, 1971. Google Scholar
  20. Jan Krajíček and Pavel Pudlák. Propositional proof systems, the consistency of first order theories and the complexity of computations. The Journal of Symbolic Logic, 54(3):1063-1079, 1989. Google Scholar
  21. François Lamarche and Lutz Straßburger. Naming proofs in classical propositional logic. In Paweł Urzyczyn, editor, TLCA'05, volume 3461 of LNCS, pages 246-261. Springer, 2005. URL: http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf.
  22. Olivier Laurent. Polarized proof-nets: proof-nets for LC (extended abstract). In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications (TLCA 1999), volume 1581 of LNCS, pages 213-227. Springer, 1999. Google Scholar
  23. Dale Miller. A proposal for broad spectrum proof certificates. In J.-P. Jouannaud and Z. Shao, editors, CPP: First International Conference on Certified Programs and Proofs, volume 7086 of Lecture Notes in Computer Science, pages 54-69, 2011. Google Scholar
  24. Rolf H. Möhring. Computationally tractable classes of ordered sets. In I. Rival, editor, Algorithms and Order, pages 105-194. Kluwer Acad. Publ., 1989. Google Scholar
  25. Novak Novakovic and Lutz Straßburger. On the power of substitution in the calculus of structures. ACM Trans. Comput. Log., 16(3):19, 2015. Google Scholar
  26. Christian Retoré. Réseaux et Séquents Ordonnés. PhD thesis, Université Paris VII, 1993. Google Scholar
  27. Christian Retoré. Handsome proof-nets: perfect matchings and cographs. Theoretical Computer Science, 294(3):473-488, 2003. Google Scholar
  28. Edmund P. Robinson. Proof nets for classical logic. Journal of Logic and Computation, 13:777-797, 2003. Google Scholar
  29. Lutz Straßburger. From deep inference to proof nets via cut elimination. Journal of Logic and Computation, 21(4):589-624, 2011. Google Scholar
  30. Lutz Straßburger. Extension without cut. Annals of Pure and Applied Logic, 163(12):1995-2007, 2012. Google Scholar
  31. Lutz Straßburger. Combinatorial Flows and Proof Compression. Research Report RR-9048, Inria Saclay, 2017. URL: https://hal.inria.fr/hal-01498468.
  32. Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, second edition, 2000. Google Scholar
  33. G. S. Tseitin. On the complexity of derivation in propositional calculus. Zapiski Nauchnykh Seminarou LOMI, 8:234-259, 1968. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact