next up previous contents
Next: Ring (ring) Up: No Title Previous: Prolog

Resolutsioonireegel (resolution)

- resolutsiooniprintsiip - tuletusreegel predikaatarvutuse disjunktide tuletamiseks:

displaymath531

kus s on literaalide L ja L' üldiseim unifikaator. Resolutsioonireegel on (koos skolemiseerimisega) täielik esimest järku klassikalises predikaatarvutuses: valem A on tuletatav parajasti siis, kui tema eitusega samaväärsest disjunktide hulgast on resolutsioonmeetodil tuletatav tühi disjunkt.



Jaan Penjam
Mon Sep 2 19:01:04 EET DST 1996