Methods of proof

premise p and conclusion c

Direct proof

Prove \(p \to c = \neg p \vee c = T\).

If we stick with direct proof, the expression to prove must have an outermost OR operator.

If p and c are complex clauses, why don’t we convert \(\neg p \vee c\) to the disjunctive normal form?

Disjunctive Normal Form

A disjunctive normal form is an expression \(x_1 \vee x_2 \vee \cdots \vee x_n\). If there is \(x_i\) and \( x_j\) in the expression such that \(x_i=\neg x_j\), we can conclude the whole expression is True.

An empty disjunctive normal form evaluates to False.^[1]

Simplify[(p && q) || (p && ! q) || (! p && r) || (! p && ! r)]

Proof by contradiction

\begin{align*}
p \to c = T \\
\neg (p \to c) = \neg T \\
\neg (\neg p \vee c) = F \\
p \wedge \neg c = F \\
\end{align*}

Hence, proving \(p \wedge \neg c = F\) is equivalent to Direct proof.

If p and c are complex clauses, why don’t we convert \(p \wedge \neg c \) to the conjunctive normal form?

Conjunctive Normal Form

A conjunctive normal form is an expression \(x_1 \wedge x_2 \wedge \cdots \wedge x_n\). If there is \(x_i\) and \( x_j\) in the expression such that \(x_i=\neg x_j\), we can conclude the whole expression is False.

An empty conjunctive normal form evaluates to True.^[1]

References

1. S. Gursky; . Minimization of Matched Formulas. WDS'11 Proceedings of Contributed Papers. 2011, (): [2025-08-02].↑↑