Skip to Main content Skip to Navigation
New interface
Book sections

From Syntactic Proofs to Combinatorial Proofs

Matteo Acclavio 1, 2, 3 Lutz Strassburger 1, 2, 3 
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 metadata
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, December 3, 2018 - 9:58:08 AM
Last modification on : Wednesday, February 2, 2022 - 3:55:18 PM
Long-term archiving on: : Monday, March 4, 2019 - 1:01:37 PM


Files produced by the author(s)


  • HAL Id : hal-01942275, version 1


Matteo Acclavio, Lutz Strassburger. 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⟩



Record views


Files downloads