From Syntactic Proofs to Combinatorial Proofs

Abstract : In this paper we investigate Hughes’ combinatorial proofs as a notion of proof identity for classical logic. We show for various syntactic formalisms including sequent calculus, analytic tableaux, and resolution, how they can be translated into combinatorial proofs, and which notion of identity they enforce. This allows the comparison of proofs that are given in different formalisms.
Document type :
Book sections
Complete list of metadatas

https://hal.inria.fr/hal-01942275
Contributor : Lutz Straßburger <>
Submitted on : Monday, December 3, 2018 - 9:58:08 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Monday, March 4, 2019 - 1:01:37 PM

File

tableau-def.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01942275, version 1

Citation

Matteo Acclavio, Lutz Straßburger. From Syntactic Proofs to Combinatorial Proofs. International Joint Conference on Automated Reasoning, IJCAR 2018, Springer, pp.481-497, 2018, 978-3-319-94204-9. ⟨hal-01942275⟩

Share

Metrics

Record views

79

Files downloads

59