Switch to: References

Add citations

You must login to add citations.
  1. Classical proof forestry.Willem Heijltjes - 2010 - Annals of Pure and Applied Logic 161 (11):1346-1366.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Canonical proof nets for classical logic.Richard McKinley - 2013 - Annals of Pure and Applied Logic 164 (6):702-732.
    Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check the correctness of a net (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation