Semantic Versus Syntactic Cutting Planes
Semantic Versus Syntactic Cutting Planes
复制标题
语义剖切面与句法剖切面
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Massimo Lauria
中科院分区：
文献类型：
--
作者：
Yuval Filmus;P. Hrubes;Massimo Lauria
在本文中，我们比较的强度的语义和句法版本的切割平面证明系统。
首先，我们表明，Pudlak的下界技术也适用于语义切割平面：证明系统具有可行的插值通过单调真实的电路，这给出了一个指数下界的长度语义切割平面反驳。
其次，我们发现语义反驳比句法反驳更强。特别地，我们给出了一个公式，任何反驳在句法切割平面需要指数长度，而有一个多项式长度反驳在语义切割平面。换句话说，句法切割平面不p-模拟语义切割平面。我们还给出了两个在句法切割平面上需要指数长度反驳的不相容整数不等式。
最后，我们提出了以下问题，这与语义推理的arity大于2：可以每一个多元非减真实的功能表示为一个组合的非减真实的功能在两个变量？
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 Pudlak 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?