27 found
Sort by:
  1. Klaus Ambos-Spies, Arnold Beckmann, Samuel R. Buss & Benedikt Löwe (2012). Computability in Europe 2009. Annals of Pure and Applied Logic 163 (5):483-484.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Samuel R. Buss (2012). Sharpened Lower Bounds for Cut Elimination. Journal of Symbolic Logic 77 (2):656-668.
    We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth d of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to d — 0(1). The proof method is based on more efficiently expressing the Gentzen-Solovay (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Samuel R. Buss (2012). Towards–Via Proof Complexity and Search. Annals of Pure and Applied Logic 163 (7):906-917.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Samuel R. Buss & Alan S. Johnson (2012). Propositional Proofs and Reductions Between NP Search Problems. Annals of Pure and Applied Logic 163 (9):1163-1182.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Samuel R. Buss & Roman Kuznets (2012). Lower Complexity Bounds in Justification Logic. Annals of Pure and Applied Logic 163 (7):888-905.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  6. Samuel R. Buss & Alan S. Johnson (2010). The Quantifier Complexity of Polynomial‐Size Iterated Definitions in First‐Order Logic. Mathematical Logic Quarterly 56 (6):573-590.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  7. Arnold Beckmann & Samuel R. Buss (2009). Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic. Journal of Mathematical Logic 9 (01):103-138.
  8. Samuel R. Buss (2009). Pool Resolution is NP-Hard to Recognize. Archive for Mathematical Logic 48 (8):793-798.
    A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  9. Samuel R. Buss, S. Barry Cooper, Benedikt Löwe & Andrea Sorbi (2009). Preface. Annals of Pure and Applied Logic 160 (3):229-230.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  10. Arnold Beckmann & Samuel R. Buss (2005). Separation Results for the Size of Constant-Depth Propositional Proofs. Annals of Pure and Applied Logic 136 (1-2):30-55.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. Arnold Beckmann, Samuel R. Buss & Chris Pollett (2003). Erratum to “Ordinal Notations and Well-Orderings in Bounded Arithmetic” [Annals of Pure and Applied Logic 120 (2003) 197–223]. [REVIEW] Annals of Pure and Applied Logic 123 (1-3):291.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  12. Arnold Beckmann, Chris Pollett & Samuel R. Buss (2003). Ordinal Notations and Well-Orderings in Bounded Arithmetic. Annals of Pure and Applied Logic 120 (1-3):197-223.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Samuel R. Buss, Alexander S. Kechris, Anand Pillay & Richard A. Shore (2001). The Prospects for Mathematical Logic in the Twenty-First Century. Bulletin of Symbolic Logic 7 (2):169-196.
    The four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  14. Samuel R. Buss & Pavel Pudlák (2001). On the Computational Content of Intuitionistic Propositional Proofs. Annals of Pure and Applied Logic 109 (1-2):49-64.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Samuel R. Buss (1999). Bounded Arithmetic, Proof Complexity and Two Papers of Parikh. Annals of Pure and Applied Logic 96 (1-3):43-55.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Samuel R. Buss (ed.) (1998). Handbook of Proof Theory. Elsevier.
    This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that the two introductory articles come first; (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  17. Samuel R. Buss (1997). Bounded Arithmetic, Cryptography and Complexity. Theoria 63 (3):147-167.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  18. Samuel R. Buss & Peter Clote (1996). Cutting Planes, Connectivity, and Threshold Logic. Archive for Mathematical Logic 35 (1):33-62.
    Originating from work in operations research the cutting plane refutation systemCP is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial sizeCP proofs are given for the undirecteds-t connectivity principle. The subsystemsCP q ofCP, forq≥2, are shown to be polynomially equivalent toCP, thus answering problem 19 from the list of open problems of [8]. We present a normal form theorem forCP (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  19. Samuel R. Buss (1995). Relating the Bounded Arithmetic and Polynomial Time Hierarchies. Annals of Pure and Applied Logic 75 (1-2):67-77.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  20. Samuel R. Buss (1995). Some Remarks on Lengths of Propositional Proofs. Archive for Mathematical Logic 34 (6):377-394.
    We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m d+1) symbols. We show that renaming (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  21. Samuel R. Buss & Aleksandar Ignjatović (1995). Unprovability of Consistency Statements in Fragments of Bounded Arithmetic. Annals of Pure and Applied Logic 74 (3):221-244.
    Samuel R. Buss and Aleksandar Ignjatović. Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  22. Samuel R. Buss (1994). On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetics. Journal of Symbolic Logic 59 (3):737-756.
    This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact. unbounded) proof speedup of (i + 1)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and · as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  23. Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
    We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  24. Samuel R. Buss (1993). Intuitionistic Validity in T-Normal Kripke Structures. Annals of Pure and Applied Logic 59 (3):159-173.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. Samuel R. Buss (1991). Propositional Consistency Proofs. Annals of Pure and Applied Logic 52 (1-2):3-29.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Samuel R. Buss (1990). The Modal Logic of Pure Provability. Notre Dame Journal of Formal Logic 31 (2):225-231.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  27. Samuel R. Buss (1987). Polynomial Size Proofs of the Propositional Pigeonhole Principle. Journal of Symbolic Logic 52 (4):916-927.
    Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation