Programs and Proofs

What does it mean to test a computing system? What does it mean for a computing system to always behave correctly?

Can a mathematical proof guarantee a real computing system will behave correctly?

Minima

The minimum of a set with respect to some comparator operator is the element which is “less than” (according to that comparator) every other element: $m \in S$ is the minimum of $S$ if and only if $\forall x \in S - { m } . m \prec x$.

$$ \forall S \in \textrm{pow}(\mathbb{N}) - { \varnothing } \ldotp \exists m \in S\ldotp \forall x \in S - {m}\ldotp m < x $$

Formulas, Propositions, and Inference Rules

$P \implies Q$ is a formula.
$\forall P \in { T, F } . \forall Q \in { T, F } . P \implies Q$ is a proposition.
$\infer{Q}{P}$ is an inference rule.

A formula is satisfiable if there is some way to make it true.

$P \implies Q$ is satisfiable:

$\exists P \in { T, F } . \exists Q \in {T, F } . P \implies Q$

We can show a formula is satisfiable by giving one choice for the variable assignments that makes it true. For example, $P = T$, $Q = T$.

A formula is valid if there is no way to make it false.

$P \implies Q$ is not valid:

$\forall P \in { T, F } . \forall Q \in {T, F } . P \implies Q$

This proposition is false, we can chose $P = T$, $Q = F$.

An inference rule is sound if it never leads to a false conclusion. An inference rule $\infer{Q}{P}$ is sound if and only if the formula $P \implies Q$ is valid. So, this way, we can find out whether an inference rule is sound or not, by checking out whether the corresponding formula is valid or not.

Negating Quantifiers

What is the negation of $\forall x \in S . P(x)$?

What is the negation of $\exists x \in S . P(x)$?

Satisfiability

Definition. A formula is in SAT if it is in CNF form and it is satisfiable.

Definition. A formula is in 3SAT if it is in 3CNF form and it is satisfiable.

$$ (x_1 \vee x_2 \vee x_3) \wedge (x_1 \vee \overline{x_2} \vee x_3) \wedge (\overline{x_1} \vee x_2 \vee \overline{x_3}) $$

\begin{center} \tiny \begin{math} (x{48} \vee x{4} \vee \overline{x{9}}) \wedge (\overline{x{44}} \vee x{50} \vee \overline{x{37}}) \wedge (\overline{x{8}} \vee \overline{x{1}} \vee x{28}) \wedge (x{21} \vee x{27} \vee \overline{x{32}}) \wedge (x{17} \vee x{29} \vee \overline{x{30}}) \wedge (x{30} \vee x{24} \vee x{37}) \wedge (\overline{x{22}} \vee \overline{x{27}} \vee \overline{x{44}}) \wedge (x{8} \vee \overline{x{25}} \vee \overline{x{24}}) \wedge (\overline{x{44}} \vee x{50} \vee x{14}) \wedge (x{45} \vee x{15} \vee x{37}) \wedge (\overline{x{16}} \vee x{14} \vee \overline{x{36}}) \wedge (\overline{x{33}} \vee x{5} \vee x{26}) \wedge (x{18} \vee \overline{x{7}} \vee \overline{x{24}}) \wedge (x{31} \vee x{38} \vee x{28}) \wedge (x{31} \vee \overline{x{33}} \vee \overline{x{8}}) \wedge (x{49} \vee x{7} \vee \overline{x{6}}) \wedge (x{34} \vee \overline{x{8}} \vee x{46}) \wedge (x{4} \vee \overline{x{5}} \vee \overline{x{35}}) \wedge (x{43} \vee x{27} \vee x{39}) \wedge (\overline{x{46}} \vee \overline{x{40}} \vee \overline{x{27}}) \wedge (\overline{x{25}} \vee x{14} \vee \overline{x{49}}) \wedge (x{38} \vee x{5} \vee x{15}) \wedge (x{9} \vee x{14} \vee \overline{x{19}}) \wedge (x{45} \vee \overline{x{42}} \vee \overline{x{39}}) \wedge (x{34} \vee \overline{x{22}} \vee \overline{x{28}}) \wedge (\overline{x{20}} \vee x{15} \vee \overline{x{8}}) \wedge (\overline{x{44}} \vee \overline{x{10}} \vee \overline{x{9}}) \wedge (x{22} \vee \overline{x{31}} \vee x{14}) \wedge (\overline{x{9}} \vee \overline{x{42}} \vee \overline{x{15}}) \wedge (\overline{x{40}} \vee x{12} \vee \overline{x{32}}) \wedge (\overline{x{20}} \vee \overline{x{6}} \vee \overline{x{15}}) \wedge (\overline{x{37}} \vee x{39} \vee \overline{x{23}}) \wedge (\overline{x{3}} \vee \overline{x{40}} \vee \overline{x{32}}) \wedge (\overline{x{4}} \vee \overline{x{25}} \vee x{7}) \wedge (\overline{x{20}} \vee \overline{x{36}} \vee \overline{x{37}}) \wedge (\overline{x{40}} \vee \overline{x{35}} \vee x{39}) \wedge (\overline{x{43}} \vee \overline{x{40}} \vee \overline{x{7}}) \wedge (x{34} \vee x{44} \vee x{26}) \wedge (x{13} \vee x{27} \vee x{28}) \wedge (x{12} \vee \overline{x{36}} \vee x{7}) \wedge (\overline{x{16}} \vee x{9} \vee \overline{x{24}}) \wedge (\overline{x{48}} \vee x{14} \vee x{28}) \wedge (x{16} \vee x{4} \vee x{40}) \wedge (\overline{x{25}} \vee x{15} \vee x{37}) \wedge (x{47} \vee \overline{x{26}} \vee \overline{x{23}}) \wedge (x{4} \vee \overline{x{13}} \vee x{36}) \wedge (x{48} \vee \overline{x{13}} \vee \overline{x{37}}) \wedge (x{4} \vee x{35} \vee \overline{x{27}}) \wedge (\overline{x{22}} \vee x{47} \vee x{26}) \wedge (\overline{x{22}} \vee \overline{x{46}} \vee x{27}) \wedge (\overline{x{20}} \vee x{49} \vee x{11}) \wedge (x{42} \vee \overline{x{10}} \vee x{28}) \wedge (\overline{x{45}} \vee x{28} \vee \overline{x{37}}) \wedge (x{14} \vee \overline{x{32}} \vee \overline{x{23}}) \wedge (x{22} \vee x{14} \vee x{23}) \wedge (\overline{x{17}} \vee \overline{x{46}} \vee \overline{x{7}}) \wedge (\overline{x{31}} \vee x{46} \vee \overline{x{50}}) \wedge (x{34} \vee \overline{x{41}} \vee x{43}) \wedge (x{17} \vee \overline{x{9}} \vee x{15}) \wedge (x{46} \vee x{14} \vee \overline{x{12}}) \wedge (\overline{x{20}} \vee x{12} \vee x{14}) \wedge (x{41} \vee x{42} \vee \overline{x{15}}) \wedge (x{48} \vee x{46} \vee \overline{x{36}}) \wedge (\overline{x{22}} \vee \overline{x{4}} \vee \overline{x{49}}) \wedge (x{22} \vee x{12} \vee \overline{x{42}}) \wedge (x{13} \vee \overline{x{38}} \vee x{39}) \wedge (x{48} \vee \overline{x{16}} \vee \overline{x{27}}) \wedge (x{17} \vee \overline{x{18}} \vee \overline{x{26}}) \wedge (x{48} \vee \overline{x{40}} \vee \overline{x{35}}) \wedge (\overline{x{43}} \vee \overline{x{40}} \vee \overline{x{49}}) \wedge (x{29} \vee x{11} \vee \overline{x{32}}) \wedge (x{33} \vee \overline{x{17}} \vee x{39}) \wedge (\overline{x{25}} \vee \overline{x{9}} \vee \overline{x{6}}) \wedge (x{40} \vee \overline{x{50}} \vee x{19}) \wedge (x{8} \vee x{10} \vee \overline{x{27}}) \wedge (x{5} \vee x{9} \vee \overline{x{26}}) \wedge (x{45} \vee \overline{x{38}} \vee \overline{x{27}}) \wedge (\overline{x{4}} \vee \overline{x{40}} \vee \overline{x{42}}) \wedge (x{21} \vee x{50} \vee x{12}) \wedge (\overline{x{8}} \vee \overline{x{14}} \vee \overline{x{42}}) \wedge (\overline{x{17}} \vee x{47} \vee \overline{x{27}}) \wedge (x{49} \vee \overline{x{12}} \vee \overline{x{6}}) \wedge (x{27} \vee x{49} \vee \overline{x{32}}) \wedge (\overline{x{29}} \vee \overline{x{12}} \vee \overline{x{26}}) \wedge (x{48} \vee \overline{x{2}} \vee x{6}) \wedge (x{16} \vee x{36} \vee x{49}) \wedge (x{33} \vee \overline{x{12}} \vee \overline{x{26}}) \wedge (\overline{x{33}} \vee x{29} \vee x{49}) \wedge (\overline{x{48}} \vee x{2} \vee x{19}) \wedge (x{25} \vee x{36} \vee x{49}) \wedge (x{21} \vee x{40} \vee \overline{x{14}}) \wedge (\overline{x{34}} \vee \overline{x{44}} \vee \overline{x{6}}) \wedge (x{48} \vee \overline{x{50}} \vee \overline{x{1}}) \wedge (x{5} \vee \overline{x{12}} \vee x{7}) \wedge (x{21} \vee \overline{x{35}} \vee \overline{x{27}}) \wedge (\overline{x{22}} \vee \overline{x{16}} \vee \overline{x{14}}) \wedge (\overline{x{13}} \vee \overline{x{35}} \vee \overline{x{12}}) \wedge (\overline{x{4}} \vee \overline{x{35}} \vee \overline{x{42}}) \wedge (\overline{x{50}} \vee \overline{x{40}} \vee x{7}) \wedge (x{25} \vee x{47} \vee \overline{x{12}}) \end{math} \end{center}

Converting Truth Tables to DNF

\begin{tabular}{cc|cc} $P$ & $Q$ & $P \implies Q$ & $P \oplus Q$ \ \hline \T & \T & \T & \F
\T & \F & \F & \T
\F & \T & \T & \T
\F & \F & \T & \F
\end{tabular}

The output of the operator is \T\ if and only if the inputs do match one row where the output is \T. So, to get a DNF we can go over all the rows where hte output is \T, and for each write a clause that means we are in that row. Then we OR all such (conjunctive) clauses. For example, for $P \oplus Q$ we get

$$(P \wedge \neg Q) \vee (\neg P \wedge Q)$$

Converting Truth Tables to CNF

\begin{tabular}{cc|cc} $P$ & $Q$ & $P \implies Q$ & $P \oplus Q$ \ \hline \T & \T & \T & \F
\T & \F & \F & \T
\F & \T & \T & \T
\F & \F & \T & \F
\end{tabular}

The output of the operator is \T\ if and only if the inputs do not match any row where the output is \F. So, to get a CNF we can go over all the rows where hte output is \F, and for each write a clause that means we are not in that row. Then we AND all such clauses. For example, for $P \oplus Q$ we get

$$(\neg P \vee \neg Q) \wedge (P \vee Q)$$

The related 3CNF formulation

When we are only interested to know whether or not a given formula is satisfiable, we can write a 3CNF that is satisfiable iff the original formula is. In order to do that, we first write an equivalent CNF, and then convert it to a 3CNF (which is not necessarily equivalent, but only guarantees to preserve the satisfiability feature) as follow. For each clause with less than 3 literals such as $(A \lor \neg B)$ we add a dummy variable $C$ (only for this clause) and interprete the $(A \lor \neg B)$ as a formula over all of $A,B,C$ and write a CNF for them (which happens to be 3CNF!). For longer clauses such as $(A \lor B \lor C \lor D)$ we do another trick of breaking them into smaller parts using new dummy variables as follows $(A \lor B \lor \neg X) \wedge (\neg X \lor C \lor D).$