Modus Ponens generalizado

• para las sentencias atómicas , siempre que haya una substitución tal que entonces para todo i:
  
• es una regla de inferencia eficiente por:
  • combina varias reglas de inferencia en una
  • usa substituciones en lugar de intentar aleatoriamente eliminaciones del universal (algoritmo de unificación)
  • todas las sentencias de la base de conocimiento deben convertirse a forma canónica
• forma canónica
  cada sentencia de la KB debe ser una sentencia atómica o una implicación con una conjunción de sentencias atómicas en la parte izquierda y una sentencia atómica en la parte derecha (sentencias de Horn, KB forma normal de Horn)
  las sentencias se convierten a sentencias de Horn usando eliminación del existencial y eliminación de and
• unificación
  
  supongamos una KB (implícitamente las variables están universalmente cuantificadas)
  
  Conoce(Juan, Juana)
  Conoce(x, Isabel)
  unificando el antecedente de la regla con los hechos de la kb:
  Unify(Conoce(Juan, x), Conoce(Juan, Juana))={x/Juana}
  de donde podemos inferir
  Subst({x/Juana}, Odia(Juan,x))=Odia(Juan, Juana)
  pero Unify(Conoce(Juan, x), Conoce(x, Isabel))=fallo
  esto es debido a un conflicto en el nombre de las variables, necesitamos normalizar por separado (standardize apart) los nombres de las variables, podemos hacerlo renombrando las variables del segundo argumento (de hecho es irrelevante que en la KB tengamos Conoce(x, Isabel) o Conoce(y, Isabel)), así
  Unify(Conoce(Juan, x), Conoce(y, Isabel))={x/Isabel, y/Juan}
  de donce podemos inferir
  Subst({x/Isabel, y/Juan}, Odia(Juan,x)=Odia(Juan, Isabel)
  
  si hay una substitución que hace los dos argumentos iguales hay un número infinito:
  Unify(Conoce(Juan, x), Conoce(y,z))={y/Juan, x/z}
  o {y/Juan, x/z, w/Pedro}
  o {y/Juan, x/Juan, z/Juan, }
  o ...
  supondremos que la rutina de unificación devuelve el unificador más general (MGU), es decir, el que hace menos compromisos en la ligadura de las variables, en este caso {y/Juan, x/z}