Proof-graphs for Minimal Implicational Logic

Marcela Quispe-Cruz
(PUC-Rio)
Edward Hermann Haeusler
(PUC-Rio)
Lew Gordeev
(Tubingen University, Ghent University, PUC-Rio)

It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The aim of this work is to study how to reduce the weight of propositional deductions. We present the formalism of proof-graphs for purely implicational logic, which are graphs of a specific shape that are intended to capture the logical structure of a deduction. The advantage of this formalism is that formulas can be shared in the reduced proof.

In the present paper we give a precise definition of proof-graphs for the minimal implicational logic, together with a normalization procedure for these proof-graphs. In contrast to standard tree-like formalisms, our normalization does not increase the number of nodes, when applied to the corresponding minimal proof-graph representations.

In Mauricio Ayala-Rincón, Eduardo Bonelli and Ian Mackie: Proceedings 9th International Workshop on Developments in Computational Models (DCM 2013), Buenos Aires, Argentina, 26 August 2013, Electronic Proceedings in Theoretical Computer Science 144, pp. 16–29.
Published: 30th March 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.144.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org