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

This page has been seen 75 times.

This article's PDF has been downloaded 26 times.