A note on semantic cutting planes.
Pavel Hrubeš · Electronic colloquium on computational complexity · 2013
We show that the semantic cutting planes proof system has feasible interpolation via monotone real circuits. This gives an exponential lower bound on proof length in the system, answering a question from [5]. We also pose the following problem: can every multivariate non-decreasing function be expressed as a composition of non-decreasing functions in two variables?