In 1965, Robinson propune principiul rezolutiei ca metoda eficienta de demonstrare a teoremelor, principiu care reprezinta baza tuturor demonstratoarelor automate de teoreme actuale. Rezolutia este o metoda de inferenta sintactica care, aplicata repetat unei multimi de formule in forma standard, determina daca multimea de formule este inconsistenta. Pentru a demonstra ca formula C este o consecinta logica a formulelor , se demonstreaza ca este o formula nerealizabila prin deducerea unei contradictii.
Principiul rezolutiei este o metoda de demonstrare prin respingere, care corespunde in general unei demonstrari prin reducere la absurd. De aceea, utilizarea principiului rezolutiei in demonstrarea teoremelor se mai numeste si metoda respingerii prin rezolutie sau respingere rezolutiva. Metoda rezolutiei se aplica insa unei forme standard a formulelor, numita forma clauzala, forma introdusa de Davis si Putnam.
3.3.1 Transformarea formulelor in forma clauzala
Definitie. Se numeste clauza o disjunctie de literali. Se numeste clauza de baza o clauza fara variabile. Se numeste clauza Horn o clauza care contine cel mult un literal pozitiv.
Definitie. Se numeste clauza vida o clauza fara nici un literal; clauza vida se noteaza, prin conventie, cu . Se numeste clauza unitara o clauza ce contine un singur literal.
