Logical structures and genus of proofs

Annals of Pure and Applied Logic 161 (2):139-149 (2010)
  Copy   BIBTEX

Abstract

Any arbitrarily complicated non-oriented graph, that is a graph of arbitrarily large genus, can be encoded in a cut-free proof. This unpublished result of Statman was shown in the early seventies. We provide a proof of it, and of a number of other related facts

Categories

Keywords

Reprint years

2009

DOI

10.1016/j.apal.2009.05.007

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,774

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Interpolants, cut elimination and flow graphs for the propositional calculus.Alessandra Carbone - 1997 - Annals of Pure and Applied Logic 83 (3):249-299.
Extension without cut.Lutz Straßburger - 2012 - Annals of Pure and Applied Logic 163 (12):1995-2007.
CERES in higher-order logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
Uncountable categoricity of local abstract elementary classes with amalgamation.John T. Baldwin & Olivier Lessmann - 2006 - Annals of Pure and Applied Logic 143 (1-3):29-42.
Logical aspects of Cayley-graphs: the group case.Dietrich Kuske & Markus Lohrey - 2004 - Annals of Pure and Applied Logic 131 (1-3):263-286.
A graph which embeds all small graphs on any large set of vertices.S. Shelah - 1988 - Annals of Pure and Applied Logic 38 (2):171-183.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
Cut normal forms and proof complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.
Cut elimination for the unified logic.Jacqueline Vauzeilles - 1993 - Annals of Pure and Applied Logic 62 (1):1-16.
The additive multiboxes.Lorenzo Tortora de Falco - 2003 - Annals of Pure and Applied Logic 120 (1-3):65-102.

Analytics

Added to PP
2013-12-22

Downloads
29 (#135,560)

6 months
7 (#1,397,300)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

The undecidability of k-provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
Duplication of directed graphs and exponential blow up of proofs.A. Carbone - 1999 - Annals of Pure and Applied Logic 100 (1-3):1-67.
The undecidability of k-provability.Samuel Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.

Add more references