## Wang, Zi Chao - Implicit Resolution

lmcs:1125 - Logical Methods in Computer Science, October 16, 2013, Volume 9, Issue 4
Implicit Resolution

Authors: Wang, Zi Chao

Let \Omega be a set of unsatisfiable clauses, an implicit resolution refutation of \Omega is a circuit \beta with a resolution proof {\alpha} of the statement "\beta describes a correct tree-like resolution refutation of \Omega". We show that such system is p-equivalent to Extended Frege. More generally, let {\tau} be a tautology, a [P, Q]-proof of {\tau} is a pair (\alpha,\beta) s.t. \alpha is a P-proof of the statement "\beta is a circuit describing a correct Q-proof of \tau". We prove that [EF,P] \leq p [R,P] for arbitrary Cook-Reckhow proof system P.

Source : oai:arXiv.org:1308.5608
DOI : 10.2168/LMCS-9(4:7)2013
Volume: Volume 9, Issue 4
Published on: October 16, 2013
Submitted on: March 8, 2013
Keywords: Computer Science - Logic in Computer Science