Rules of Inference

Modus ponens

$\begin{array}{l}p\\ p\to q\\ \therefore q\end{array}$

Modus tollens

$\begin{array}{l}\neg q\\ p\to q\\ \therefore \neg p\end{array}$

Hypothetical Syllogism

$\begin{array}{l}p\to q\\ q\to r\\ \therefore p\to r\end{array}$

Disjunctive Syllogism

$\begin{array}{l}p\vee q\\ \neg p\\ \therefore q\end{array}$

Addition

$\begin{array}{l}p\\ \therefore p\vee q\end{array}$

Simplification

$\begin{array}{l}p\wedge q\\ \therefore p\end{array}$

Conjunction

$\begin{array}{l}p\\ q\\ \therefore p\wedge q\end{array}$

Resolution

$\begin{array}{l}p\vee q\\ \neg p\vee r\\ \therefore q\vee r\end{array}$

Universal Instantiation

$\begin{array}{c}(\forall x\mid x\in D:P(x))\\ \therefore P(c/x)\end{array}$

Universal Generalization

$\begin{array}{c}P(c/x)\\ \therefore (\forall x\mid x\in D:P(x))\end{array}$

Existential Instantiation

$\begin{array}{c}(\exists x\mid x\in D:P(x))\\ \therefore P(c^{\ast }/x)\end{array}$

Existential Generalization

$\begin{array}{c}P(c^{\ast }/x)\\ \therefore (\exists x\mid x\in D:P(x))\end{array}$