A note on bounded arithmetic
A note on proofs of falsehood.
An upper bound on the space complexity of random formulae in resolution
We prove that, with high probability, the space complexity of refuting a random unsatisfiable Boolean formula in -CNF on variables and clauses is .
An Upper Bound on the Space Complexity of Random Formulae in Resolution
We prove that, with high probability, the space complexity of refuting a random unsatisfiable Boolean formula in k-CNF on n variables and m = Δn clauses is .
Consistency proof without transfinite induction for a formal system for turing machines.
Diagonalization in proof complexity
We study diagonalization in the context of implicit proofs of [10]. We prove that at least one of the following three conjectures is true: ∙ There is a function f: 0,1* → 0,1 computable in that has circuit complexity . ∙ ≠ co . ∙ There is no p-optimal propositional proof system. We note that a variant of the statement (either ≠ co or ∩ co contains a function hard on average) seems to have a bearing on the existence of good proof complexity generators. In particular, we prove that if a minor variant...
Eine beweistheoretische Anwendung partieller stetiger Funktionale.
Functorial bounds for cut elimination in L... .I.
Functorial bounds for cut elimination in L.. .II.
Intuitionistic Frege systems are polynomially equivalent.
Monotone sequent calculus and resolution
We study relations between propositional Monotone Sequent Calculus (MLK --- also known as Geometric Logic) and Resolution with respect to the complexity of proofs, namely to the concept of the polynomial simulation of proofs. We consider Resolution on sets of monochromatic clauses. We prove that there exists a polynomial simulation of proofs in MLK by intuitionistic proofs. We show a polynomial simulation between proofs from axioms in MLK and corresponding proofs of contradiction (refutations) in...
Natural limitations of decisions procedures for arithmetic with bounded quantifiers.
On cut elimination in the presence of peirce rule.
On effective speed-up and long proofs of trivial theorems in formal theories
On sequent calculi for intuitionistic propositional logic
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
On the weak pigeonhole principle
We investigate the proof complexity, in (extensions of) resolution and in bounded arithmetic, of the weak pigeonhole principle and of the Ramsey theorem. In particular, we link the proof complexities of these two principles. Further we give lower bounds to the width of resolution proofs and to the size of (extensions of) tree-like resolution proofs of the Ramsey theorem. We establish a connection between provability of WPHP in fragments of bounded arithmetic and cryptographic assumptions (the existence...
Representation of metamorphosis grammar in logic grammar: Proof trees and their lengths.
Speed-up for propositional Frege systems via generalizations of proofs
Statistical testing procedure for lengths of formalized proofs
Statistical theory of logical derivability