Classical proof forestry

Research output: Contribution to journalArticlepeer-review

17 Citations (SciVal)
185 Downloads (Pure)


Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.
This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.
Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising.
Original languageEnglish
Pages (from-to)1346–1366
Number of pages21
JournalAnnals of Pure and Applied Logic
Issue number11
Early online date6 Jun 2010
Publication statusPublished - Aug 2010


Dive into the research topics of 'Classical proof forestry'. Together they form a unique fingerprint.

Cite this