Completitud y decidibilidad

• Modus Ponens generalizado es incompleto
  
  
  
  
  no podemos probar S(A) a pesar de que es una consecuencia lógica de la KB
  es debido a que no puede convertirse a sentencia de Horn y no podemos aplicar MPG
• Teorema de la completitud de Gödel, para FOL
  
  si una sentencia es una consecuencia lógica de la KB entonces existe un mecanismo de inferencia para probarla (Robinson lo encontró en 1965, resolución)
• Pero dada una sentencia arbitraria, podemos probar que es una consecuencia lógica de la KB?
  • si lo es podemos probarlo, pero si no lo es no siempre podemos probar que no lo es; la consecuencia lógica en FOL es semidecidible
  • la consistencia de un conjunto de sentencias (ver si hay una manera de que todas sean ciertas) también es semidecidible