Formas canónicas

• forma normal conjuntiva (CNF): en la primera version de la regla cada sentencia de la KB es una disyunción de literales, y se supone que estan unidas en una gran conjunción
• forma normal implicativa (INF): en la segunda version de la regla cada sentencia de la KB es una implicación con una conjunción de átomos en la izquierda y una disyunción en la derecha
• son variantes denotacionales
  
  
  
• resolución es una generalización de Modus Ponens
  • INF es más general que las sentencias de Horn
  • es equivalente a