Logic seminar

Lower bounds on semantic cutting planes

Cutting Planes is a refutation system which certifies unsatisfiability of a set of linear inequalities. Typically, it is defined as using the addition rule and rounding rule. We consider the semantic version of the system, where every sound inference with a constant number of premises is allowed. We observe that the semantic system has feasible interpolation via monotone real circuits - a fact previously established for syntactic cutting planes by P. Pudlak. Nevertheless, we show that the semantic system is strictly stronger than the syntactic. Joint work with Y. Filmus and M. Lauria.