"unifitseerija" - 1 õppematerjal

Loogilise programmeerimise 1.kontrolltöö konspekt

Pärast RR iga rakendamist on saadud valemis 2 literaali vähem kui RR eeldusvalemites. Muutujat V sisaldav väide tähistab kõikide konkretiseeritud väidete hulka, kus konkretiseerimise all mõeldakse V asendamist kas konstantide või muutujaid sisaldavate termidega. q Kuidas unifitseerida, kui mõlemad literaalid sisaldavad muutujaid? Minimaalse substitutsiooni reegel: 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}