Implicit Resolution

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.