In the first half of my talk I will mention the history of our logic group in our institute and how we gradually moved from studying metamathematics of Peano Arithmetic to weak fragments, and eventually to proof complexity of propositional logic. In the second part I will talk about my project to define a hierarchy of propositional proof systems indexed by ordinals up to epsilon_0 with the aim to prove that they characterize the proof system associated with Peano Arithmetic.
Logic seminar
usually takes place each Monday at 16:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
From Peano Arithmetic to propositional calculus and back
Pavel Pudlák
IM CAS
Monday, 2. May 2022 - 16:00 to 17:30
in IM, rear building, ground floor - *not broadcast*
Simulations in QBF Proof Complexity
Leroy Chew
TU Wien
Monday, 25. April 2022 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
Quantified Boolean Formulas (QBF) extend propositional formulas with Boolean quantifiers. Solving a QBF is PSPACE complete, and QBFSAT is seen as a natural extension of the SAT problem. Just as propositional proof complexity underlies the theory behind SAT solving, QBF proof complexity underlies the theory behind QBF solving. Here we will focus on the relative strengths of QBF proof systems via p-simulation.
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
Proof complexity of CSP on algebras with linear congruence, Part 2
Azza Gaysin
Charles University
Monday, 11. April 2022 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.
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.
Proof complexity of CSP on algebras with linear congruence
Azza Gaysin
Charles University
Monday, 4. April 2022 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.
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.
A Walk with Goodstein
David Fernández-Duque
Ghent University and Czech Academy of Sciences
Monday, 21. March 2022 - 16:00 to 17:30
Main lecture room in the rear building at Zitna; online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join on zoom
The classical Goodstein process is based on writing numbers in "normal form" in terms of addition and exponentiation with some base k. By iteratively changing base and subtracting one, one obtains very long sequences of natural numbers which eventually terminate. The latter is proven by comparing base-k normal forms with Cantor normal forms for ordinals, and in fact this proof relies heavily on the notion of normal form. The question then naturally arises: what if we write natural numbers in an arbitrary fashion, not necessarily using normal forms? What if we allow not only addition and exponentiation, but also multiplication for writing numbers?
A "Goodstein walk" is any sequence obtained by following the standard Goodstein process but arbitrarily choosing how each element of the sequence is represented. As it turns out, any Goodstein walk is finite, and indeed the longest possible Goodstein walk is given by the standard normal forms. In this talk we sketch a proof of this fact... more
Nisan-Wigderson generators in Proof Complexity: New lower bounds
Erfan Khaniki
Institute of Mathematics
Monday, 14. March 2022 - 16:00 to 17:30
Main lecture room in the rear building at Zitna; online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join on zoom
A map g:{0,1}^n --> {0,1}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b in {0,1}^m\Rng(g) the formula \tau_b(g), naturally expressing b \not \in Rng(g), requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if A is a suitable matrix and f is a NP \cap CoNP function hard-on-average for P/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege.
In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.
In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.