[go: up one dir, main page]
Scribd
Upload
57 views13 pages

Prolog 06 Conversion

The document describes the 9 step process of converting a logical statement to clause form: 1) Eliminate implications 2) Reduce the scope of negation 3) Standardize variables apart 4) Move quantifiers to the left 5) Introduce Skolem functions to eliminate existential quantifiers 6) Drop universal quantifiers as they are assumed 7) Create a conjunction of disjuncts 8) Break into separate clauses for each conjunction 9) Standardize variables between clauses This process is demonstrated on the example of converting "All Romans who know Marcus either hate Caesar or think anyone who hates anyone is crazy" to clause form.

Uploaded by

jaypee peng
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPT, PDF, TXT or read online on Scribd
57 views13 pages

Prolog 06 Conversion

The document describes the 9 step process of converting a logical statement to clause form: 1) Eliminate implications 2) Reduce the scope of negation 3) Standardize variables apart 4) Move quantifiers to the left 5) Introduce Skolem functions to eliminate existential quantifiers 6) Drop universal quantifiers as they are assumed 7) Create a conjunction of disjuncts 8) Break into separate clauses for each conjunction 9) Standardize variables between clauses This process is demonstrated on the example of converting "All Romans who know Marcus either hate Caesar or think anyone who hates anyone is crazy" to clause form.

Uploaded by

jaypee peng
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPT, PDF, TXT or read online on Scribd
You are on page 1/ 13

Prolog

Conversion to clause form


Reference: Artificial Intelligence, by Elaine Rich and Kevin Knight
I’m thinking of something.

A. Animal
B. Vegetable
C. Mineral

0% 0% 0%

al le l
ra
im ab n e
An get M
i
Ve
Running example
 All Romans who know Marcus either hate Caesar or
think that anyone who hates anyone is crazy

 x, [ Roman(x)  know(x, Marcus) ] 


[ hate(x, Caesar) 
(y, z, hate(y, z)  thinkCrazy(x, y))]

3
Step 1: Eliminate implications
 Use the fact that x  y is equivalent to x  y

 x, [ Roman(x)  know(x, Marcus) ] 


[ hate(x, Caesar) 
(y, z, hate(y, z)  thinkCrazy(x, y))]

 x, [ Roman(x)  know(x, Marcus) ] 


[hate(x, Caesar) 
(y, (z, hate(y, z)  thinkCrazy(x, y))]

4
Step 2: Reduce the scope of 
 Reduce the scope of negation to a single term, using:
 (p)  p
 (a  b)  (a  b)
 (a  b)  (a  b)
 x, p(x)  x, p(x)
 x, p(x)  x, p(x)

 x, [ Roman(x)  know(x, Marcus) ] 


[hate(x, Caesar) 
(y, (z, hate(y, z)  thinkCrazy(x, y))]

 x, [ Roman(x)  know(x, Marcus) ] 


[hate(x, Caesar) 
(y, z, hate(y, z)  thinkCrazy(x, y))]

5
Step 3: Standardize variables apart
 x, P(x)  x, Q(x)
becomes
x, P(x)  y, Q(y)
 This is just to keep the scopes of variables from getting
confused
 Not necessary in our running example

6
Step 4: Move quantifiers
 Move all quantifiers to the left, without changing their
relative positions

 x, [ Roman(x)  know(x, Marcus) ] 


[hate(x, Caesar) 
(y, z, hate(y, z)  thinkCrazy(x, y)]

 x, y, z,[ Roman(x)  know(x, Marcus) ] 


[hate(x, Caesar) 
(hate(y, z)  thinkCrazy(x, y))]

7
Step 5: Eliminate existential quantifiers
 We do this by introducing Skolem functions:
 If x, p(x) then just pick one; call it x’
 If the existential quantifier is under control of a universal
quantifier, then the picked value has to be a function of the
universally quantified variable:
 If x, y, p(x, y) then x, p(x, y(x))

 Not necessary in our running example

8
Step 6: Drop the prefix (quantifiers)
 x, y, z,[ Roman(x)  know(x, Marcus) ] 
[hate(x, Caesar)  (hate(y, z)  thinkCrazy(x, y))]
 At this point, all the quantifiers are universal quantifiers
 We can just take it for granted that all variables are
universally quantified
 [ Roman(x)  know(x, Marcus) ] 
[hate(x, Caesar)  (hate(y, z)  thinkCrazy(x, y))]

9
Step 7: Create a conjunction of disjuncts
 [ Roman(x)  know(x, Marcus) ] 
[hate(x, Caesar)  (hate(y, z)  thinkCrazy(x, y))]

becomes

Roman(x)  know(x, Marcus) 


hate(x, Caesar)  hate(y, z)  thinkCrazy(x, y)

10
Step 8: Create separate clauses
 Every place we have an , we break our expression up
into separate pieces
 Not necessary in our running example

11
Step 9: Standardize apart
 Rename variables so that no two clauses have the same
variable
 Not necessary in our running example

 Final result:
Roman(x)  know(x, Marcus) 
hate(x, Caesar)  hate(y, z)  thinkCrazy(x, y)

 That’s it! It’s a long process, but easy enough to do


mechanically

12
The End

13

You might also like