Research

Classical proof forestry


Reference:

Heijltjes, W., 2010. Classical proof forestry. Annals of Pure and Applied Logic, 161 (11), 1346–1366.

Related documents:

[img]
Preview
PDF (author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (369kB) | Preview

    Official URL:

    http://dx.doi.org/10.1016/j.apal.2010.04.006

    Abstract

    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.

    Details

    Item Type Articles
    CreatorsHeijltjes, W.
    DOI10.1016/j.apal.2010.04.006
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementClassical_Proof_Forestry.pdf: NOTICE: this is the author’s version of a work that was accepted for publication in Annals of Pure and Applied Logic. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Annals of Pure and Applied Logic, vol 161, issue 11, 2010, DOI 10.1016/j.apal.2010.04.006
    RefereedYes
    StatusPublished
    ID Code32340

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...