slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

On the Conjectures of Razborov and Rudich
Rahul Santhanam
University of Oxford
Monday, 23. May 2022 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
We say that Rudich's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of random truth table tautologies. We say that Razborov's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of any truth table tautologies. A fundamental task in proof complexity and the meta-mathematics of circuit lower bounds is to understand for which Q these conjectures hold. We show various results about these conjectures, including evidence for their difficulty.

Based on joint work with Jan Pich.

In search of the first-order part of Ramsey's theorem for pairs
Leszek Kołodziejczyk
University of Warsaw
Monday, 16. May 2022 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
Reverse mathematics studies the logical strength of mathematical theorems formalized as statements in the language of second-order arithmetic (which is a two-sorted language with one sort of variables for natural numbers and another for sets of natural numbers). The strength is usually measured in terms of implications between the theorems and some set existence axioms, but it also makes sense to ask about the first-order consequences of a theorem, that is, what statements about natural numbers it implies.

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 proving consistency of equational theories in Bounded Arithmetic
Yoriyuki Yamagata
AIST
Monday, 9. May 2022 - 11:00 to 12:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.

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*
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.

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.

Pages

  • …
  • 2
  • …