The Polynomial Hierarchy and Fragments of Bounded Arithmetic (Extended Abstract) - Samuel R. Buss (STOC, 1985)

The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic. - Samuel R. Buss (SCT, 1986)

The Boolean Formula Value Problem Is in ALOGTIME - Samuel R. Buss (STOC, 1987)

Polynomial Size Proofs of the Propositional Pigeonhole Principle. - Samuel R. Buss (J. Symb. Log., 1987)

On truth-table reducibility to SAT and the difference hierarchy over NP. - Samuel R. Buss; Louise Hay (SCT, 1988)

Resolution Proofs of Generalized Pigeonhole Principles. - Samuel R. Buss; György Turán (Theor. Comput. Sci., 1988)

The Modal Logic of Pure Provability. - Samuel R. Buss (Notre Dame J. Formal Log., 1990)

On the Deduction Rule and the Number of Proof Lines - Maria Luisa Bonet; Samuel R. Buss (LICS, 1991)

Propositional Consistency Proofs. - Samuel R. Buss (Ann. Pure Appl. Log., 1991)

The Undecidability of k-Provability. - Samuel R. Buss (Ann. Pure Appl. Log., 1991)

On the Predictability of Coupled Automata: An Allegory about Chaos. - Samuel R. Buss; Christos H. Papadimitriou; John N. Tsitsiklis (Complex Syst., 1991)

On Truth-Table Reducibility to SAT - Samuel R. Buss; Louise Hay (Inf. Comput., 1991)

The Graph of Multiplication is Equivalent to Counting. - Samuel R. Buss (Inf. Process. Lett., 1992)

An Optimal Parallel Algorithm for Formula Evaluation. - Samuel R. Buss; Stephen A. Cook; A. Gupta; V. Ramachandran (SIAM J. Comput., 1992)

Intuitionistic Validity in T-Normal Kripke Structures. - Samuel R. Buss (Ann. Pure Appl. Log., 1993)

The Deduction Rule and Linear and Near-Linear Proof Simulations. - Maria Luisa Bonet; Samuel R. Buss (J. Symb. Log., 1993)

How to Lie Without Being (Easily) Convicted and the Length of Proofs in Propositional Calculus. - Pavel Pudlák; Samuel R. Buss (CSL, 1994)

On Herbrand's Theorem. - Samuel R. Buss (LCC, 1994)

Linear and O(n log n) Time Minimum-Cost Matching Algorithms for Quasi-Convex Tours. - Samuel R. Buss; Peter N. Yianilos (SODA, 1994)

Size-Depth Tradeoffs for Boolean Fomulae. - Maria Luisa Bonet; Samuel R. Buss (Inf. Process. Lett., 1994)

On Gödel's Theorems on Lenghts of Proofs I: Number of Lines and Speedup for Arithmetics. - Samuel R. Buss (J. Symb. Log., 1994)

Some remarks on lengths of propositional proofs. - Samuel R. Buss (Arch. Math. Log., 1995)

Relating the Bounded Arithmetic and Polynomial Time Hierarchies. - Samuel R. Buss (Ann. Pure Appl. Log., 1995)

Unprovability of Consistency Statements in Fragments of Bounded Arithmetic. - Samuel R. Buss; Aleksandar Ignjatovic (Ann. Pure Appl. Log., 1995)

The Serial Transitive Closure Problem for Trees. - Maria Luisa Bonet; Samuel R. Buss (SIAM J. Comput., 1995)

Lower bounds on Nullstellensatz proofs via designs. - Samuel R. Buss (Proof Complexity and Feasible Arithmetics, 1996)

Cutting planes, connectivity, and threshold logic. - Samuel R. Buss; Peter Clote (Arch. Math. Log., 1996)

Resolution and the Weak Pigeonhole Principle. - Samuel R. Buss; Toniann Pitassi (CSL, 1997)

Alogtime Algorithms for Tree Isomorphism, Comparison, and Canonization. - Samuel R. Buss (Kurt Gödel Colloquium, 1997)

Proof Complexity in Algebraic Systems and Bounded Depth Frege Systems with Modular Counting. - Samuel R. Buss; Russell Impagliazzo; Jan Krajícek; Pavel Pudlák; Alexander A. Razborov; Jirí Sgall (Comput. Complex., 1997)

Good Degree Bounds on Nullstellensatz Refutations of the Induction Principle. - Samuel R. Buss; Toniann Pitassi (J. Comput. Syst. Sci., 1998)

Linear and O(n log n) Time Minimum-Cost Matching Algorithms for Quasi-Convex Tours. - Samuel R. Buss; Peter N. Yianilos (SIAM J. Comput., 1998)

Linear Gaps Between Degrees for the Polynomial Calculus Modulo Distinct Primes (Abstract). - Samuel R. Buss; Dima Grigoriev; Russell Impagliazzo; Toniann Pitassi (CCC, 1999)

Bounded Arithmetic, Proof Complexity and Two Papers of Parikh. - Samuel R. Buss (Ann. Pure Appl. Log., 1999)

The Complexity of the Disjunction and Existential Properties in Intuitionistic Logic. - Samuel R. Buss; Grigori Mints (Ann. Pure Appl. Log., 1999)

Incompleteness of Behavioral Logics. - Samuel R. Buss; Grigore Rosu (CMCS, 2000)

On the computational content of intuitionistic propositional proofs. - Samuel R. Buss; Pavel Pudlák (Ann. Pure Appl. Log., 2001)

The prospects for mathematical logic in the twenty-first century. - Samuel R. Buss; Alexander S. Kechris; Anand Pillay; Richard A. Shore (Bull. Symb. Log., 2001)

Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. - Samuel R. Buss; Dima Grigoriev; Russell Impagliazzo; Toniann Pitassi (J. Comput. Syst. Sci., 2001)

Minimum Propositional Proof Length Is NP-Hard to Linearly Approximate. - Michael Alekhnovich; Samuel R. Buss; Shlomo Moran; Toniann Pitassi (J. Symb. Log., 2001)

Spherical averages and applications to spherical splines and interpolation. - Samuel R. Buss; Jay P. Fillmore (ACM Trans. Graph., 2001)

Resource-bounded continuity and sequentiality for type-two functionals. - Samuel R. Buss; Bruce M. Kapron (ACM Trans. Comput. Log., 2002)

Erratum to "Ordinal notations and well-orderings in bounded arithmetic" [Annals of Pure and Applied Logic 120 (2003) 197-223]. - Arnold Beckmann; Samuel R. Buss; Chris Pollett (Ann. Pure Appl. Log., 2003)

Ordinal notations and well-orderings in bounded arithmetic. - Arnold Beckmann; Chris Pollett; Samuel R. Buss (Ann. Pure Appl. Log., 2003)

A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. - Nathan Segerlind; Samuel R. Buss; Russell Impagliazzo (SIAM J. Comput., 2004)

Separation results for the size of constant-depth propositional proofs. - Arnold Beckmann; Samuel R. Buss (Ann. Pure Appl. Log., 2005)

Selectively Damped Least Squares for Inverse Kinematics. - Samuel R. Buss; Jin-Su Kim (J. Graph. Tools, 2005)

Collision detection with relative screw motion. - Samuel R. Buss (Vis. Comput., 2005)

Polynomial-size Frege and resolution proofs of st-connectivity and Hex tautologies. - Samuel R. Buss (Theor. Comput. Sci., 2006)

Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning. - Samuel R. Buss; Jan Hoffmann 002; Jan Johannsen (Log. Methods Comput. Sci., 2008)

The NP-hardness of finding a directed acyclic graph for regular resolution. - Samuel R. Buss; Jan Hoffmann 002 (Theor. Comput. Sci., 2008)

The NP-Completeness of Reflected Fragments of Justification Logics. - Samuel R. Buss; Roman Kuznets (LFCS, 2009)

Efficient Large-Scale Sweep and Prune Methods with AABB Insertion and Removal. - Daniel J. Tracy; Samuel R. Buss; Bryan M. Woods (VR, 2009)

Pool resolution is NP-hard to recognize. - Samuel R. Buss (Arch. Math. Log., 2009)

Preface. - Samuel R. Buss; S. Barry Cooper; Benedikt Löwe; Andrea Sorbi (Ann. Pure Appl. Log., 2009)

Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic. - Arnold Beckmann; Samuel R. Buss (J. Math. Log., 2009)

The quantifier complexity of polynomial-size iterated definitions in first-order logic. - Samuel R. Buss; Alan S. Johnson (Math. Log. Q., 2010)

Strong isomorphism reductions in complexity theory. - Sam Buss; Yijia Chen 001; Jörg Flum; Sy-David Friedman; Moritz Müller (J. Symb. Log., 2011)

Corrected upper bounds for free-cut elimination. - Arnold Beckmann; Samuel R. Buss (Theor. Comput. Sci., 2011)

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. - Maria Luisa Bonet; Samuel R. Buss (SAT, 2012)

Computability in Europe 2009. - Klaus Ambos-Spies; Arnold Beckmann; Samuel R. Buss; Benedikt Löwe (Ann. Pure Appl. Log., 2012)

Towards NP-P via proof complexity and search. - Samuel R. Buss (Ann. Pure Appl. Log., 2012)

Propositional proofs and reductions between NP search problems. - Samuel R. Buss; Alan S. Johnson (Ann. Pure Appl. Log., 2012)

Lower complexity bounds in justification logic. - Samuel R. Buss; Roman Kuznets (Ann. Pure Appl. Log., 2012)

Sharpened lower bounds for cut elimination. - Samuel R. Buss (J. Symb. Log., 2012)

3-D Computer Graphics. - Samuel R. Buss (Cambridge University Press, 2013)

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract). - Maria Luisa Bonet; Sam Buss (IJCAI, 2013)

Alternation Trading Proofs and Their Limitations. - Sam Buss (MFCS, 2013)

Computability in Europe 2011. - Sam Buss; Benedikt Löwe; Dag Normann; Ivan N. Soskov (Ann. Pure Appl. Log., 2013)

Probabilistic algorithmic randomness. - Sam Buss; Mia Minnes (J. Symb. Log., 2013)

Sub-computable Boundedness Randomness. - Sam Buss; Douglas Cenzer; Jeffrey B. Remmel (Log. Methods Comput. Sci., 2014)

Small Stone in Pool. - Samuel R. Buss; Leszek Aleksander Kolodziejczyk (Log. Methods Comput. Sci., 2014)

Improved Separations of Regular Resolution from Clause Learning Proof Systems. - Maria Luisa Bonet; Sam Buss; Jan Johannsen (J. Artif. Intell. Res., 2014)

Unshuffling a square is NP-hard. - Sam Buss; Michael Soltys (J. Comput. Syst. Sci., 2014)

Fragments of Approximate Counting. - Samuel R. Buss; Leszek Aleksander Kolodziejczyk; Neil Thapen (J. Symb. Log., 2014)

Improved witnessing and local improvement principles for second-order bounded arithmetic. - Arnold Beckmann; Samuel R. Buss (ACM Trans. Comput. Log., 2014)

Propositional Proofs in Frege and Extended Frege Systems (Abstract). - Sam Buss (CSR, 2015)

Limits on Alternation Trading Proofs for Time-Space Lower Bounds. - Samuel R. Buss; Ryan Williams 001 (Comput. Complex., 2015)

Safe Recursive Set Functions. - Arnold Beckmann; Samuel R. Buss; Sy-David Friedman (J. Symb. Log., 2015)

Book Review: Matthias Baaz and Alexander Leitsch, Methods of Cut-Elimination. - Sam Buss (Stud Logica, 2015)

Quasipolynomial size proofs of the propositional pigeonhole principle. - Sam Buss (Theor. Comput. Sci., 2015)

Cobham recursive set functions. - Arnold Beckmann; Sam Buss; Sy-David Friedman; Moritz Müller; Neil Thapen (Ann. Pure Appl. Log., 2016)

Expander Construction in VNC1. - Sam Buss; Valentine Kabanets; Antonina Kolokolova; Michal Koucký 001 (Electron. Colloquium Comput. Complex., 2016)

On Linear Resolution. - Sam Buss; Jan Johannsen (J. Satisf. Boolean Model. Comput., 2016)

Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Sets. - James Aisenberg; Maria Luisa Bonet; Sam Buss (J. Symb. Log., 2016)

Injection Structures Specified by Finite State Transducers. - Sam Buss; Douglas Cenzer; Mia Minnes; Jeffrey B. Remmel (Computability and Complexity, 2017)

Expander Construction in VNC1. - Sam Buss; Valentine Kabanets; Antonina Kolokolova; Michal Koucký 001 (ITCS, 2017)

Uniform proofs of ACC representations. - Sam Buss (Arch. Math. Log., 2017)

The NP Search Problems of Frege and Extended Frege Proofs. - Arnold Beckmann; Sam Buss (ACM Trans. Comput. Log., 2017)

MaxSAT Resolution With the Dual Rail Encoding. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; João Marques-Silva 001; António Morgado 001 (AAAI, 2018)

Reordering Rule Makes OBDD Proof Systems Stronger. - Sam Buss; Dmitry Itsykson; Alexander Knop; Dmitry Sokolov 001 (Electron. Colloquium Comput. Complex., 2018)

Short proofs of the Kneser-Lovász coloring principle. - James Aisenberg; Maria Luisa Bonet; Sam Buss; Adrian Craciun; Gabriel Istrate (Inf. Comput., 2018)

Short refutations for an equivalence-chain principle for constant-depth formulas. - Sam Buss; Ramyaa Ramyaa (Math. Log. Q., 2018)

DRAT Proofs, Propagation Redundancy, and Extended Resolution. - Sam Buss; Neil Thapen (SAT, 2019)

DRMaxSAT with MaxHS: First Contact. - António Morgado 001; Alexey Ignatiev; Maria Luisa Bonet; João Marques-Silva 001; Sam Buss (SAT, 2019)

Strategies for Stable Merge Sorting. - Sam Buss; Alexander Knop (SODA, 2019)

On transformations of constant depth propositional proofs. - Arnold Beckmann; Sam Buss (Ann. Pure Appl. Log., 2019)

Feasible set functions have small circuits. - Arnold Beckmann; Sam Buss; Sy-David Friedman; Moritz Müller; Neil Thapen (Comput., 2019)

Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs. - Sam Buss; Anupam Das 002; Alexander Knop (CSL, 2020)

Lower Bounds on OBDD Proofs with Several Orders. - Sam Buss; Dmitry Itsykson; Alexander Knop; Artur Riazanov; Dmitry Sokolov 001 (Electron. Colloquium Comput. Complex., 2020)

2-D Tucker is PPA complete. - James Aisenberg; Maria Luisa Bonet; Sam Buss (J. Comput. Syst. Sci., 2020)

Propositional proof systems based on maximum satisfiability. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (Artif. Intell., 2021)

DRAT and Propagation Redundancy Proofs Without New Variables. - Sam Buss; Neil Thapen (Log. Methods Comput. Sci., 2021)

Proof Complexity and SAT Solving. - Sam Buss; Jakob Nordström (Handbook of Satisfiability, 2021)

TFNP Characterizations of Proof Systems and Monotone Circuits. - Sam Buss; Noah Fleming; Russell Impagliazzo (Electron. Colloquium Comput. Complex., 2022)

Polynomially Verifiable Arithmetic. - Sam Buss (Logic, Automata, and Computational Complexity, 2023)

On the Consistency of Circuit Lower Bounds for Non-deterministic Time. - Albert Atserias; Sam Buss; Moritz Müller (STOC, 2023)

Extended Resolution Clause Learning via Dual Implication Points. - Sam Buss; Jonathan Chung 003; Vijay Ganesh 001; Albert Oliveras (CoRR, 2024)

Redundancy for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Sam Buss; Massimo Lauria (Electron. Colloquium Comput. Complex., 2024)

Regular resolution effectively simulates resolution. - Sam Buss; Emre Yolcu (Inf. Process. Lett., 2024)

Redundancy Rules for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Sam Buss; Massimo Lauria (SAT, 2025)

A simple supercritical tradeoff between size and height in resolution. - Sam Buss; Neil Thapen (Inf. Process. Lett., 2026)