leidub veel asendus , nii et = st. iga termi t korral (t) = ((t)) Märkus: mgu annab kõige vähem konkretiseeritud omavahel unifitseeruvad termid. Lause: Leidub algoritm mgu, mis arvutab literaalide või termide x ja y kõige üldisema unifitseerija. Näiteid: mgu(P(a,X), P(Y,b)) = {Y/a, X/b} mgu(P(X, f(X)), P(f(Y), U)) = {X/f(Y), U/f(f(Y))} mgu(L(g(X,X)), L(g(f(a), f(a)))) = {X/f(a)} mgu(R(a,b), R(a,b)) = {} Reegel: Disjunktsioonides, millele rakendatakse üldistatud RR reeglit, tuleb eelnevalt asendada samanimelised muutujad. 7.1. Listid Esitavad järjestatud elementide korteeže List unifitseerub • ühe muutujaga List = [a, d, f, [s, f, [],d]] • Listi erinevaid osi adresseerivate muutujatega, kui on mitte-tühi list [Head|Tail] Head (listi pea) - listi ilmutatult viidatavad esimesed elemendid Tail (listi saba) – ülejäänud listi elemendid | - eraldussümbol. 1
tehe, seega peab kasutama sulge) o TKNK-le viimise algoritm: Elimineerida implikatsioonid ja ekvivalentsid Viia eitused vahetult lausemuutujate ette (st konjunktsioonide ja disjunktsioonide sisse) ,,Liita" konjunktsioonid läbi (teise distributiivsuse seaduse abil) Kaotada samaselt tõesed disjunktsioonid ja sama liikme mitmekordsed esinemised disjunktsioonides Lisada disjunktsioonidele puuduvad muutujad Korrastada valem (järjestada muutujad disjunktsioonides ja kaotada korduvad disjunktsioonid) Lausearvutuse valemid A(X1 ,..., Xn ) ja B(X1 ,..., Xn ) on loogiliselt samaväärsed parajasti siis, kui nende TDNK-d koosnevad samadest elementaarkonjunktsioonidest Lausearvutuse valemist A(X1 ,..., Xn ) järeldub valem B(X1 ,..., Xn ) parajasti
annaabi.ee 
