Definition. Eliminating Implications and Biconditionals [000j]

unsatisfiability: \(F\) is unsatisfiable if and only if \(F'\) is unsatisfiable.
model correspondence: For every satisfying assignment (model) of \(F'\), there exists a corresponding satisfying assignment of \(F\), and vice versa, when restricted to the original variables of \(F\).

To eliminate implications (\(\to \)) and biconditionals (\(\leftrightarrow \)) from a formula \(F\), we can use the following equivalences:

\[ \begin {align*} p \to q &\equiv \neg p \lor q \\ p \leftrightarrow q &\equiv (p \land q) \lor (\neg p \land \neg q) \end {align*} \]

VU-VFS-2025. Lecture 2 - Normal Forms & DPLL [000b]