Weak Versions of Extended Resolution
summary
Shows that a family of explicitly defined weakenings of extended resolution (BC-, SBC-, RAT-, SPR- etc.) are pairwise incomparable by giving a uniform, syntactic guarded extension variables construction that uses redundancy notions (blocked/set-blocked/subsumption/RAT) plus effective simulation tricks to turn an ER proof into a short proof for one system but not the other. Gives short lower bounds for several cases, cheap separations like BC-minus vs RAT-minus, and isolates SPR- as the stubborn frontier where lower bounds remain hard.
AI-written summary · about
chapters (7)
- 0:00Intro
- 1:26Example: resolution proof
- 2:07Extended resolution (ER)
- 10:34Syntactic criteria for redundancy
- 20:34Guarded extension variables
- 22:48Example: lower bound
- 23:38Separating constructions
related talks
18mType-Based Incorrectness Reasoning
17mPushing the Limit of 1-Minimality of Language-Agnostic Program Reduction
31mA Comparison of Program Logics for (In)Correctness
21mSupermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
18mPreview: Verification (Correctness)
19mNon-Termination Proving at Scale
20mTruly Stateless, Optimal Dynamic Partial Order Reduction