Rezolucija (logika)

U matematičkoj logici i automatizovanom dokazivanju teorema, rezolucija je pravilo zaključivanja koje vodi do tehnike dokazivanja teorema potpunog pobijanja za rečenice u propozicionoj logici i logici prvog reda. Za propozicionu logiku, sistematska primena pravila rezolucije deluje kao postupak odlučivanja za nezadovoljivost formule, rešavajući (komplement) Bulovog problema zadovoljivosti. Za logiku prvog reda, rezolucija se može koristiti kao osnova za polualgoritam za problem nezadovoljivosti logike prvog reda, pružajući praktičniji metod od onog koji sledi iz Gedelove teoreme potpunosti.

Pravilo rezolucije se može pratiti do Dejvisa i Putnama (1960);^[1] međutim, njihov algoritam je zahtevao isprobavanje svih osnovnih instanci date formule. Ovaj izvor kombinatorne eksplozije eliminisan je 1965. godine algoritmom sintaksičke unifikacije Džona Alana Robinsona, koji je omogućio instanciranje formule tokom dokaza „na zahtev“ onoliko koliko je potrebno da bi se pobijanje održalo u potpunosti.^[2]

Klauzula proizvedena pravilom rezolucije ponekad se naziva rezolventom.