Publications and Other Research
Sam Buss


Publication and research web page.  When possible, papers are available to download.
Warning:  These online versions may differ from the actual published versions (sometimes better, sometimes worse, than the published version).

My online CV also has a list of my publications — but usually there are more papers available below than are listed in my c.v.

For papers that are too recent to appear here, please email me, sbuss@math.ucsd.edu.

Copyright notice:  All material downloadable from this page is copyrighted by Sam Buss, his coauthors, and/or the publishers.

Publications.

Books (authored)

  1. Samuel R. Buss, 3D Computer Graphics: A Mathematical Introduction with OpenGL, Cambridge University Press, 2003.
  2. Samuel R. Buss, Bounded Arithmetic, Bibliopolis, Naples 1986.  221+v pages. Revision of 1985 Ph.D. thesis.

Books (edited)

  1. Samuel R. Buss, Petr Hájek and Pavel Pudlák (eds), Logic Colloquium '98, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Prague, Czech Republic, August 9-15, 1998, Lecture Notes in Logic 13, Association for Symbolic Logic, AK Peters, Natick, MA, 2000.   xvi+541 pages.
  2. Samuel R. Buss (ed.), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics #137, Elsevier, Amsterdam, 1998, x+811 pages.
  3. Paul Beame and Samuel R. Buss (eds.), Proof Complexity and Feasible Arithmetics, DIMACS Series in Discrete Mathematics and Theoretical Computer Science #39, American Mathematical Society, Providence, RI, 1998, xii+320 pages.
  4. Samuel R. Buss and Phillip J. Scott (eds.), Feasible Mathematics: A Mathematical Sciences Institute Workshop, Ithaca, New York June 1989, Progress in Computer Science #9, Birkhauser, Boston, 1990, viii+350 pages.

Patents

  1. Peter N. Yianilos and Samuel R. Buss, Associative Memory Circuit System and Method, continuation in part, U.S. Patent #4490811, December 1984.  European patent #83903352.9, January 1986.
  2. Samuel R. Buss and Peter N. Yianilos, Linear and Non-linear Time Methods for Minimum Cost Matching on Quasiconvex Tours, U.S. Patent #5841958, November 1998.

Software

  1. OpenGL Computer graphics software accompanying the book "3D Computer Graphics: A Mathematical Introduction with OpenGL".
  2. Raytrace software, accompanying the same book.
  3. Inverse Kinematics demos,  (with Jin-Su Kim).   Associated article and unpublished survey are also available.
  4. Spherical Averages and Spherical Splines.   Software for the Buss-Fillmore spherical averages algorithms.
  5. bussproofs.sty.   The "Buss proofs" LaTeX/TeX style file for creating proof trees.
  6. qcmatch.  Quasiconvex minimum-cost matching algorithm in ANSI C.  (joint with D. Robinson, K. Kanzelberg, P. Yianilos).   Associated article and technical report also available.

Papers - journal articles and conference proceedings.

  1. (with Mia Minnes). Algorithmic Randomness with Probabilistic Strategies and Intermediate Success. Preprint version. March 2013.
  2. (with Michael Soltys). Unshuffling a Square is NP-Hard. Preprint version. November 2012.
  3. (with Leszek Kołodziejczyk). Small Stone in Pool. Preprint version. October 2012.
  4. (with Maria Luisa Bonet and Jan Johannsen). Improved Separations of Regular Resolution from Clause Learning Proof Systems. Submitted for publication. August 2012.
  5. (with Arnold Beckmann and Sy Friedman). Safe Recursive Set Functions. Submitted for publication, 2012.
  6. (with Leszek Kołodziejczyk and Konrad Zdanowski). Collapsing Modular Counting in Bounded Arithmetic and Constant Depth Propositional Proofs. Preprint, 2012.
  7. (with Mia Minnes). Probabilistic Algorithmic Randomness. To appear in the Journal of Symbolic Logic, 201?.
  8. (with Arnold Beckmann). Improved Witnessing and Local Improvement Principles for Second-Order Bounded Arithmetic. To appear in Transactions on Computational Logic. 201?.
  9. (with Leszek Kołodziejczyk and Neil Thapen). Fragments of Approximate Counting. Submitted for publication, 2012.
  10. Cut Elimination In Situ. Submitted for publication, 2012.
  11. (with Maria Luisa Bonet). An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. In Theory and Applications of Satisfiability Testing (SAT 2012), Springer-Verlag Lecture Notes in Computer Science 7317, pp. 44-57, 2012. A subsequent full version by M. Bonet, S. Buss and J. Johannsen is available and contains additional results.
  12. (with Ryan Williams). Limits on Alternation-Trading Proofs for Time-Space Lower Bounds. in Proc. IEEE 27th Annual Conference on Computational Complexity (CCC), pp. 181-191, 2012. Expanded journal version submitted for publication, 2011.
  13. (with Alan Johnson). Propositional proofs and reductions between NP search problems. Annals of Pure and Applied Logic 163, 9 (2012) 1163-1182.
  14. (with Yijia Chen, Jörg Flum, Sy Friedman, and Moritz Müller). Strong isomorphism reductions in complexity theory. Journal of Symbolic Logic 76, 4 (2011) 1381-1402.
  15. Sharpened Lower Bounds for Cut Elimination. Journal of Symbolic Logic 77, 2 (2012) 656-668.
  16. (with Arnold Beckmann). Corrected Upper Bounds for Free-Cut Elimination. Theoretical Computer Science 412, 39 (2011) 5433-5445.
  17. (with Alan Johnson). The Quantifier Complexity of Polynomial-Size Iterated Definitions in First-Order Logic. Mathematical Logic Quarterly, 56, 6 (2010) 573-590.
  18. Towards NP-P via Proof Complexity and Search. Annals of Pure and Applied Logic 163, 7 (2012) 906-917. Also in: Foundation Adventures: Essays in Honor of Harvey Friedman, Templeton Foundation Press, Article 13, 2012. To appear.
  19. (with Arnold Beckmann). Characterizing Definable Search Problems in Bounded Arithmetic via Proof Notations. In Ways of Proof Theory, ONTOS Series in Mathematical Logic, pp. 65-134, 2010.
  20. (with Daniel Tracy and Bryan Woods). Efficient Large-Scale Sweep and Prune Methods with AABB Insertion and Removal. In: IEEE Virtual Reality (VR2009), pp. 191-198, 2009.
  21. (with Arnold Beckmann). Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic. Journal of Mathematical Logic 9, 1 (2009) 103-138.
  22. Pool Resolution is NP-hard to Recognize. Archive for Mathematical Logic 48, 8 (2009) 793-798.
  23. (with Roman Kuznets). Lower Complexity Bounds in Justification Logic. Annals of Pure and Applied Logic 163, 7 (2012) 888-905.
    Earlier conference proceedings version: The NP-Completeness of Reflected Fragments of Justification Logics. In Logical Foundations of Computer Science, LFCS'09, Springer-Verlag Lecture Notes in Computer Science #5407, 2009, pp. 122-136.
  24. (with Jan Hoffmann and Jan Johannsen). Resolution Trees with Lemmas - Resolution Refinements that Characterize DLL-Algorithms with Clause Learning. Logical Methods in Computer Science, 4, 4:13, 2008.
  25. (with Jan Hoffmann). The NP-hardness of Finding a Directed Acyclic Graph for Regular Resolution. Theoretical Computer Science 396 (2008) 271-276.
  26. The Computational Power of Bounded Arithmetic from the Predicative Viewpoint. In New Computational Paradigms, Changing Conceptions of What is Computable, edited by S.B. Cooper, B. Löwe, A. Sorbi, Springer, New York, 2008, pp. 213-222.
  27. Nelson's Work on Logic and Foundations and Other Reflections on Foundations of Mathematics. In  Diffusion, Quantum Theory, and Radically Elementary Mathematics, edited by W. Faris, Princeton University Press, 2006, pp. 183-208. Slides from a related talk also available.
  28. Bounded Arithmetic and Constant Depth Frege Proofs.   In Complexity of Computations and Proofs, edited by J. Krajíček, Quaderni di Matematica, vol. 13, 2004, pp. 153-174.   Slides from a related conference presentation also available.
  29. (with Arnold Beckmann). Separation Results for the Size of Constant-depth Propositional Proofs. Annals of Pure and Applied Logic 136, no 1-2 (2005) 30-55.
  30. Collision Detection with Relative Screw Motion. The Visual Computer 21 (2005) 41-58.
  31. (with Jin-Su Kim). Selectively Damped Least Squares for Inverse Kinematics. Journal of Graphics Tools, 10, no.3 (2005) 37-49.
  32. (with Peter Clote). Solving the Fisher-Wright and coalescence problems with a discrete Markov chain analysis. Advances in Applied Probability 36, 4 (2004) 117-197.
  33. Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies. Theoretical Computer Science 357, no. 1-3, (2006) 35-52.
  34. (with Nate Segerlind and Russell Impagliazzo). A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM Journal on Computing 33, 5 (2004) 1171-1200. An earlier version appeared in the Proceedings of the 43rd Annual Symposium on Foundations of Computer Science (FOCS'02), IEEE Computer Society, 2002, pp. 604-613.
  35. Accurate and Efficient Simulations of Rigid Body Rotations. Journal of Computational Physics 164 (2000) 377-406.
  36. (with Alekos Kechris, Anand Pillay and Richard Shore). Prospects for Mathematical Logic in the Twenty-first Century, Journal of Symbolic Logic 7 (2001) 169-196.
  37. (with Bruce Kapron). Resource-bounded Continuity and Sequentiality for Type-two Functionals, ACM Transactions on Computational Logic 3 (2002) 402-417. Extended abstract appeared in Proceedings, 15th IEEE Symposium on Logic in Computer Science (LICS), 2000, pp. 77-83.
  38. (with Arnold Beckmann and Chris Pollett). Ordinal Notations and Well-orderings in Bounded Arithmetic, Annals of Pure and Applied Logic 120 (2002) 197-223. Publisher's erratum: Annals of Pure and Applied Logic 123 (2003) 291.
  39. (with Pavel Pudlák). On the Computational Content of Intuitionistic Propositional Proofs, Annals of Pure and Applied Logic 109 (2001) 49-64.
  40. (with Grigori Rosu). Incompleteness of Behavioral Logics, Proceedings, Coalgebraic Methods in Computer Science, CMCS'2000, Electronic Notes in Theoretical Computer Science 33 (2000) 61-69.
  41. (with Peter Yianilos). Linear and O(n log n) Time Minimum-cost Matching Algorithms for Quasiconvex Tours, SIAM Journal on Computing 27 (1998) 170-201. Expanded version of a paper which appeared in Proceedings of the Fifth ACM-SIAM Symposium on Discrete Algorithms (SODA), 1994, pp. 65-76. See also associated software and technical report.
  42. (with Dima Grigoriev, Russell Impagliazzo and Toniann Pitassi). Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. Journal of Computer and System Sciences 62 (2001) 267-289. Earlier version in Proceedings, 31st Annual ACM Symposium on Theory of Computing (STOC'99), pp. 547-556. One page abstract in 14th IEEE Conference on Computational Complexity (CCC'99) p. 5-5.
  43. (with Jay Fillmore). Spherical Averages and Applications to Spherical Splines and Interpolation. ACM Transactions on Graphics 20 (2001) 95-126. Source code for a C++ implementation available too.
  44. (with Grigori Mints). The Complexity of the Disjunction and Existence Properties in Intuitionistic Logic. Pure and Applied Logic 99 (1999) 93-104.
  45. Propositional Proof Complexity: An Introduction. In Computational Logic, edited by U. Berger and H. Schwichtenberg, Springer-Verlag, Berlin, 1999, pp. 127-178.
  46. An Introduction to Proof Theory. In Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 1-78.
  47. First-order Proof Theory of Arithmetic. In Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 79-147.
  48. (with Misha Alekhnovich, Shlomo Moran and Toniann Pitassi). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. Journal of Symbolic Logic 66 (2001) 171-191. An extended abstract appeared earlier in Mathematical Foundations of Computer Science (MFCS'98), Lecture Notes in Computer Science #1450, Springer-Verlag, 1998, pp. 176-184.
  49. Bounded Arithmetic, Proof Complexity and Two Papers of Parikh. Annals of Pure and Applied Logic 96 (1999) 43-55.
  50. Alogtime Algorithms for Tree Isomorphism, Comparison and Canonization. In Computational Logic and Proof Theory, Proceedings 5th Gödel Colloquium '97. Lecture Notes in Computer Science #1289, Springer-Verlag, Berlin, 1997, pp. 18-33.
  51. (with Toniann Pitassi). Resolution and the Weak Pigeonhole Principle. In Proceedings, Computer Science Logic (CSL'97), Lecture Notes in Computer Science #1414, Springer-Verlag, 1998, pp.149-156.
  52. Bounded Arithmetic and Propositional Proof Complexity. In Logic of Computation,, edited by H. Schwichtenberg, Springer-Verlag, Berlin, 1997, pp. 67-122.
  53. Lower Bounds on Nullstellensatz Proofs via Designs. In Proof Complexity and Feasible Arithmetics, edited by S. Buss and P. Beame, American Mathematical Society, Providence, RI, 1998, pp. 59-71.
  54. Bounded Arithmetic, Cryptography and Complexity. Theoria 63 (1997)147-167.
  55. (with Peter Clote). Cutting Planes, Connectivity and Threshold Logic. Archive for Mathematical Logic 35 (1996) 33-62.
  56. (with R. Impagliazzo, J. Krajíček, P. Pudlák, A. Razborov and J. Sgall). Proof Complexity in Algebraic Systems and Constant Depth Frege Systems with Modular Counting. Computational Complexity 6 (1995/1996) 256-298.
  57. (with Toniann Pitassi). Good Degree Bounds on Nullstellensatz Refutations of the Induction Principle. Journal of Computer and System Sciences 57 (1998) 162-171. Earlier version appeared in Complexity '96, Proceedings of the Eleventh Annual IEEE Conference on Computational Complexity, 1996, pp 233-242.
  58. (with Aleksandar Ignjatović). Unprovability of Consistency Statements in Fragments of Bounded Arithmetic. Annals of Pure and Applied Logic 74 (1995) 221-244.
  59. On Herbrand's Theorem. In Logic and Computational Complexity, Lecture Notes in Computer Science #960, 1995, Springer-Verlag, pp. 195-209.
  60. (with Pavel Pudlák). How To Lie Without Being (Easily) Convicted and Lengths of Proofs in Propositional Calculus. In Eighth Workshop on Computer Science Logic (CSL'94), Lecture Notes in Computer Science #933, Springer-Verlag, 1995, pp. 151-162.
  61. (with Maria Luisa Bonet and Toniann Pitassi). Are There Hard Examples for Frege Systems? In Feasible Mathematics II, Birkhauser, 1995, pp. 31-56.
  62. Relating the Bounded Arithmetic and Polynomial-Time Hierarchies. Annals of Pure and Applied Logic, 75 (1995) 67-77.
  63. (with Maria Luisa Bonet). Size-Depth Tradeoff for Boolean Formulae.. Information Processing Letters, 11 (1994) 151-155.
  64. Some Remarks on the Lengths of Propositional Proofs. Archive for Mathematical Logic 34 (1995) 377-394.
  65. On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedups for Arithmetic. Journal of Symbolic Logic 39 (1994) 737-756.
  66. On Gödel's Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability. In Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.
  67. (with Maria Luisa Bonet). On the Serial Transitive Closure Problem. SIAM Journal on Computing 24 (1995) 109-122. See also next two items.
  68. (with Maria Luisa Bonet). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (1993) 688-709. See also previous item and next item.
  69. (with Maria Luisa Bonet). On the Deduction Rule and the Number of Proof Lines In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science. (LICS'91). IEEE Computer Society Press, 1991, pp. 286-297. Subsumed by the previous two journal articles.
  70. The Witness Function Method and Provably Recursive Functions Of Peano Arithmetic. In Proceedings of Ninth International Congress on Logic, Methodology and Philosophy of Science, D. Prawitz, B. Skyrms and D. Westerstahl (eds), Elsevier Science North-Holland, 1994, pp. 29-68.
  71. Algorithms for Boolean Formula Evaluation and For Tree-Contraction. In Proof Theory, Complexity, and Arithmetic, P. Clote and J. Krajíček (eds), Oxford University Press, 1993, pp. 95-115.
  72. (with Jan Krajíček) An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic. Proceedings of the London Mathematical Society 69 (1994) 1-21.
  73. (with Jan Krajíček and Gaisi Takeuti). Provably Total Functions in the Bounded Arithmetic Theories Ri3, Ui2, and Vi2. In Proof Theory, Arithmetic, and Complexity, P. Clote and J. Krajíček (eds), Oxford University Press, 1993, pp. 116-161.
  74. The Graph of Multiplication is Equivalent to Counting. Information Processing Letters 41 (1992) 199-201.
  75. (with Christos Papadimitriou and John Tsitsiklis).  On the predictability of coupled automata: an allegory about chaos.  Complex Systems 5 (1991) 525-539.  Earlier draft appeared in Proceedings of the 31st Annual Symposium on Foundations of Computer Science, volume II (FOCS' 1990), IEEE Computer Society Press, 1990, pp. 788-793.
  76. Intuitionistic validity in T-normal Kripke structures.  Annals of Pure and Applied Logic 59 (1993) 159-173.
  77. On model theory for intuitionstic bounded arithmetic with applications to independence.  In Feasible Mathematics: A Mathematical Sciences Institute Workshop held in Ithaca, New York, June 1989.  S. Buss and P. Scott (eds).   Birkhauser,  1990, pp. 27-47.
  78. A note on bootstrapping intuitionistic bounded arithmetic.   In Proof Theory: a selection of papers from the Leeds Theory Programme 1990.   P. Aczel, H. Simmons, S. Wainer (eds).  Cambridge University Press, 1992, pp. 142-169.
  79. Propositional consistency proofs.  Annals of Pure and Applied Logic 52 (1991) 3-29.
  80. The undecidability of k-provability.  Annals of Pure and Applied Logic 53 (1991) 75-102
  81. (with Louise Hay).   On truth-table reducibility to SAT.  Information and Computation 91 (1991) 86-102.
  82. (with Louise Hay.) On truth-table reducibility to SAT and the difference hierarchy over NP."  In Proceedings of the the IEEE Structure in Complexity Conference, IEEE Computer Society Press, 1988, pp. 224-233.
  83. The modal logic of pure provability. Notre Dame Journal of Formal Logic 31 (1990) 225-231.
  84. (with Stephen A. Cook and Arvind Gupta and Vijaya Ramachandran).  An optimal parallel algorithm for formula evaluation. SIAM Journal on Computing 21 (1992 755-780.
  85. (with Gyorgy Turan).  Resolution proofs of generalized pigeonhole principles.  Theoretical Computer Science 62 (1988) 311-317.
  86. Axiomatizations and conservation results for fragments of bounded arithmetic.   In Logic and Computation, Proceedings of a Workshop held at Carnegie Mellon University, June 30-July 2, 1987. AMS Contemporary Mathematics 106 (1990) 57-84.
  87. The Boolean formula value problem is in ALOGTIME.  In Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC'87), 1987, pp. 123-131.
  88. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic 52 (1987) 916-927.
  89. The polynomial hierarchy and intuitionistic Bounded Arithmetic.   In  Structure in Complexity, Lecture Notes in Computer Science #223, Springer Verlag, 1986, pp. 77-103.
  90. A conservation result concerning bounded theories and the collection axiom.  Proceedings of the American Mathematic Society 100 (1987) 709-716.
  91. The polynomial hierarchy and fragments of bounded arithmetic.  In Proceedings of the 17-th Annual ACM Symposium on Theory of Computing (STOC'85), 1985, pp. 285-290.
  92. (with P.N. Yianilos and R.A. Harbort),  The application of a pattern matching algorithm to searching medical record text.  In IEEE Symposium on Computer Applications in Medical Care, 1978, pp. 308-313.

Ph.D./Honors theses.

  1. Samuel R. Buss, Bounded Arithmetic, Ph.D. thesis, Department of Mathematics, Princeton University, 1985. 188+v pages.
  2. Samuel R. Buss, The Word Problem for Groups, Undergraduate Honors Thesis, Department of Mathematics, Emory University, 1979,  79 pages.

Reviews, unpublished articles and surveys, course lecture notes, and miscellaneous items.

  1. A review of Forcing With Random Variables and Proof Complexity by Jan Krajíček. Bulletin of Symbolic Logic, 18,4 (2012) 576-578.
  2. Introduction to Inverse Kinematics with Jacobian Transpose, Pseudoinverse and Damped Least Squares methods.  Unpublished survey article, 2004.
  3. (with R. Iemhoff).  The Depth of Intuitionistic Cut Free Proofs.  Unpublished manuscript 2003.
  4. Student-written notes of my Math 267 - Propositional Proof Complexity course in Winter 2002.
  5. (with P. Yianilos).  A Bipartite Matching Approach to Approximate String Comparison and Seach. Unpublished manuscript.
  6. (with P. Yianilos). Secure Short-Key Cryptosystems: Forty Bits is Enough.   Unpublished manuscript.
  7. Lectures on Proof Theory, Technical Report number SOCS-96.1, School of Computer Science, McGill University, 1996, 117 pages.
  8. A review of the biography of K. Godel, Logical Dilemmas, by John Dawson. SIAM Review 40 (1998) 397-400.
  9. Student-written notes of my Math 267 - Mathematical Foundations of Cryptography course in Winter 1997.
  10. (with Peter Clote).  Threshold logic proof systems.  Unpublished manuscript.  May 1995.
  11. (with D. Robinson, K. Kanzelberg, P. Yianilos).  Solving the Minimum-Cost Matching Principle for Quasi-Convex Tours: An Efficient ANSI C Implementation. Technical report #370, Dept. of Computer Science Engineering, UCSD, April 1994, 69 pages.  Associated software and journal article also available.
  12. A review of Exponential lower bounds for the pigeonhole principle by P. Beame, R. Impagliazzo, J Krajíček, T. Pitassi, P. Pudlák and A. Woods, in Computing Reviews 34 (May 1993) 261-261.   Reprinted in SIGACT News 24 (1993) 41-41.
  13. Student-written notes of my Math 267 - Circuit Complexity course in Winter-Spring 1992.
  14. A review of three papers of Neil Immerman, Journal of Symbolic Logic 54 (1989) 287-288.
  15. (with S.A. Cook, P.W. Dymond and L. Hay), The log space oracle hierarchy collapses.   Technical report #CS87-103,  Computer Science Engineering Department, Univ. of California, San Diego, 1987.
  16. Student-written notes for Math 260A-C on Introduction to Mathematical Logic, Fall 1988-Spring 1989.
  17. Student-written notes of my Math 271 (Berkeley) topics course on Weak Formal Systems and Connections to Computational Complexity, Winter-Spring 1988.
  18. Neighborhood metrics on n-dimension blocks of characters.  Technical report #00218-86, Mathematical Sciences Research Institute, Berkeley, California, September 1985. 

Selected recent talks with computer generated slides.

  1. Collapsing Modular Counting in Bounded Arithmetic and Constant Depth Propositional Proofs. Limits of Theorem Proving (LiThPr). Rome, Italy, September 2012.
  2. An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. Theory and Applications of Satisfiability Testing (SAT 2012). Trento, Italy, June 2012.
  3. Total NP Functions I: Complexity and Reducibility and Total NP Functions II: Provability and Reducibility. Two tutorial talks on NP Search. Workshop on Logical Approaches to Complexity II, Newton Institute, Cambridge, England, March 2012.
  4. Expressibility, and the Complexity of Proofs, PhilMath Intersem, Paris 7 Diderot, June 2011.
  5. Proof Complexity and the Complexity of SAT Solvers, First International SAT/SMT Solver Workshop, Boston, June 2011.
  6. Limits on Alternation-Trading Proofs for Time-Space Bounds for Satisfiability, Barcelona, February 2011; Wales, March 2011; Paris, June 2011.
  7. SAT Solver Trials: Experiments with a SAT Solver, Infinity Project, Centre de Recerca Matemàtica, Barcelona, Spain, December 2009.
  8. A series of four talks on NP Functions, Local Search, and Bounded Arithmetic, Prague Fall School on Logic and Complexity, four plenary talks, September 2009.
  9. Towards NP-P and Satisfiability via Proof Complexity and Proof Search, Logical Foundations of Computer Science (LFCS'09), plenary talk, January 2009.
  10. The NP-Completeness of Reflected Fragments of Justification Logics, Logical Foundations of Computer Science (LFCS'09), January 2009.
  11. Polynomial Local Search higher in the Polynomial Hierachy and Bounded Arithmetic, BIRS Workshop on Computability, Reverse Mathematics and Combinatorics, Banff, Canada, December 2008. Also at Research Workshop on Proof Theory and Constructivity, Leeds, July 2009.
  12. Large Numbers, Busy Beavers, Noncomputability and Incompleteness, Food for Thought seminar, UCSD, November 2007.
  13. The Computational Power of Bounded Arithmetic from the Predicative Viewpoint ASL Winter Meeting, special session. January 2007.
  14. Propositional Proof Systems and Search, Connections II: Fundamentals of Network Science, Caltech, August 2006.
  15. Proof Complexity and Computational Hardness, Computability in Europe (CiE), July 2006, Swansea, Wales.  Three tutorial lectures.
  16. Bounded Arithmetic, Constant-Depth Proofs and st-Connectivity.  UCLA Logic Meeting (VIG), February 2004.  Contains st-Connectivity and Hex tautology work.
  17. Ed Nelson's Work on Logic and Foundations: Radical Constructivism.  Presentation at Workshop on Analysis, Probability and Logic, Pacific Institute of Mathematical Studies, UBC, Vancouver, June 2004.  A related paper is also available.
  18. Is it easier to "Discover" than to "Verify"?
    19.  UCSD Math Circle presentation to high school students, May 22, 2004.
  19. Bounded arithmetic and bounded depth propositional proofs. Takeuti Symposium on Mathematical Logic, Kobe, Japan, December, 2003.
  20. Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies.
    21.  Workshop on Proof Theory, Muenster, October 2003; and 12th Latin American Symposium on Mathematical Logic (SLALM), Costa Rica, January 2004.
  21. Spherical Splines and Applications to Spherical Splines and Interpolation.  Pixel Cafe, UCSD, December 2002.
  22. Taylor series methods for rigid body simulation and extensions to Lie groups.  Seventh SIAM Conference on Geometric Design and Computing. Sacramento, November 2001.
  23. Bounded arithmetic and propositional proofs.  NATO International Summer School on Logic of Computation.  Marktoberdorf, Germany.   July-August 1995.  Five hours of lectures.

Selected Ph.D. dissertations by students. (More can be available upon request.)

  1. David Robinson, Parallel Algorithms for Group Word Problems, Ph.D. Thesis, Department of Mathematics, University of Califoria, San Diego, 1993.

Acknowledgements. The bulk of the above work on this page was performed with partial financial support under various NSF grants.   Some parts of the above work were funded in part by grants from NATO and from the Czech Academy of Sciences.

Computer games. Computer games with algorithms or code by Buss. See also my Moby Games rap sheet at http://www.mobygames.com/developer/sheet/view/developerId,42330/ (This lists only games with explicit credit given, not all the games that use Buss's algorithms and code.)

  1. Grand Theft Auto: Episodes from Liberty City., Rockstar Games, 2010.
  2. Grand Theft Auto IV: The Lost and Damned., Rockstar Games, 2010.
  3. Grand Theft Auto: The Ballad of Gay Tony., Rockstar Games, 2010.
  4. Grand Theft Auto IV, Rockstar Games, 2008.
  5. Smuggler's Run: Warzones, Rockstar Games, 2002.
  6. TransWorld SURF, Infogrames, 2002.
  7. Smuggler's Run 2: Hostile Territory, Rockstar Games, 2001.
  8. Midnight Club: Street Racing, Rockstar Games, 2000.
  9. Midtown Madness 2, Microsoft Game Studios, 2000.
  10. Smuggler's Run, Rockstar Games, 2000.
  11. Midtown Madness, Microsoft Game Studios, 1999.