Conversion to Clause Form

Scheme format:

(A (?x) (  (brick ?x) ->
          (  (E (?y) ((on ?x ?y) & (~ (pyramid ?y))))
           & (~ (E (?y) ((on ?x ?y) & (on ?y ?x))))
           & (A (?y) ((~ (brick ?y)) -> (~ (equal ?x ?y)))) )))

1. Eliminate all of the implications by substituting ~a V b for a -> b.

   

   Scheme format:

   (A (?x) ( (~ (brick ?x)) V
             (  (E (?y) ((on ?x ?y) & (~ (pyramid ?y))))
              & (~ (E (?y) ((on ?x ?y) & (on ?y ?x))))
              & (A (?y) ((~ (~ (brick ?y))) V (~ (equal ?x ?y)))) )))
   

2. Move all of the negations down to the atomic formulas.

   

   Scheme format:

   (A (?x) ( (~ (brick ?x)) V
             (  (E (?y) ((on ?x ?y) & (~ (pyramid ?y))))
              & (A (?y) ((~ (on ?x ?y)) V (~ (on ?y ?x))))
              & (A (?y) ((brick ?y) V (~ (equal ?x ?y)))) )))
   

3. Rename ("standardize") variables so each quantifier has only one.

   

   Scheme format:

   (A (?x) ( (~ (brick ?x)) V
             (  (E (?y) ((on ?x ?y) & (~ (pyramid ?y))))
              & (A (?z) ((~ (on ?x ?z)) V (~ (on ?z ?x))))
              & (A (?w) ((brick ?w) V (~ (equal ?x ?w)))) )))
   

4. Move all quantifiers to the left without changing their order.

   

   Scheme format:

   (A (?x)
     (E (?y)
       (A (?z)
          (A (?w)
             ( (~ (brick ?x))
               V (((on ?x ?y) & (~ (pyramid ?y)))
                  & ((~ (on ?x ?z)) V (~ (on ?z ?x)))
                  & ((brick ?w) V (~ (equal ?x ?w)))) )))))
   

5. Eliminate existential quantifiers by creating Skolem functions or constants.

   

   Scheme format:

   (A (?x)
     (A (?z)
       (A (?w)
          ( (~ (brick ?x))
            V (((on ?x (support ?x)) & (~ (pyramid (support ?x))))
               & ((~ (on ?x ?z)) V (~ (on ?z ?x)))
               & ((brick ?w) V (~ (equal ?x ?w))))) )))
   

6. Drop the universal quantifiers.

   

   Scheme format:

   ( (~ (brick ?x))
     V (((on ?x (support ?x)) & (~ (pyramid (support ?x))))
        & ((~ (on ?x ?z)) V (~ (on ?z ?x)))
        & ((brick ?w) V (~ (equal ?x ?w)))) )
   

7. Move the disjunctions down to the literals.

   

   Scheme format:

   (  ((~ (brick ?x)) V (on ?x (support ?x)))
    & ((~ (brick ?x)) V (~ (pyramid (support ?x))))
    & ((~ (brick ?x)) V (~ (on ?x ?z)) V (~ (on ?z ?x)))
    & ((~ (brick ?x)) V (brick ?w) V (~ (equal ?x ?w))) )
   

8. Make each conjunct into a separate clause.

   

   Scheme format:

   ((~ (brick ?x))  (on ?x (support ?x)))
   ((~ (brick ?x))  (~ (pyramid (support ?x))))
   ((~ (brick ?x))  (~ (on ?x ?z))  (~ (on ?z ?x)))
   ((~ (brick ?x))  (brick ?w)  (~ (equal ?x ?w)))
   

9. Rename ("standardize apart") the variables so that no two clauses use the same variables.

   

   Scheme format:

   ((~ (brick ?x))  (on ?x (support ?x)))
   ((~ (brick ?y))  (~ (pyramid (support ?y))))
   ((~ (brick ?w))  (~ (on ?w ?z))  (~ (on ?z ?w)))
   ((~ (brick ?u))  (brick ?v)  (~ (equal ?u ?v)))
   

Representation and Reasoning: Unification

Representation and Reasoning: Resolution and Variables