Rules of Inference

Tautology	Name
$(p\wedge (p\to q))\to q$	Modus ponens
$(\neg q\wedge (p\to q)\to \neg p)$	Modus tollens
$((p\to q)\wedge (q\to r))\to (p\to r)$	Hypothetical syllogism
$((p\vee q)\wedge \neg p)\to q$	Disjunctive syllogism
$p\to (p\vee q)$	Addition
$(p\wedge q)\to p$	Simplification
$((p)\wedge (q))\to (p\wedge q)$	Conjunction
$((p\vee q)\wedge (\neg p\vee r))\to (q\vee r)$	Resolution

Resolution

Computer programs have been developed to automate the task of reasoning and proving theorems. Many of these programs make use of a rule of inference known as resolution. (This has something to do with normal forms)

$$((p\vee q)\wedge (\neg p\vee r))\to (q\vee r)$$

The final disjunction is called the resolvent.