Resolutsioon on mehaaniline tõestusmeetod. Selle asemel et otse näidata, et väide järeldub, võtame järelduse eituse ja näitame, et see eitus koos eeldustega teeb vastuolu – toob tühja klausli □. Vastuolu tähendab: eitust ei saanud olla, järeldus on tõestatud.
Eeldustes võivad olla pikad valemid, kus segunevad implikatsioonid, konjunktsioonid, disjunktsioonid ja eitused. Iga selline üksik valem tuuakse esiteks normaalsele klauslikujule (DNF). Eeldusi kasutatakse tõestamisel: eeldustes loetletud üksikud valemid paigutatakse samm-sammult puusse, et oleks võimalik rakendada resolutsiooni reeglit.
Vajalikud reeglid: X → Y ≡ ¬X ∨ Y · De Morgan: ¬(X ∧ Y) ≡ ¬X ∨ ¬Y, ¬(X ∨ Y) ≡ ¬X ∧ ¬Y · ¬¬X ≡ X
Tahame tõestada V. Lisame hulga klauslisse tema eituse ¬V. Kui resolutsioon viib selleni, et □ tuleb kätte, oli hulk vastuoluline ja V on tõestatud.
Võtame kaks klauslit. Ühes on mingi literaal A, teises tema täiend ¬A. Need kaks „punast“ literaali taanduvad – üle jääb kõigi muude literaalide disjunktsioon, ehk resolvent:
Näide: p ∨ q ja ¬p ∨ r annavad resolventi q ∨ r. Kui rohkem literaale ei jää, on tulem □ – tühi klausel, st vastuolu.
„Kui sajab, siis on märg. Kui on märg, siis peab olema vihmavari. Sajab.“ Tõesta: on vihmavari. S = sajab, M = märg, V = vihmavari
Klauslid: (1) ¬S ∨ M · (2) ¬M ∨ V · (3) S · (4) ¬V (järelduse eitus). Resolutsioon samm-sammult:
Tekkis □ ⇒ vastuolu ⇒ „vihmavari ei ole“ on võimatu ⇒ vihmavari on.
Ülesanne. „Kui kohv on kuum, siis aurab. Kui aurab, siis tuleb ettevaatlik olla. Kohv on kuum.“ Tõesta: tuleb ettevaatlik olla.
K = kohv on kuum, A = aurab, E = tuleb ettevaatlik olla
Ülesanne. „Kui Mari treenib, siis ta võidab. Kui ta võidab, siis ta rõõmustab. Mari treenib.“ Tõesta: Mari rõõmustab.
M = treenib, T = võidab, R = rõõmustab. Klauslid: (1) ¬M ∨ T · (2) ¬T ∨ R · (3) M · (4) ¬R
Klauslid (1), (3) ja (4) on antud. Kirjuta klausel (2) ja tühjadesse kastidesse resolvendid – kokku kolm resolutsioonisammu, et jõuda □-ni. Vajadusel vihje ühe kaupa.
Ülesanne. „Kui ilm on pilvine, siis tõuseb tuul. Kui tuul tõuseb, siis lainetavad puud. Ilm on pilvine.“ Tõesta: puud lainetavad.
I = ilm on pilvine, T = tõuseb tuul, P = puud lainetavad.
Siin pole ühtegi kasti ette antud: kirjuta kõikidesse kastidesse sobivad klauslid ja resolvendid. „Vihje“ toob ühe vihje ja avab ühe kasti – samm kaupa, mitte kõike korraga.
Ülesanne. „Kui aku on tühi ja ekraan on põlema jäänud, siis läheb vool välja. Kui vool läheb välja, siis kaovad andmed. Aku on tühi. Ekraan on põlema jäänud.“ Tõesta: andmed kaovad.
A = aku on tühi, E = ekraan on põlema jäänud, V = vool läheb välja, D = andmed kaovad. Järelduse eitus: ¬D.
Osad valemid pole veel klauslid. Kasuta reegleid: X → Y ≡ ¬X ∨ Y ja ¬(X ∧ Y) ≡ ¬X ∨ ¬Y.
Klauslid: (1) ¬A ∨ ¬E ∨ V · (2) ¬V ∨ D · (3) A · (4) E · (5) ¬D. Kirjuta iga resolvent kasti. Vihjed tulevad samm-sammult nupust „Vihje“.
Ülesanne. „Kui töö on tehtud ja aeg on käes, siis saab puhata. Kui saab puhata, siis meeleolu paraneb. Töö on tehtud. Aeg on käes.“ Tõesta: meeleolu paraneb.
T = töö on tehtud, A = aeg on käes, P = saab puhata, M = meeleolu paraneb. Järelduse eitus: ¬M.
Nüüd pole midagi ette antud – kirjuta kõik kastid ise. „Vihje“ annab samm-sammult vihje ja avab korraga ühe kasti.