Drawing Sound Conclusions from Unsound Premises

Given sets $Φ_1=\{ϕ_{11},...,ϕ_{1u(1)}\}, ...,Φ_{z}=\{ϕ_{z1},...,ϕ_{zu(z)}\}$ of boolean formulas, a formula $ω$ follows from the conjunction $\bigwedgeΦ_i= \bigwedge ϕ_{ij}$ iff $\neg ω\wedge \bigwedge_{i=1}^z Φ_i$ is unsatisfiable. Now assume that, given integers $0\leq e_i < u(i)$, we must check if $\neg ω\wedge \bigwedge_{i=1}^z Φ'_i$ remains unsatisfiable, where $Φ'_i\subseteq Φ_i$ is obtained by deleting $\,\,e_{i}$ arbitrarily chosen formulas of $Φ_i$, for each $i=1,...,z.$ Intuitively, does $ω$ {\it stably} follow, after removing $e_i$ random formulas from each $Φ_i$? We construct a quadratic reduction of this problem to the consequence problem in infinite-valued \luk\ logic Ł$_\infty$. In this way we obtain a self-contained proof that the Ł$_\infty$-consequence problem is coNP-complete.

No reviews yet.

No comments yet.