Switch to: References

Add citations

You must login to add citations.
  1. Duplication of directed graphs and exponential blow up of proofs.A. Carbone - 1999 - Annals of Pure and Applied Logic 100 (1-3):1-67.
    We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and lower bounds (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.
    We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions. Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only elementary cut-elimination.
    Download  
     
    Export citation  
     
    Bookmark  
  • The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
    The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...)
    Download  
     
    Export citation  
     
    Bookmark