Estrategias de resolución

Estrategias para guiar la búsqueda hacia una prueba

• preferencia de cláusula unitaria, intentar la resolución cuando una de las sentencias es un único literal (cláusula unitaria)
• conjunto de apoyo, elegir un subconjunto de sentencias de la KB e intentar la resolución sólo con las sentencias de ese subconjunto, añadiendo los resolventes a ese subconjunto. Si el resto de sentencias son satisfacibles (verificables) la resolución será completa; elegir la negación de la pregunta como conjunto de apoyo (suponemos que la KB original es consistente)
• input resolution, cada resolución combina una de las sentencias de entrada (de la KB o de la pregunta) con alguna otra sentencia. Modus Ponens es una estrategia de este tipo. No es completa
• resolución lineal, P y Q se pueden resolver si P está en la KB original o si P es un ancestro de Q en el árbol de prueba. Es completa
• subsumisión, eliminar sentencias que son más específicas que otras existentes. Si tenemo P(x) en la KB no tiene sentido añadir P(A) o (P(A)or P(B))