Asendamata jäetakse kõik muutujad, mille jaoks puudub konkretiseeriv asendus. Definitsioon (Kõige üldisem unifitseerija - mgu): Termide t1 ja t2 kõige üldisem unifitseerija on asendus , mis rahuldab tingimusi: 1. on termide t1 ja t2 unifitseerija t1 ja t2 iga unifitseerija korral 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]]
kasutatavaid elemente. y1’ = x2’x3 x4 + x2 x3’+ x2 x4’ + x1’x4’ /x2 --> x3’+ x4’ /x4’ --> x2 + x1’ y2 = x3’x4’ + x2’x3 x4 + x1’x2’ + x1’x4’ /x1’ --> x2’ + x4’ /x2’ --> x3 x4 + x1’ /x4’ --> x3’ + x1’ y3 = x1’x3 + x1x3’+ x2x3’ /x3’ --> x1 + x2 y4’ = x2’x3 x4 + x1 x3’+ x2 x4’ Järelduste tegemisel on eeldatud, et 4-AND realiseerub 3-AND ja 2-AND elementidena ning 4-OR kui 3-OR + 2-OR. Samuti on hinnatud literaalide (sisendite arvu) muutust (nt. ’[11->9]’). ’#2’ näitab, millised variandid on valitud skeemi realiseerimiseks. y1’: /x2 : 2-AND + 2-AND + 4-OR --> 2-OR + 2-AND + 3-OR [(2+2+(3+2)=9 -> (2+2+3)=7 parim] /x4’: 2-AND + 2-AND + 4-OR --> 2-OR + 2-AND + 3-OR [(2+2+(3+2)=9 -> (2+2+3)=7 sama] y2: /x1’: 2-AND + 2-AND + 4-OR --> 2-OR + 2-And + 3-OR [2+2+(3+2)=9 -> 2+2+3=7 valitud]
kirjeldused. TDNK olemasolu ja ühesus. TDNK-le teisendamise algoritm, tema etappidel kasutatavad samaväärsused. [1] Literaal o DEF: Literaaliks nimetatakse lausemuutujat või selle eitust, literaale loetakse positiivseks või negatiivseks vastavalt selelle, kas ta on puhas lausemuutuja või koos eitusega. N: A, B, ¬C Täielik elementaalkonjuktsioon o DEF: Muutujate X1, X2…, Xn täielikuks elementaarkonjunktsiooniks nimetatakse literaalide konjunktsiooni L1&L2&,..., &Ln Täielik disjunktiivne normaalkuju o DEF: Lausearvutuse valemi F täielikuks disjunktiivseks normaalkujuks (TDNK) nimetatakse valemiga F samaväärset valemit, mis kujutab endast erinevate täielike elementaarkonjunktsioonide disjunktsiooni. Tõestuspiirkondade kirjeldused TDNK olemasolu ja ühesus Teoreem. Kui valem F ei ole samaselt väär, siis tal leidub täielikdisjunktiivne normaalkuju. Järeldus
annaabi.ee 
