Complejidad de la inferencia proposicional

• método de inferencia usando la tabla de verdad
  • es completo: se pueden enumerar las filas de la tabla para cualquier prueba de una sentencia con n símbolos proposicionales
  • tiempo de computación exponencial en n
• se ha demostrado que chequear la satisfacibilidad de un conjunto de sentencias (SAT problems) es NP-completo
• la lógica proposicional es monótona: añadiendo nuevas sentencias a la KB, todas las sentencias originalmente válidas siguen siéndolo, formalmente
  
• sentencias de Horn
  • con todos los literales positivos
  • si Q es la cte False es equivalente a
  • si es la cte True y n=1 es equivalente a Q
  • existe un método de inferencia de complejidad polinómica: applicar modus ponens mientras sea posible
  • no todas las bases de conocimiento se pueden escribir como colecciones de cláusulas Horn