7 found
Order:
  1.  23
    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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  2.  1
    Sebastian Eberhard & Stefan Hetzl (2015). Inductive Theorem Proving Based on Tree Grammars. Annals of Pure and Applied Logic 166 (6):665-700.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  3.  2
    Stefan Hetzl, Alexander Leitsch & Daniel Weller (2011). CERES in Higher-Order Logic. Annals of Pure and Applied Logic 162 (12):1001-1034.
    We define a generalization of the first-order cut-elimination method CERES to higher-order logic. At the core of lies the computation of an set of sequents from a proof π of a sequent S. A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of π into a cut-free proof of S. An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  4.  9
    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)  
     
    Export citation  
     
    My bibliography  
  5.  2
    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)  
     
    Export citation  
     
    My bibliography  
  6.  4
    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)  
     
    Export citation  
     
    My bibliography  
  7.  0
    Stefan Hetzl (2009). Describing Proofs by Short Tautologies. Annals of Pure and Applied Logic 159 (1):129-145.
    Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology composed of instances of (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography