FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
From Syntactic Proofs to Combinatorial Proofs

Authors: Matteo Acclavio and Lutz Strassburger

Paper Information

Title:From Syntactic Proofs to Combinatorial Proofs
Authors:Matteo Acclavio and Lutz Strassburger
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:sequent calculus, tableaux, combinatorial proofs, proof identity
Abstract:

ABSTRACT. In this paper we investigate Hughes' combinatorial proofs as 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, in particular, to compare proofs that are given in different formalisms.

Pages:16
Talk:Jul 15 16:00 (Session 107D: Logics, Frameworks and Proofs)
Paper: