• Feasibly constructive proofs of succinct weak circuit lower bounds 

      Muller, Moritz Martin; Pich, Ján (2020-02)
      Article
      Accés obert
      We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial ...
    • Lower bounds for DNF-refutations of a relativized weak pigeonhole principle 

      Atserias, Albert; Müller, Moritz; Oliva Valls, Sergi (2015-06-01)
      Article
      Accés obert
      The relativized weak pigeonhole principle states that if at least 2n out of n(2) pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle ...
    • On the consistency of circuit lower bounds for non-deterministic time 

      Atserias, Albert; Buss, Sam; Müller, Moritz (Association for Computing Machinery (ACM), 2023)
      Text en actes de congrés
      Accés obert
      We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory ‍V20 is consistent with the conjecture ...
    • Partially definable forcing and bounded arithmetic 

      Atserias, Albert; Müller, Moritz (2015-02-01)
      Article
      Accés obert
      We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity.
    • The ordering principle in a fragment of approximate counting 

      Atserias, Albert; Thapen, Neil (2014)
      Article
      Accés obert
      The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized ...