40g人工智能算法课.pdf

Unsatisfiability

1

DemonstratingUnsatisfiability

Startwithpremises.

Applyresolutionrepeatedly.

Ifemptyclausegenerated,theoriginalsetisunsatisfiable.

2

Example

1.{p(a,b),q(a,c)}Premise

2.{¬p(x,y),r(x)}Premise

3.{¬q(x,y),r(x)}Premise

4.{¬r(z)}Premise

3

Example

1.{p(a,b),q(a,c)}Premise

2.{¬p(x,y),r(x)}Premise

3.{¬q(x,y),r(x)}Premise

4.{¬r(z)}Premise

5.{q(a,c),r(a)}1,2

4

Example

1.{p(a,b),q(a,c)}Premise

2.{¬p(x,y),r(x)}Premise

3.{¬q(x,y),r(x)}Premise

4.{¬r(z)}Premise

5.{q(a,c),r(a)}1,2

6.{r(a)}5,3

5

Example

1.{p(a,b),q(a,c)}Premise

2.{¬p(x,y),r(x)}Premise

3.{¬q(x,y),r(x)}Premise

4.{¬r(z)}Premise