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.

Towards P != NP from Extended Frege lower bounds

Ján Pich
University of Oxford
Monday, 12. December 2022 - 16:00 to 17:30
We prove that if conditions I-II (below) hold and there is a sequence of Boolean functions $f_n$ hard to approximate by p-size circuits such that p-size circuit lower bounds for $f_n$ do not have p-size proofs in Extended Frege system EF, then $P \ne NP$.

I. $S^1_2$ proves that there is a function $g\in E$ hard to approximate by subexponential-size circuits.

II. (Learning from the non-existence of OWFs.) $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits learning p-size circuits over the uniform distribution, with membership queries.

Here, $S^1_2$ is Buss's theory of bounded arithmetic formalizing p-time reasoning.

Further, we show that any of the following assumptions implies that $P \ne NP$, if EF is not p-bounded:

1. (Feasible anticheckers.) $S^1_2$ proves that a p-time function generates anticheckers for SAT.

2. (Witnessing $NP\not\subseteq P/poly$.) $S^1_2$ proves that a p-time... more

On the parameterized complexity of Delta-0 truth

Moritz Müller
University of Passau
Monday, 21. November 2022 - 16:00 to 17:30
We consider the problem, given a Δ0 formula φ(x) and a natural number n in unary, whether φ(n) is true. We are interested in instances of the problem where n is much bigger than φ. More precisely, we consider the parameterized problem with parameter |φ|. We show unconditionally that this problem does not belong to the parameterized version of AC0. We also show that certain natural upper bounds on the parameterized complexity of the problem imply separations of classical complexity classes. These results are obtained by an analysis of a parameterized halting problem. A related problem concerns the provability of the MRDP theorem in bounded arithmetic.

Integrating Machine Learning into Saturation-based ATPs

Martin Suda
CVUT
Monday, 14. November 2022 - 16:00 to 17:30
Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.

Elementary analytic functions in VTC^0, Part 2

Emil Jeřábek
IM CAS
Monday, 24. October 2022 - 16:00 to 17:30
It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.

Pages