Switch to: References

Add citations

You must login to add citations.
  1. The undecidability of k-provability.Samuel Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
    Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines. This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if and (...)
    Download  
     
    Export citation  
     
    Bookmark   26 citations  
  • Bounds for proof-search and speed-up in the predicate calculus.Richard Statman - 1978 - Annals of Mathematical Logic 15 (3):225.
    Download  
     
    Export citation  
     
    Bookmark   28 citations  
  • A Note on the Length of Proofs.Tsuyoshi Yukami - 1994 - Annals of the Japan Association for Philosophy of Science 8 (4):203-209.
    Download  
     
    Export citation  
     
    Bookmark  
  • A unification-theoretic method for investigating the k-provability problem.William M. Farmer - 1991 - Annals of Pure and Applied Logic 51 (3):173-214.
    The k-provability for an axiomatic system A is to determine, given an integer k 1 and a formula in the language of A, whether or not there is a proof of in A containing at most k lines. In this paper we develop a unification-theoretic method for investigating the k-provability problem for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata and a finite number of rules of inference. We show that the k-provability problem (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • The undecidability of k-provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
    Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines . This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Generalizing theorems in real closed fields.Matthias Baaz & Richard Zach - 1995 - Annals of Pure and Applied Logic 75 (1-2):3-23.
    Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A is provable in length k for all n ϵ ω , then A is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Bounded arithmetic, proof complexity and two papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Generalizing proofs in monadic languages.Matthias Baaz & Piotr Wojtylak - 2008 - Annals of Pure and Applied Logic 154 (2):71-138.
    This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.
    Download  
     
    Export citation  
     
    Bookmark  
  • Herbrand's theorem and term induction.Matthias Baaz & Georg Moser - 2006 - Archive for Mathematical Logic 45 (4):447-503.
    We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.
    Download  
     
    Export citation  
     
    Bookmark