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.
Reference
уреди- ^ Davis, Martin; Putnam, Hilary (1960). „A Computing Procedure for Quantification Theory”. J. ACM. 7 (3): 201—215. S2CID 31888376. doi:10.1145/321033.321034
. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".
- ^ Robinson 1965
Literatura
уреди- Robinson, J. Alan (1965). „A Machine-Oriented Logic Based on the Resolution Principle”. Journal of the ACM. 12 (1): 23—41. S2CID 14389185. doi:10.1145/321250.321253 .
- Leitsch, Alexander (1997). The Resolution Calculus. Texts in Theoretical Computer Science. An EATCS Series. Springer. ISBN 978-3-642-60605-2.
- Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row.
- Lee, Chin-Liang Chang, Richard Char-Tung (1987). Symbolic logic and mechanical theorem proving
. Academic Press. ISBN 0-12-170350-9.
Spoljašnje veze
уреди- Alex Sakharov. „Resolution Principle”. MathWorld.
- Alex Sakharov. „Resolution”. MathWorld.