Transcript prop-proofs - Department of Computer Science

Propositional Calculus – Methods
of Proof
Predicate Calculus
Math Foundations of Computer
Science
Propositional Calculus – Methods
of Proof
Logic is useful in design theory
Also useful in reasoning about mathematical
statements:
Case Analysis
Proof of the contrapositive
Proof by contradiction
Proof by reduction to truth
Math Foundations of Computer
Science
2
Law of Excluded Middle

Handy for Case Analysis:
Can now prove
Dual of the Excluded Middle
A proposition and its negative can’t be
simultaneously true
Does this jive with the real world?
Do we have contradictions in mathematics?
Handy for proofs by Contradiction
Contrapositive
Example: Prove “If x is greater than 2 and
prime, then x is odd”
The contrapositive is:
“If x is even, then x <= 2 or x is composite”
Propositional logic fails at this point; we
need to talk about the meaning of our
terms
Contradiction
Rather than proving E, we assume NOT E,
and look for a contradiction
Example (from previous slide)
a
x>2
b
x is prime
c
x is odd
We want to prove ab → c
(cont.)
6
Contradiction - example
So, as assume a b and NOT c
Derive a contradiction
Equivalence by Truth
(p ≡ 1) ≡ p
Use the tautologies to reduce the
expression to 1
Probably most like the examples we’ve
been looking at
Deduction
The use of logic in sequences of statements
that constitute a complete proof
Start with certain hypotheses (“givens”)
Apply a sequence of inference rules
Results in a conclusion
Most familiar to you, from geometry
9
Deduction
Given expressions E1, E2, …, Ek as
hypotheses, we wish to draw conclusion E,
another logical expression
Generally, none of these is a tautology
Show that
E1 ∩ E2 ∩ … ∩ Ek → E
is a tautology
Deduction – guidelines
Any tautology may be a line in a proof
modus ponens – if E and E→F are lines,
then F may be added as a line
If E and F are lines in a proof, then we may
add the line E ∩ F
If E and E≡F are lines, the F can be added
Resolution – a handy inference
rule
Based on this tautology:
Just another inference rule
But a common one
Often used in a deductive proof
Resolution
Applied to clauses (your hypotheses) (as in
deduction)
Convert hypotheses into clauses (conjunctive
normal form)
Write each clause as a line
Use resolution to write other lines
Simplifying clauses
Consider a clause as a set of literals
Given commutativity, associativity and
idempotence of OR
Remove duplicate literals:
Simplifying clauses
Eliminate clauses that have contradictory
literals

, by the annihilator law of OR
These clauses are equivalent to 1, and are
not needed in a proof
Resolution - example
Given these 2 clauses:
Rearrange terms, and apply resolution
Remove duplicates
Put Expressions into Conjunctive
Normal Form
1. Get rid of all operators but NOT, AND, and
OR


NAND and NOR are easily replaced with
AND and OR followed by a NOT
2. Apply DeMorgan’s laws to push negations
down as far as they will go
Put Expressions into Conjunctive
Normal Form
3. Apply distributive law for OR over AND
 Push the ORs as low as they’ll go
 E.g.
 Replace the implication
 Push that outer NOT down:
CNF – Example (cont.)
Push the first OR below the first AND
Regroup
Push that OR down over the inner AND
And now you have an expression in CNF
Resolution Proofs by
Contradiction
A more common use
Start with both the hypotheses, and the
negation of the conclusion
Try to drive a clause w/no literals
This clause has value 0