Semantic entailment
= Semantic entailment
{title2=$\varphi\models\psi$}
A <propositional formula> $\varphi$ semantically entails $\psi$ when every <Boolean valuation> satisfying $\varphi$ satisfies $\psi$. Equivalently, $\varphi\land\neg\psi$ is an <unsatisfiable Boolean formula>. Deciding <semantic entailment> is <co-NP>-complete: a counterexample <Boolean valuation> certifies failure in <polynomial time>, while $\theta\mapsto\langle\theta,p\land\neg p\rangle$ reduces unsatisfiability to <semantic entailment>.