5 problems

Analyzability requires lower bounds or proofs that are hard to find. For every propositional proof system $Q$, if $Q$ is analyzable, then $Q$ is not p-optimal.

Analyzability requires lower bounds. For every propositional proof system $Q$, if $Q$ is analyzable, then $Q$ is not optimal.

Tseitin SPR− conjecture. The tautology ${\mathrm{TS}}_G$ has polynomial-size ${\mathrm{SPR}}^-$ refutations for every graph $G$.

A p-optimal proof system is a propositional proof system that polynomially simulates every propositional proof system. No p-optimal proof system conjecture. There exists no p-optim…

A propositional proof system is a polynomial-time computable function onto the set of tautologies. It is length-optimal if every proof in any proof system can be replaced by a proo…