Neil Thapen

Institute of Mathematics, AS CR
Žitná 25, 115 67 Praha 1
Czech Republic

I am a researcher at the Institute of Mathematics of the Academy of Sciences of the Czech Republic. My research is mostly in logic, in particular proof complexity and weak arithmetic.

Until 2023 I organized the institute's logic seminar (old page).

Published papers/preprints

These may differ from the final published versions.
  1. The strength of the dominance rule (pdf)
    Leszek Kołodziejczyk and Neil Thapen. Submitted, 2024.

  2. TFNP Intersections through the Lens of Feasible Disjunction (pdf)
    Pavel Hubáček, Erfan Khaniki and Neil Thapen. Proceedings of ITCS 2024, LIPIcs Vol 287, pp. 63:1 - 63:24, 2024.

  3. A Simple Supercritical Tradeoff between Size and Height in Resolution (pdf)
    Samuel Buss and Neil Thapen. Submitted, 2023.

  4. Approximate counting and NP search problems (pdf)
    Leszek Kołodziejczyk and Neil Thapen. Journal of Mathematical Logic, Vol 22:3, 2022.

  5. A separation of PLS from PPP (on ECCC)
    Ilario Bonacina and Neil Thapen. ECCC report TR22-089, 2022.

  6. First-order reasoning and efficient semialgebraic proofs (pdf)
    Fedor Part, Neil Thapen and Iddo Tzameret. Proceedings of LICS 2021.

  7. DRAT and propagation redundancy proofs without new variables (pdf)
    Samuel Buss and Neil Thapen. Logical Methods in Computer Science, Vol 17:2, article 12, 2021.
    A version appeared in SAT 2019, pp. 71-89.

  8. Random resolution refutations (pdf)
    Pavel Pudlák, Neil Thapen. Computational Complexity, Vol 28:2, pp. 185-239, 2019
    A version appeared in CCC 2017, LIPIcs Vol 79, pp. 1:1-1:10, 2015.

  9. Feasible set functions have small circuits (pdf)
    Arnold Beckmann, Sam Buss, Sy-David Friedman, Moritz Müller, Neil Thapen. Computability, Vol 8:1, pp. 67-98, 2019.

  10. Polynomial calculus space and resolution width (revised pdf)
    Nicola Galesi, Leszek Kołodziejczyk and Neil Thapen. Proceedings of FOCS 2019, pp. 1325–1337, 2019.

  11. On semantic cutting planes proofs with very small coefficients (pdf)
    Massimo Lauria and Neil Thapen. Information Processing Letters, Vol 136, pp. 70-75, 2018.

  12. Cobham Recursive Set Functions and Weak Set Theories (pdf)
    Arnold Beckmann, Sam Buss, Sy-David Friedman, Moritz Müller, Neil Thapen.
    In Sets and Computations, Lecture Notes Series 33, Institute for Mathematical Sciences, National University of Singapore, pp. 55-116, 2017.

  13. The complexity of proving that a graph is Ramsey (pdf)
    Massimo Lauria, Pavel Pudlák, Vojtěch Rödl and Neil Thapen. Combinatorica, Vol 37 (2), pp. 253-268, 2017.
    An earlier version appeared at ICALP 2013, LNCS Vol 7965, pp. 648-695, 2013.

  14. A tradeoff between length and width in resolution (pdf)
    Neil Thapen. Theory of Computing, Vol 12:5, pp. 1-14, 2016.

  15. Total space in resolution (pdf)
    Ilario Bonacina, Nicola Galesi, Neil Thapen. SIAM Journal on Computing, Vol 45:5, pp. 1894-1909, 2016.
    An earlier version appeared in FOCS 2014, pp. 641-650.

  16. Cobham Recursive Set Functions (pdf)
    Arnold Beckmann, Sam Buss, Sy-David Friedman, Moritz Müller, Neil Thapen. Annals of Pure and Applied Logic, Vol 167:3, pp. 335-369, 2016.

  17. Space Complexity in Polynomial Calculus (pdf)
    Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen and Noga Ron-Zewi. SIAM Journal on computing, Vol 44:4, pp. 1119-1153, 2015.
    An earlier version appeared in IEEE Conference on Computational Complexity 2012, pp. 334-344.

  18. The space complexity of cutting planes refutations (pdf)
    Nicola Galesi, Pavel Pudlák, Neil Thapen. Proceedings of CCC 2015, LIPIcs Vol 33, pp. 433-447, 2015.

  19. The Ordering Principle in a Fragment of Approximate Counting (pdf)
    Albert Atserias and Neil Thapen. ACM Transactions on Computational Logic, Vol 15:4, article 29, 2014.

  20. Fragments of approximate counting (pdf)
    Samuel Buss, Leszek Kołodziejczyk and Neil Thapen. Journal of Symbolic Logic, Vol 79:2, pp. 496-525, 2014.
    [An open problem from this paper is solved in "The Ordering Principle in a Fragment of Approximate Counting" above.]

  21. Parity games and propositional proofs (pdf)
    Arnold Beckmann, Pavel Pudlák and Neil Thapen. ACM Transactions on Computational Logic, Vol 15:2, article 17, 2014.

  22. How much randomness is needed for statistics? (pdf)
    Bjørn Kjos-Hanssen, Antoine Taveneaux and Neil Thapen. Annals of Pure and Applied Logic, Vol 165:9, pp. 1470-1483, 2014.
    An earlier version appeared in Computability in Europe 2012, LNCS Vol 7318, pp. 395-404, 2012.

  23. Alternating minima and maxima, Nash equilibria and Bounded Arithmetic (pdf)
    Pavel Pudlák and Neil Thapen. Annals of Pure and Applied Logic, Vol 163:5, pp. 604-614, 2012.

  24. Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem (pdf)
    Neil Thapen. Archive for Mathematical Logic, Vol 50:7-8, pp. 665-680, 2011.

  25. The provably total NP search problems of weak second order bounded arithmetic (pdf)
    Leszek Kołodziejczyk, Phuong Nguyen and Neil Thapen. Annals of Pure and Applied Logic, Vol 162:6, pp. 419-446, 2011.

  26. The provably total search problems of bounded arithmetic (pdf)
    Alan Skelley and Neil Thapen. Proceedings of the London Mathematical Society, Vol 103:1, pp. 106-138, 2011.

  27. The polynomial and linear hierarchies in V_0 (pdf)
    Leszek Kołodziejczyk and Neil Thapen. Mathematical Logic Quarterly, Vol 55:5, pp. 509-514, 2009.
    An earlier version appeared in Computability in Europe 2007.

  28. The polynomial and linear hierarchies in models where the weak pigeonhole principle fails (pdf)
    Leszek Kołodziejczyk and Neil Thapen. Journal of Symbolic Logic, Vol 73:2, pp. 578-592, 2008.

  29. NP search problems in low fragments of bounded arithmetic (pdf)
    Jan Krajíček, Alan Skelley and Neil Thapen. Journal of Symbolic Logic, Vol 72:2, pp. 649-672, 2007.

  30. The strength of replacement in weak arithmetic (pdf)
    Stephen Cook and Neil Thapen. ACM Transactions on Computational Logic, Vol 7:4, pp. 749-764, 2006.
    An earlier version appeared in LICS 2004.

  31. A note on Delta_1 induction and Sigma_1 collection (pdf)
    Neil Thapen. Fundamenta Mathematicae, Vol 186, pp. 79-84, 2005.

  32. Resolution and pebbling games (pdf)
    Nicola Galesi and Neil Thapen. SAT 2005, LNCS 3569, pp. 76-90, 2005.

  33. Weak theories of linear algebra (pdf)
    Neil Thapen and Michael Soltys. Archive for Mathematical Logic, Vol 44:2, pp. 195-208, 2005.

  34. Structures interpretable in models of bounded arithmetic (pdf)
    Neil Thapen. Annals of Pure and Applied Logic, Vol 136:3, pp. 247-266, 2005.

  35. A model-theoretic characterization of the weak pigeonhole principle (pdf)
    Neil Thapen. Annals of Pure and Applied Logic, Vol 118:1-2, pp. 175-195, 2002.

Some slides from talks

  1. Resolution height and a candidate formula hard for CDCL without restarts (pdf)
    SAT and Interactions, Schloss Dagstuhl, 18 October 2024.

  2. The strength of the dominance rule (pdf)
    SAT 2024, Tata Consultancy Services, Pune, 21 August 2024.

  3. First-order logic and algebraic proof systems (pdf)
    ASL annual North American meeting, UC Irvine, 26 March 2023.

  4. A logical approach to TFNP (pdf)
    Reflections on Propositional Proofs in Algorithms and Complexity, Workshop at FOCS 21, online, 7 February 2022.

  5. DRAT proofs, propagation redundancy and extended resolution (pdf)
    SAT 2019, Calouste Gulbenkian Foundation, Lisbon, 9 July 2019.

  6. Approximate counting and NP search (pdf)
    ITI fest, Villa Lanna, Prague, 4 December 2018.

  7. Random resolution (pdf)
    Proof Complexity and Beyond, MF Oberwolfach, 18 August 2017.

  8. Small circuits for feasible set functions (pdf)
    Prague–Vienna Set Theory Workshop, Czech Academy of Sciences, 17 October 2016.

  9. A feasible set theory (pdf)
    Journées sur les Arithmétiques Faibles 35, University of Lisbon, 6 June 2016.

  10. Parity games and propositional proofs (pdf)
    Proof Complexity 2014, Vienna Technical University, 13 August 2014.

Other things

9/10/21 Neil Thapen