正则归结有效模拟归结
Regular resolution effectively simulates resolution
AI总结：
本文证明正则归结在有效模拟下与归结等价，并借此以黑盒方式重新得到正则归结自动化困难性的结果。
摘要：
正则归结是归结证明系统的一种精化，要求证明中任意路径上同一变量不得被归结超过一次。已知存在公式序列，它们在正则归结中需要指数规模的证明，而在归结中却有多项式规模的证明。因此，就通常的模拟概念而言，正则归结与归结是分离的。比较证明系统的另一种较弱概念是“有效模拟”，它允许在证明系统之间转换时同时翻译公式和证明。我们证明，在有效模拟下，正则归结与归结等价。作为推论，我们以黑盒方式重新得到了最近关于正则归结自动化困难性的结果。
英文摘要：
Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an "effective simulation," which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
