G4G0-2/AI & Data Mining/Week 23/Week 23 - Deductive Proofs.md

Slide 3: Recap on Logical Implication (Entailment) |-|=-

• Entailment notation: p |=q if and only if the implication p$\implies$q is a tautology.
• Example:
  • p \land q |=q
  • Truth table for p \implies q:

p	q	p \land q	p \implies q
T	T	T	T
T	F	F	F
F	T	F	T
F	F	F	T

Slide 4: (r \implies s) \land (r \implies $\lnot$s) |-|=-

• Intuitively, if r implies both s and $\lnot$s, then r must be false.
• Truth table for (r \implies s) \land (r \implies $\lnot$s):

r	s	$\lnot$s	(r \implies s) \land (r \implies $\lnot$s)
T	T	F	F
T	F	F	F
F	T	T	T
F	F	T	T

Slide 5: p \vdash q

• Notation: p \vdash q means q is provable from p using inference rules.
• Example:
  • A \implies B, $\lnot$A, therefore $\lnot$B

Slide 6: Differences Between |-|=- and $\vdash$

• |= indicates semantic entailment (truth conditions).
• \vdash represents syntactic derivation (inference rules).

Slide 7: Recap on Inference Rules

• Example inference rules:

  • Modus Ponens ($\implies$Elim):

    p \implies q, p \vdash q

  • Conjunction Introduction ($\land$Intro):

    p \vdash q, p \vdash r \vdash p \land q

  • Conditional Proof ($\implies$Intro):

    p \vdash r, p \vdash s \vdash p \implies (r \land s)

Slide 8: Layout of an Inference Rule

• Premises above the line, conclusion below the line.

• Example inference rule ($\implies$Intro):

  p \vdash r, p \vdash s p \implies (r \land s)

Slide 9: Presentation of Proofs

• Steps:
  • Number each step.
  • Justify each step with previous line(s) and inference rule used.

Slide 10: Deriving $\lnot$p \implies r From (p \land q) \lor r

• Example proof:

  (p \land q) \lor r, $\lnot$E … $\lnot$p \implies r

Slide 11: Two Special Inference Rules

• Deductive Theorem ($\implies$Intro):

  p \vdash r, p \vdash s p \implies (r \land s)

• Reductio ad absurdum ($\lnot$Intro):

  p \vdash r, p \vdash $\lnot$s p \vdash $\lnot$r

Slide 12: Conditional Proofs

• Strategy: Assume p, deduce q if possible, discharge assumption.

• Example:

  (p \land q) \lor r … $\lnot$p \implies r

Slide 13: Indirect Proofs

• Strategy: Assume negation of goal, deduce contradiction.

• Example:

  (p \land q) \lor r … $\lnot$p \implies r

Slide 14: Solution to Exercise

Given argument: A (You eat carefully) ⇒ B (You have a healthy digestive system) C (You exercise regularly) ⇒ D (You are very fit) B ∨ D ⇒ E (You live to a ripe old age) ¬E Therefore, ¬A ∧ ¬C

Proof:

Line	Formula	Justification
1	A ⇒ B	Premise
2	C ⇒ D	Premise
3	B ∨ D ⇒ E	Premise
4	¬E	Premise
5	¬(B ∨ D)	Modus Tollens (3, 4)
6	¬B ∧ ¬D	De Morgan's Law (5)
7	¬B	∧Elim (6)
8	¬A	Modus Tollens (1, 7)
9	¬D	∧Elim (6)
10	¬C	Modus Tollens (2, 9)
11	¬A ∧ ¬C	∧Intro (8, 10)

Conclusion: We have proven that ¬A ∧ ¬C, i.e., you did not eat carefully and you did not exercise regularly.

Slide 15: Two Special Inference Rules (continued)

• Deductive Theorem:

  p \vdash r, p \vdash s p \implies (r \land s)

• Reductio ad absurdum:

  p \vdash r, p \vdash $\lnot$s p \vdash $\lnot$r

Slide 16: Soundness and Completeness

• Sound: Valid argument with true premises.
• Complete: Derives any sentence entailed by premises.

Slide 17: Formal Proofs of Natural Language Arguments

• Steps:
  • Identify atomic propositions.
  • Formalize argument in logic.
  • Check for invalidity.
  • Attempt proof.

Slide 18: Example - Travel

• Argument:

  … Therefore, if my neighbours claim to be impressed then they are just pretending.

Slide 19: Example - Travel (continued)

• Formalize argument:

  p \implies q, $\lnot$p \implies $\lnot$r, $\lnot$q … $\lnot$r

• Proof:

  … $\lnot$p \implies r

Slide 20: Example - Nutrition

• Argument:

  … Therefore, you did not eat carefully and you did not exercise regularly.

Slide 21: Example - Nutrition (continued)

• Formalize argument: A \implies B, C \implies D, B \lor D \implies E, $\lnot$E … $\lnot$A \land $\lnot$C
• Proof: … $\lnot$A \land $\lnot$C

Slide 22: Application to Software Engineering

• Questions about software specifications and claims are arguments.

Slide 23: Reading and References

• Russell and Norvig, Artificial Intelligence (4th Edition)
• Nissanke, Introductory Logic and Sets for Computer Scientists
• Gray, Logic, Algebra and Databases