6 found
Sort by:
  1. Matthias Baaz, Stefan Hetzl & Daniel Weller (2012). On the Complexity of Proof Deskolemization. Journal of Symbolic Logic 77 (2):669-686.
    We consider the following problem: Given a proof of the Skolemization of a formula F, what is the length of the shortest proof of F? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  2. Stefan Hetzl (2012). The Computational Content of Arithmetical Proofs. Notre Dame Journal of Formal Logic 53 (3):289-296.
    For any extension $T$ of $I\Sigma_{1}$ having a cut-elimination property extending that of $I\Sigma_{1}$ , the number of different proofs that can be obtained by cut elimination from a single $T$ -proof cannot be bound by a function which is provably total in $T$.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Matthias Baaz & Stefan Hetzl (2011). On the Non-Confluence of Cut-Elimination. Journal of Symbolic Logic 76 (1):313 - 340.
    We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. Stefan Hetzl, Alexander Leitsch & Daniel Weller (2011). CERES in Higher-Order Logic. Annals of Pure and Applied Logic 162 (12):1001-1034.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Stefan Hetzl (2010). On the Form of Witness Terms. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Stefan Hetzl (2009). Describing Proofs by Short Tautologies. Annals of Pure and Applied Logic 159 (1):129-145.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation