TheoLog, 1-3

F -> G

NOT F OR G

NOT (F -> G)

F AND NOT G

F

(F -> G) AND (G -> F)

F

(F AND G) OR (NOT F AND NOT G)

NOT (F AND G)

NOT F OR NOT G

NOT (F OR G)

NOT F AND NOT G

NOT NOT F

F

NOT (F

(F AND NOT G) OR (NOT F AND G)

(F AND G) -> H

F -> (G -> H)

F -> (G -> H)

(F AND G) -> H

0 AND 0

0

1 AND 0

0

0 AND 1

0

1 AND 1

1

0 OR 0

0

1 OR 0

1

0 OR 1

1

1 OR 1

1

NOT 0

1

NOT 1

0

0 -> 0

1

1 -> 0

0

0 -> 1

1

1 -> 1

1

0

1

1

0

0

0

1

1

F AND top

F

F AND bot

bot

F OR top

top

F OR bot

F

NOT top

bot

NOT bot

top

F AND F

F

F OR F

F

F AND (F OR G)

F

F OR (F AND G)

F

F AND NOT F

bot

F OR NOT F

top

F AND (G OR H)

(F AND G) OR (F AND H)

F OR (G AND H)

(F OR G) AND (F OR H)

NNF: NOT (F AND G)

NOT F OR NOT G

NNF: NOT (F OR G)

NOT F AND NOT G

NNF: NOT NOT F

F

NNF: NOT (F -> G)

F AND NOT G

NNF: NOT (F

(F AND NOT G) OR (NOT F AND G)

Horn: NOT p OR NOT q OR r

(p AND q) -> r

Horn: p

top -> p

Horn: NOT p OR NOT q

(p AND q) -> bot

Resolvent of {p, NOT q} and {q, r} on q

{p, r}

Resolvent of {p} and {NOT p} on p

bot

Resolvent of {p, q} and {NOT p, NOT q} on p

{q, NOT q}

DNF satisfiable when

at least one monom has no atom both negated and non-negated

KNF tautology when

every clause contains p OR NOT p for some p

KNF from truth table: row = 0, F=1 G=0

NOT F OR G

DNF from truth table: row = 1, F=1 G=0

F AND NOT G

Simplify: (p -> q) -> p -> p

tautology (Peirce's law - check with truth table)

Simplify: NOT (p OR NOT p)

bot

Simplify: NOT (p AND NOT p)

top

Simplify: (p AND q) OR (p AND NOT q)

p

Simplify: (p OR q) AND (p OR NOT q)

p

Simplify: p AND (NOT p OR q)

p AND q

Simplify: p OR (NOT p AND q)

p OR q

Expand: p -> q -> r (right-associative: p -> (q -> r))

(p AND q) -> r

Expand: NOT (p -> q) -> r

(p AND NOT q) -> r i.e. NOT (p AND NOT q) OR r

Rewrite p

NOT (p AND NOT q) AND NOT (q AND NOT p)

Rewrite p

(NOT p OR q) AND (NOT q OR p)

Convert to NNF: NOT (p -> (q AND r))

p AND (NOT q OR NOT r)

Convert to NNF: NOT (NOT p AND q)

p OR NOT q

Convert to NNF: NOT (p

(p AND NOT q) OR (NOT p AND q)

Convert to KNF: (p AND q) OR r

(p OR r) AND (q OR r)

Convert to KNF: p OR (q AND r)

(p OR q) AND (p OR r)

Convert to KNF: NOT (p -> q)

p AND NOT q — already a monom, so KNF = p AND NOT q

Convert to DNF: (p OR q) AND r

(p AND r) OR (q AND r)

Convert to DNF: (p OR q) AND (p OR r)

p OR (q AND r)

Resolvent of {NOT p, q} and {p, NOT q} on p

{q, NOT q}

Resolvent of {NOT p, q} and {p, NOT q} on q

{NOT p, p}

Resolvent of {p, q, r} and {NOT q, NOT r} on q

{p, r, NOT r}

Resolvent of {NOT p, NOT q, r} and {p, q} on p

{NOT q, r, q} simplify: {r, q, NOT q}

Is {p, NOT p OR q, NOT q} satisfiable? Show via resolution

{p} + {NOT p OR q} -> {q}. Then {q} + {NOT q} -> bot. Unsatisfiable.

Is {p OR q, NOT p, NOT q} satisfiable? Show via resolution

{NOT p} + {p OR q} -> {q}. Then {q} + {NOT q} -> bot. Unsatisfiable.

Is {p -> q, q -> r, p} satisfiable? Find model.

Rewrite: {NOT p OR q, NOT q OR r, p}. {p} + {NOT p OR q} -> {q}. {q} + {NOT q OR r} -> {r}. No bot. Model: p=1 q=1 r=1.

w(p)=1 w(q)=0. Value of p -> q

0

w(p)=0 w(q)=1. Value of p -> q

1

w(p)=1 w(q)=0. Value of p

0

w(p)=1 w(q)=1. Value of NOT p OR q

1

w(p)=0 w(q)=0. Value of NOT (p AND q)

1

w(p)=1 w(q)=0. Value of NOT (p OR q)

0

w(p)=1 w(q)=1 w(r)=0. Value of (p AND q) -> r

0

w(p)=0 w(q)=1 w(r)=0. Value of (p AND q) -> r

1

w(p)=1 w(q)=0 w(r)=1. Value of p -> (q OR r)

1

w(p)=1 w(q)=1. Value of (p -> q) AND (q -> p)

1

w(p)=1 w(q)=0. Value of (p -> q) AND (q -> p)

0