Conversion to Canonical Form

• Result of moving “not” inwards

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

• Standardize Variables

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

• Move Quantifiers Left

Previous slide

Next slide

Back to first slide

View graphic version