Switch to: References

Add citations

You must login to add citations.
  1. Bounded Arithmetic, Proof Complexity and Two Papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.
  • 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   11 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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark