Loogilise programmeerimise 1.kontrolltöö konspekt
ØValem Δ ⇒ D kehtib parajasti siis, kui tema eitus ¬ (Δ ⇒ D) ≡ Δ ∧¬ D on vasturääkiv.
ØHorni lause tõestamiseks tõestatakse, et positiivse literaali eituse konjunktsioonist
eeldusdisjunktidega saab tuletada vastuolu.
Øst temast saab tuletada tühja disjunkti.
Tühja disjunkti tuletamiseks kasutame klassikalise loogika reegli modus
ponens üldistust - resolutsiooni reeglit (RR).
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
annaabi.ee 
