Rezolucja – metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią.
Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu.
Zasady generowania nowych klauzul Zasady generowania nowych klauzul to: z klauzuli można utworzyć i z klauzuli można utworzyć z pary klauzul i gdzie i się unifikują, zaś jest ich najmniejszym unifikatorem – (zasada rezolucji),
gdzie to formuły, – zbiory formuł.
W rachunku zdań reguła rezolucji upraszcza się do: Z pary klauzul i można utworzyć
Jeśli potrafimy dojść do klauzuli pustej, rezolucja jest zakończona i twierdzenie jest sprzeczne (a więc jego zaprzeczenie jest tautologią).
Przykład działania. Udowodnimy, że
Sprowadźmy najpierw do postaci z negacjami na liściach (nie jest to konieczne, ale potrzebne by były wtedy reguły usuwania każdego ze spójników oraz podwójnej negacji):
Rezolucja w działaniu:
i reguły rezolucji