CSE 311 Lecture 08: Inference Rules and Proofs for Predicate ...

[Pages:70]CSE 311 Lecture 08: Inference Rules and Proofs for Predicate Logic

Emina Torlak and Kevin Zatloukal

1

Topics

Propositional logic proofs A brief review of Lecture 07.

A quick look at predicate logic proofs Inference rules for quantifiers and a "hello" world example.

An in-depth look at predicate logic proofs Understanding rules for quantifiers through more advanced examples.

2

Propositional logic proofs

A brief review of Lecture 07.

3

Inference rules for propositional logic

Two rules per binary connective: to eliminate and introduce it.

Intro

A; B AB

Elim

AB A, B

Intro

A A B, B A

Elim

A B; ?A B

AB Direct Proof Rule A B

A; A B

Modus Ponens

B

Direct Proof Rule is special: not like the other rules.

4

Proving implications with the direct proof rule

AB Direct Proof Rule A B The premise A B means "Given A, we can prove B."

So the direct proof rule says that if we have such a proof, then we can

conclude that A B is true.

5

Proving implications with the direct proof rule

AB Direct Proof Rule A B

The premise A B means "Given A, we can prove B."

So the direct proof rule says that if we have such a proof, then we can

conclude that A B is true.

Example: prove (p q) (p q).

1.1. p q 1.2. p 1.3. p q

Assumption

2. (p q) (p q) Direct Proof Rule

Indent the proof subroutine. Write the assumption and the goal.

5

Proving implications with the direct proof rule

AB Direct Proof Rule A B

The premise A B means "Given A, we can prove B."

So the direct proof rule says that if we have such a proof, then we can

conclude that A B is true.

Example: prove (p q) (p q).

1.1. p q 1.2. p 1.3. p q

Assumption

Elim : 1.1 Intro : 1.2

2. (p q) (p q) Direct Proof Rule

Indent the proof subroutine. Write the assumption and the goal. Fill in the steps.

5

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download