Implicit Resolution
Zi Chao Wang (Charles University in Prague)

TL;DR
This paper introduces the concept of implicit resolution, showing its equivalence to Extended Frege, and explores proof systems involving circuits and tautologies, establishing complexity relationships among them.
Contribution
It formalizes implicit resolution and proves its p-equivalence to Extended Frege, extending the understanding of proof system relationships involving circuits and tautologies.
Findings
Implicit resolution is p-equivalent to Extended Frege.
The paper establishes p-reductions between various proof systems.
It generalizes proof system comparisons involving circuits and tautologies.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
