We can use propositional logic to reason formally about (or construct proofs of) propositions.

A *deductive argument* takes as given a set of *premises*
(or *hypotheses*) which are known to be true
and attempts to prove a *conclusion* valid
by a sequence of steps, termed *inferences*.

Each inference follows from the premises or a previous inference
by the application of an *inference rule*.

Given premises (or inferences) P1..Pn, we can infer expression E if P1 AND P2 AND .. Pn -> E is a tautology.

- Whenever E is a tautology, P1 AND P2 AND .. Pn -> E is a
tautology.
- Given two premises P1 and P2, we can infer P1 AND P2.
- If P1 and (P1 -> P2) are given or inferred,
then we can infer P2
by the rule of modus ponens (p AND (p->q) -> q).
- If NOT P2 and (P1 -> P2) are given or inferred,
then we can infer NOT P1
by the rule of modens tollens.
- If P1 and (P1==P2) are given or inferred, we can infer P2.

Prove (p -> q) AND (NOT p -> q) == q:

1. (p -> q) AND (NOT p -> q) Given 2. (NOT p OR q) AND (NOT NOT p OR q) Rewriting -> in terms of NOT and OR 3. (NOT p OR q) AND (p OR q) Elimination of double negation 4. ((NOT p OR q) AND p) OR ((NOT p OR q) AND q) Distribute AND over OR 5. ( NOT p AND p OR q AND p) OR (NOT p AND q OR q) Distribute AND over OR 6. (q AND p) OR (NOT p AND q OR q) Eliminate p AND NOT p 7. (q AND p) OR q Subsumption 8. q Subsumption QED

If the weather is warm and the sky is clear, then either we go swimming or we go boating. It is not the case that if the sky is clear then we go swimming. Therefore, if we do not go boating, then the weather is not warm.

We can rewrite this argument formally, using the following variables to correspond to each of the propositions in the argument:

w = weather is warm c = sky is clear s = we go swimming b = we go boating

If the weather is warm and the sky is clear, then either we go swimming or we go boating:

(w AND c) -> (s OR b)

It is not the case that if the sky is clear then we go swimming.

NOT (c -> s)

Therefore, if we do not go boating, then the weather is not warm.

NOT b -> NOT w

To prove the conclusion given the premises, we need to be able to infer the conclusion from the premises.

1. (w AND c) -> (s OR b) Premise 1 2. NOT (c -> s) Premise 2 3. NOT (w AND c) OR (s OR b) L1, rewriting -> 4. (NOT w OR NOT c) OR (s OR b) L3, DeMorgan's law 5. NOT (NOT c OR s) L2, rewriting -> 6. c AND NOT s L5, DeMorgan's law 7. c L6 8. NOT s L6 9. (NOT w OR b) OR (NOT c OR s) L4, assoc/comm OR 10. (NOT w OR b) OR s L7,L9, (F OR p == p) 11. NOT w OR b L8,L10, (p OR F == p) 12. w -> b L11, rewriting -> 13. NOT b -> NOT w QED L12, contrapos. law

The previous examples of proofs show how to start with a set of premises and prove a conclusion (or infer an equivalence).

In proving an equivalence using inferences, we repeatedly simplify a complex logical expression until the result is the simplified expression for which equivalence is desired.

In proving a conclusion from a set of premises, we repeatedly establish inferences from the premises until we are able to infer the conclusion.

In each case, the process is somewhat ad hoc, with no guarantee that the simplifications we choose will lead to the desired conclusion (or equivalence) quickly.

Since the best known algorithm for the tautology problem is exponential, there is no optimal algorithm for finding a proof that doesn't explore all possible simplications (in the worst case).

However, there are techniques that help direct our search for
a proof in the right direction.
*Resolution* is one such technique.