Zi Chao Wang - Implicit Resolution

lmcs:1125 - Logical Methods in Computer Science, October 16, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:7)2013
Implicit ResolutionArticle

Authors: Zi Chao Wang

    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.


    Volume: Volume 9, Issue 4
    Published on: October 16, 2013
    Imported on: March 8, 2013
    Keywords: Computer Science - Logic in Computer Science

    27 Documents citing this article

    Consultation statistics

    This page has been seen 940 times.
    This article's PDF has been downloaded 237 times.