Combinatorial Flows and Proof Compression

Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : This paper introduces the notion of combinatorial flows as a generalization of combinatorial proofs that also includes cut and substitution as methods of proof compression. We show a normalization procedure for combinatorial flows, and how syntactic proofs in sequent calculus, deep inference, and Frege systems are translated into combinatorial flows and vice versa.
Document type :
Reports
Liste complète des métadonnées

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-01498468
Contributor : Lutz Straßburger <>
Submitted on : Thursday, March 30, 2017 - 10:15:59 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM

File

RR-9048.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01498468, version 1

Citation

Lutz Straßburger. Combinatorial Flows and Proof Compression. [Research Report] RR-9048, Inria Saclay. 2017. ⟨hal-01498468⟩

Share

Metrics

Record views

604

Files downloads

457