Conversion to Canonical Form

• Result of moving quantifiers left

  (exists ?i (or (not (Type ?g OR))
  
  (and (or (not (Signal (Out 1 ?g) On))
  (Signal (In ?i ?g) On))
  (or (not (Signal (In ?j ?g) On))
  (Signal (Out 1 ?g) On)))))

• Skolemize

  (or (not (Type ?g OR))
  
  (and (or (not (Signal (Out 1 ?g) On))
  (Signal (In (Sk1 ?g ?j) ?g) On))
  (or (not (Signal (In ?j ?g) On))
  (Signal (Out 1 ?g) On))))

• Distribute “and” over “or”

Previous slide

Next slide

Back to first slide

View graphic version