Skip to content (access key 's')
Logo of Technion
Logo of CS Department

The Taub Faculty of Computer Science Events and Talks

Theory Seminar: The power of the Binary Value Principle in Proof Complexity
event speaker icon
Yaroslav Alekseev (St. Petersburg university)
event date icon
Wednesday, 02.11.2022, 12:30
event location icon
Taub 201
The (extended) Binary Value Principle (eBVP: $k + x_0 + 2x_1 + … + 2^n x_n $ for $k>0$ and $x^2_i=x_i$) has received a lot of attention recently: several lower bounds have been proved for it (Alekseev et al 2020, Alekseev 2021, Part and Tzameret 2021), and a polynomial simulation of a strong semialgebraic proof system in IPS+eBVP has been shown (Alekseev et al 2020). In this talk, we consider Polynomial Calculus with the algebraic version of Tseitin’s extension rule. We show that in this context eBVP still allows to simulate similar semialgebraic systems. We also prove that it allows to simulate the Square Root Rule (Grigoriev and Hirsch 2003), which is absolutely unclear in the context of ordinary Polynomial Calculus. On the other hand, we demonstrate that eBVP probably does not help in proving exponential lower bounds for Boolean tautologies: we show that an Extended Polynomial Calculus derivation of any such tautology from eBVP must be of exponential size.