Implicit resolution
From MaRDI portal
Publication:2851676
DOI10.2168/LMCS-9(4:7)2013zbMATH Open1297.03029arXiv1308.5608MaRDI QIDQ2851676
Author name not available (Why is that?)
Publication date: 16 October 2013
Published in: (Search for Journal in Brave)
Abstract: Let Omega be a set of unsatisfiable clauses, an implicit resolution refutation of Omega is a circuit �eta with a resolution proof {alpha} of the statement "�eta describes a correct tree-like resolution refutation of Omega". We show that such system is p-equivalent to Extended Frege. More generally, let { au} be a tautology, a [P, Q]-proof of { au} is a pair (alpha,�eta) s.t. alpha is a P-proof of the statement "�eta is a circuit describing a correct Q-proof of au". We prove that [EF,P] leq p [R,P] for arbitrary Cook-Reckhow proof system P.
Full work available at URL: https://arxiv.org/abs/1308.5608
No records found.
No records found.
This page was built for publication: Implicit resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851676)
