Resolución Semántica

controlada por la semántica declarativa

Idea: dividir al conjunto insatisfacible de cláusulas $C$, en dos conjuntos, basados en una interpretación $I$ particular:

• $S_1$ los que son verdaderos y
• $S_2$ los que son falsos

Como $S$ es insatisfacible, no existe una interpretación que haga los dos conjuntos verdaderos o falsos.

Escoger una claúsula de $S_1$ y una de $S_2$ y añadir el resolvente a donde le corresponda

e.g., $S = \{P, \neg P \vee Q, \neg P \vee \neg Q \vee R, \neg R\}$

$I:$ (interpretación)
$I(P) = false$
$I(Q) = false$
$I(R) = false$

$S_1 = \{P\}$
$S_2 = \{\neg P \vee Q, \neg P \vee \neg Q \vee R, \neg R\}$

Variantes: asignar un orden a las literales de las cláusulas