resolucion proposicional

Es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto (en inglés refutational complete and sound) para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacibles. Por otro lado si el conjunto de proposiciones de hecho es satisfacible, puede o no terminar en una cantidad finita de pasos una demostración por resolución, generalmente lo que sucede es que se asigna un tiempo límite para hallar si un conjunto es insatisfacible o no.


algoritmo
Sea U = {u1, u2, . . . , un} un conjunto de variables booleanas. Una asignaci´on de verdad para U es una funci´on t : U −→ {0, 1}. Si t(u) = 1 decimos que u es verdadera bajo t; si t(u) = 0 decimos que u es falsa. Si u es una variable de U entonces u y u son literales sobre U. El literal u es verdadero bajo t si y s´olo si

EJEMPLOS
¿Es inconsistente por resolucion {{p}, {¬p, q}, {¬q}}? Sı (*)
 ¿Es inconsistente por resolucion {{p}, {¬p, q}}? No
¿Es inconsistente por resolucion {{p, q}, {¬p, q}, {p,¬q}, {¬p,¬q}}? Sı