2026-07-25T06:59:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5736 2024-03-06T10:36:57Z ddc:004 open_access

Semantic Versus Syntactic Cutting Planes Filmus, Yuval Hrubeš, Pavel Lauria, Massimo proof complexity cutting planes lower bounds In this paper, we compare the strength of the semantic and syntactic version of the cutting planes proof system. First, we show that the lower bound technique of Pudlák applies also to semantic cutting planes: the proof system has feasible interpolation via monotone real circuits, which gives an exponential lower bound on lengths of semantic cutting planes refutations. Second, we show that semantic refutations are stronger than syntactic ones. In particular, we give a formula for which any refutation in syntactic cutting planes requires exponential length, while there is a polynomial length refutation in semantic cutting planes. In other words, syntactic cutting planes does not p-simulate semantic cutting planes. We also give two incompatible integer inequalities which require exponential length refutation in syntactic cutting planes. Finally, we pose the following problem, which arises in connection with semantic inference of arity larger than two: can every multivariate non-decreasing real function be expressed as a composition of non-decreasing real functions in two variables? Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yuval Filmus and Pavel Hrubeš and Massimo Lauria 2016 Is Part Of LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2016.35 urn:nbn:de:0030-drops-57367 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.35 eng https://creativecommons.org/licenses/by/3.0/legalcode