Order:
Disambiguations
Samuel R. Buss [33]Sam Buss [17]Samuel Buss [3]
  1.  28
    Handbook of Proof Theory.Samuel R. Buss (ed.) - 1998 - 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  
     
    Export citation  
     
    Bookmark   15 citations  
  2.  5
    Relating the Bounded Arithmetic and Polynomial Time Hierarchies.Samuel R. Buss - 1995 - Annals of Pure and Applied Logic 75 (1-2):67-77.
    The bounded arithmetic theory S2 is finitely axiomatized if and only if the polynomial hierarchy provably collapses. If T2i equals S2i + 1 then T2i is equal to S2 and proves that the polynomial time hierarchy collapses to ∑i + 3p, and, in fact, to the Boolean hierarchy over ∑i + 2p and to ∑i + 1p/poly.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  3.  7
    Polynomial Size Proofs of the Propositional Pigeonhole Principle.Samuel R. Buss - 1987 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  4.  25
    Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic.Arnold Beckmann & Samuel R. Buss - 2009 - Journal of Mathematical Logic 9 (1):103-138.
  5.  8
    Fragments of Approximate Counting.Samuel R. Buss, Leszek Aleksander Kołodziejczyk & Neil Thapen - 2014 - Journal of Symbolic Logic 79 (2):496-525.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6. Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
    We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  30
    On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetics.Samuel R. Buss - 1994 - 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 (9 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  8.  12
    Safe Recursive Set Functions.Arnold Beckmann, Samuel R. Buss & Sy-David Friedman - 2015 - Journal of Symbolic Logic 80 (3):730-762.
  9.  6
    The Complexity of the Disjunction and Existential Properties in Intuitionistic Logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
    This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  10.  5
    On the Computational Content of Intuitionistic Propositional Proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
    The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic propositional calculus does (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  11.  5
    Intuitionistic Validity in T-Normal Kripke Structures.Samuel R. Buss - 1993 - Annals of Pure and Applied Logic 59 (3):159-173.
    Let T be a first-order theory. A T-normal Kripke structure is one in which every world is a classical model of T. This paper gives a characterization of the intuitionistic theory T of sentences intuitionistically valid in all T-normal Kripke structures and proves the corresponding soundness and completeness theorems. For Peano arithmetic , the theory PA is a proper subtheory of Heyting arithmetic , so HA is complete but not sound for PA-normal Kripke structures.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  12.  9
    Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.Samuel R. Buss & Aleksandar Ignjatović - 1995 - 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)  
     
    Export citation  
     
    Bookmark   6 citations  
  13.  8
    Propositional Consistency Proofs.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 52 (1-2):3-29.
    Partial consistency statements can be expressed as polynomial-size propositional formulas. Frege proof systems have polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size proofs of partial consistency of extended Frege proof systems if and only if Frege proof systems polynomially simulate extended Frege proof systems. We give a new proof of Reckhow's theorem that any two Frege proof systems p-simulate each other. The proofs depend on polynomial size propositional formulas defining the truth of propositional formulas. These are already known to (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  14.  42
    Bounded Arithmetic, Cryptography and Complexity.Samuel R. Buss - 1997 - Theoria 63 (3):147-167.
  15.  24
    Strong Isomorphism Reductions in Complexity Theory.Sam Buss, Yijia Chen, Jörg Flum, Sy-David Friedman & Moritz Müller - 2011 - Journal of Symbolic Logic 76 (4):1381-1402.
    We give the first systematic study of strong isomorphism reductions, a notion of reduction more appropriate than polynomial time reduction when, for example, comparing the computational complexity of the isomorphim problem for different classes of structures. We show that the partial ordering of its degrees is quite rich. We analyze its relationship to a further type of reduction between classes of structures based on purely comparing for every n the number of nonisomorphic structures of cardinality at most n in both (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  6
    Separation Results for the Size of Constant-Depth Propositional Proofs.Arnold Beckmann & Samuel R. Buss - 2005 - Annals of Pure and Applied Logic 136 (1-2):30-55.
    This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  17.  19
    The Quantifier Complexity of Polynomial‐Size Iterated Definitions in First‐Order Logic.Samuel R. Buss & Alan S. Johnson - 2010 - Mathematical Logic Quarterly 56 (6):573-590.
    We refine the constructions of Ferrante-Rackoff and Solovay on iterated definitions in first-order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier-free case and in the case of purely existential or universal quantifiers, we show that Ω quantifiers (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  18.  25
    Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  19.  30
    The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  20.  22
    The Modal Logic of Pure Provability.Samuel R. Buss - 1990 - Notre Dame Journal of Formal Logic 31 (2):225-231.
  21. The Superjump in Martin-Löf Type Theory.Michael Rathjen & Samuel R. Buss - 2002 - Bulletin of Symbolic Logic 8 (4):538-538.
  22.  18
    Cutting Planes, Connectivity, and Threshold Logic.Samuel R. Buss & Peter Clote - 1996 - 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  23.  24
    The Prospects for Mathematical Logic in the Twenty-First Century.Samuel R. Buss, Alexander S. Kechris, Anand Pillay & Richard A. Shore - 2001 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  24.  4
    Ordinal Notations and Well-Orderings in Bounded Arithmetic.Arnold Beckmann, Chris Pollett & Samuel R. Buss - 2003 - Annals of Pure and Applied Logic 120 (1-3):197-223.
    This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  21
    Propositional Proofs and Reductions Between NP Search Problems.Samuel R. Buss & Alan S. Johnson - 2012 - Annals of Pure and Applied Logic 163 (9):1163-1182.
  26.  20
    Probabilistic Algorithmic Randomness.Sam Buss & Mia Minnes - 2013 - Journal of Symbolic Logic 78 (2):579-601.
    We introduce martingales defined by probabilistic strategies, in which randomness is used to decide whether to bet. We show that different criteria for the success of computable probabilistic strategies can be used to characterize ML-randomness, computable randomness, and partial computable randomness. Our characterization of ML-randomness partially addresses a critique of Schnorr by formulating ML randomness in terms of a computable process rather than a computably enumerable function.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  27.  30
    Sharpened Lower Bounds for Cut Elimination.Samuel R. Buss - 2012 - 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 (6 more)  
     
    Export citation  
     
    Bookmark  
  28.  16
    Lower Complexity Bounds in Justification Logic.Samuel R. Buss & Roman Kuznets - 2012 - Annals of Pure and Applied Logic 163 (7):888-905.
  29.  14
    Pool Resolution is NP-Hard to Recognize.Samuel R. Buss - 2009 - 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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  30.  12
    Towards–Via Proof Complexity and Search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.
  31.  10
    Computability in Europe 2011.Sam Buss, Benedikt Löwe, Dag Normann & Ivan Soskov - 2013 - Annals of Pure and Applied Logic 164 (5):509-510.
  32.  10
    University of California, Irvine Irvine, California March 27–30, 2008.Sam Buss, Stephen Cook, José Ferreirós, David Marker, Theodore Slaman & Jamie Tappenden - 2008 - Bulletin of Symbolic Logic 14 (3).
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  33.  9
    Erratum to “Ordinal Notations and Well-Orderings in Bounded Arithmetic” [Annals of Pure and Applied Logic 120 197–223]. [REVIEW]Arnold Beckmann, Samuel R. Buss & Chris Pollett - 2003 - Annals of Pure and Applied Logic 123 (1-3):291.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34.  6
    Book Review: Matthias Baaz and Alexander Leitsch, Methods of Cut-Elimination. [REVIEW]Sam Buss - 2015 - Studia Logica 103 (3):663-667.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35.  5
    University of Sao Paulo (Sao Paulo), Brazil, July 28–31, 1998.Sergei Artemov, Sam Buss, Edmund Clarke Jr, Heinz Dieter Ebbinghaus, Hans Kamp, Phokion Kolaitis, Maarten de Rijke & Valeria de Paiva - 1999 - Bulletin of Symbolic Logic 5 (3).
    Direct download  
     
    Export citation  
     
    Bookmark  
  36.  5
    Bounded Arithmetic, Proof Complexity and Two Papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.
  37.  3
    Quasipolynomial Size Frege Proofs of Frankl’s Theorem on the Trace of Sets.James Aisenberg, Maria Luisa Bonet & Sam Buss - 2016 - Journal of Symbolic Logic 81 (2):687-710.
  38.  3
    Cobham Recursive Set Functions.Arnold Beckmann, Sam Buss, Sy-David Friedman, Moritz Müller & Neil Thapen - 2016 - Annals of Pure and Applied Logic 167 (3):335-369.
  39.  3
    Computability in Europe 2009.Klaus Ambos-Spies, Arnold Beckmann, Samuel R. Buss & Benedikt Löwe - 2012 - Annals of Pure and Applied Logic 163 (5):483-484.
  40.  2
    Review: Neil Immerman, Upper and Lower Bounds for First Order Expressibility; Neil Immerman, Relational Queries Computable in Polynomial Time; Neil Immerman, Languages That Capture Complexity Classes. [REVIEW]Samuel Buss - 1989 - Journal of Symbolic Logic 54 (1):287-288.
  41.  2
    Immerman Neil. Upper and Lower Bounds for First Order Expressibility. Journal of Computer and System Sciences, Vol. 25 (1982), Pp. 76–98. Immerman Neil. Relational Queries Computable in Polynomial Time. Information and Control, Vol. 68 (1986), Pp. 86–104. Immerman Neil. Languages That Capture Complexity Classes. SIAM Journal on Computing, Vol. 16 (1987), Pp. 760–778. [REVIEW]Samuel Buss - 1989 - Journal of Symbolic Logic 54 (1):287-288.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  42. 2008 Annual Meeting of the Association for Symbolic Logic-University of California, Irvine-Irvine, California-March 27-30, 2008-Abstracts. [REVIEW]Sam Buss, Stephen Cook, Jos Ferreirs, Andy Lewis, David Marker, Theodore Slaman & Jamie Tappenden - 2008 - Bulletin of Symbolic Logic 14 (3).
  43. 1998-99 Annual Meeting of the Association for Symbolic Logic.Sam Buss - 1999 - Bulletin of Symbolic Logic 5 (3):395-421.
  44. Preface.Samuel R. Buss, S. Barry Cooper, Benedikt Löwe & Andrea Sorbi - 2009 - Annals of Pure and Applied Logic 160 (3):229-230.
  45. REVIEWS-J. Krajíček, Forcing with Random Variables and Proof Complexity.Sam Buss - 2012 - Bulletin of Symbolic Logic 18 (4):576.
  46. Short Refutations for an Equivalence-Chain Principle for Constant-Depth Formulas.Sam Buss & Ramyaa Ramyaa - forthcoming - Mathematical Logic Quarterly.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark