Implicit Resolution
Logic in Computer Science
2015-07-01 v2
Abstract
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.
Cite
@article{arxiv.1308.5608,
title = {Implicit Resolution},
author = {Zi Chao Wang},
journal= {arXiv preprint arXiv:1308.5608},
year = {2015}
}