Structural Complexity of Proofs (1974) is the title of a Ph.D. thesis by Richard Statman, who was a student of Georg Kreisel at Stanford University. Among other contributions, the thesis is notable for defining a notion of “genus of a proof”, as a global measure of complexity more interesting than (but analogous to) number of inferences, depth of the proof tree, etc.
Any proof in natural deduction induces a rooted tree, by representing the judgments occurring in the proof as nodes (note that different occurrences of the same judgment are represented as distinct nodes), and drawing a directed edge
just in case occurs as a premise of the inference rule with conclusion . This rooted tree can then be turned into a directed graph by adding more edges
just in case the assumption is discharged by the inference rule with conclusion (see natural deduction: hypothetical reasoning?).
The genus of the proof is then defined to be the graph genus of , i.e., the minimal genus of a surface in which embeds without crossing edges.
Richard Statman. Structural Complexity of Proofs, Ph.D. Thesis (1974), Stanford University.
Alessandra Carbone. Logical structures and the genus of proofs, APAL 161:2, 2009. (doi)
Last revised on March 10, 2015 at 11:58:44. See the history of this page for a list of all contributions to it.