Based on joint work with Jan Pich.
Based on joint work with Jan Pich.
In recent decades, a particularly interesting case study has been provided by RT^2_2: Ramsey's theorem for pairs and two colours. RT^2_2 and its variants are anomalous in the sense of not being equivalent to any of the typical set existence axioms considered in reverse mathematics, or to each other. Characterizing the first-order part of RT^2_2 is a long-standing and highly interesting open problem. Methods used to make progress on this problem have typically been based on some... more
On the surface QBF proof systems seem harder to compare to one another since they vary considerably in how they deal with quantification. In particular there's a vast difference between theory systems that generalise from propositional logic, the proof systems that capture the process of CDCL solving and the proof systems that capture the expansion and CEGAR based solvers. And many results do formally show an incomparability in the proof complexity between different systems as we suspect. However, there are a few non-obvious cases where a simulation is possible. In this talk we... more
We show that Zhuk's algorithm for algebras with linear congruence can be formalized in the theory V^1. Thus, using known methods of proof complexity, Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects X that cannot be homomorphically mapped into A but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.