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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Note that this is only a cosmetic limitation. The theory of combinatorial proofs can easily be extended to the full language including implication and general negation.
- 3.
It cannot happen that both \(\varGamma \) and \(\varDelta \) are empty.
References
Bellin, G., van de Wiele, J.: Subnets of proof-nets in MLL\(^-\). In: Advances in Linear Logic, pp. 249–270. Cambridge University Press (1995)
Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45653-8_24
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36–50 (1979)
Das, A.: On the relative proof complexity of deep inference via atomic flows. Log. Methods Comput. Sci. 11(1), 1–23 (2015)
Das, A., Straßburger, L.: On linear rewriting systems for Boolean logic and some applications to proof theory. Log. Methods Comput. Sci. 12(4), 1–27 (2016)
Duffin, R.: Topology of series-parallel networks. J. Math. Anal. Appl. 10(2), 303–318 (1965)
Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer Science & Business Media, Heidelberg (2012)
Gentzen, G.: Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift 39, 176–210 (1935)
Guglielmi, A., Straßburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54–68. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_5
Hughes, D.: Proofs Without Syntax. Ann. Math. 164(3), 1065–1076 (2006)
Hughes, D.: Towards Hilbert’s 24\({}^{\text{ th }}\) problem: combinatorial proof invariants: (preliminary version). Electr. Notes Theor. Comput. Sci. 165, 37–63 (2006)
Hughes, D.J.: Unification nets: canonical proof net quantifiers. In: LICS 2018 (2018)
Marin, S., Straßburger, L.: Label-free modular systems for classical and intuitionistic modal logics. In: Advances in Modal Logic 10 (2014)
Retoré, C.: Handsome proof-nets: perfect matchings and cographs. Theor. Comput. Sci. 294(3), 473–488 (2003)
Smullyan, R.M.: First-Order Logic. Courier Corporation, Massachusetts (1995)
Straßburger, L.: A characterization of medial as rewriting rule. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 344–358. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73449-9_26
Straßburger, L.: Combinatorial flows and proof compression. Research report RR-9048, Inria Saclay (2017). https://hal.inria.fr/hal-01498468
Straßburger, L.: Combinatorial flows and their normalisation. In: Miller, D. (ed.) FSCD 2017. LIPIcs, vol. 84, pp. 31:1–31:17. Schloss Dagstuhl (2017)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, vol. 43. Cambridge University Press, Cambridge (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Acclavio, M., Straßburger, L. (2018). From Syntactic Proofs to Combinatorial Proofs. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-94205-6_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94204-9
Online ISBN: 978-3-319-94205-6
eBook Packages: Computer ScienceComputer Science (R0)