A Generalized Resolution Proof Schema and the Pigeonhole Principle
David M. Cerna
备注：
Work is progress. This is the current extension of the the schematic resolution refutation formalism. A better formalism is being investigated. arXiv admin note: substantial text overlap with arXiv:1503.08551, arXiv:1601.06548
The schematic CERES method is a method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can be thought of as a way to circumvent the addition of an induction rule to the LK-calculus. In this work, we formalize a schematic version of the Infinitary Pigeonhole Principle (IPP), in the LKS-calculus, and analyse the extracted clause set schema. However, the refutation we find cannot be expressed as a resolution proof schema because there is no clear ordering of the terms indexing the recursion, every ordering is used in the refutation. Interesting enough, the clause set and its refutation is very close to a canonical form found in cut elimination of LK-proofs. Not being able to handle refutations of this form is problematic in that proof schema, when instantiated, are LK-proofs. Based on the structure of our refutation and structural results, we develop a generalized resolution proof schema based on recursion over a special type of list, and provide a refutation, using our generalization, of the clause set extracted from our formal proof of IPP. We also extract a Herbrand System from the refutation.
Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice
University of Oregon（俄勒冈大学）；University of Massachusetts, Lowell（马萨诸塞大学洛厄尔分校）；Université Paris Cité, Inria, CNRS, IRIF（巴黎西岱大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRIF）
证明图式是LK-证明的一种变体，能够通过向标准的一阶LK-演算添加所谓的证明链接来模拟一阶逻辑中的各种归纳方案。证明链接允许证明引用证明，从而为证明模式提供递归结构。不幸的是，在存在证明链接的情况下，应用约简割消是不平凡的。借用函数式编程中的惰性实例化的概念，我们在本地评估证明链接，允许还原切割消除进行过去。虽然，这种方法不能被用来获得切割自由证明模式，我们仍然获得了重要的结果，示意CERES方法，即切割消除证明模式的基础上的决议。在“Towards a clausal analysis of cut-elimination”一文中，我们指出，约简割消变换了一个给定的LK-证明，使得变换前后的特征子句集（即表示一个LK-证明的割结构的子句集）之间存在一个包含关系。设CL（A '）是一个LK-证明A的范式A'的特征子句集，该范式A '是通过对A进行约化割消元而不进行原子割消元得到的。则CL（A '）被从对A的任何约化割消应用中提取的所有特征小句集合所包含。这种范式被称为ACNF top，在通过分解消除割的方法中起着重要作用。这些结果可以通过我们的证明链接的“惰性实例化”推广到证明模式，并且为证明模式的完全切消元法提供了必要的一步。
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
我们研究了多项式演算（PC）和多项式演算分辨率（PCR）在证明度上获得下界的问题，因此[Impagliazzo et al. '99]也研究了证明大小。[Alekhnovich and Razborov '03]建立了如果CNF公式F的子句变量关联图是足够好的扩展器，则证明F是不可满足的需要高PC/PCR度。我们进一步发展了[AR 03]中的技术，以表明如果可以在某种意义上以“尊重公式的结构”的方式“聚类”子句和变量，则该聚类版本的关联图是扩展器就足够了。作为一个推论，我们证明了功能鸽子洞原理（FPHP）公式时，需要高PC/PCR度限制为常数度扩展图。这回答了[Razborov '02]中的一个公开问题，并且还意味着FPHP公式的标准CNF编码在多项式演算分辨率中需要指数证明大小。因此，虽然Onto-FPHP公式对于多项式微积分来说很容易，如[Riis '93]所示，但FPHP和Onto-PHP公式即使在限制于有界度展开式时也很难。
