"eeldusdisjunktidega" - 1 õppematerjal

Loogilise programmeerimise 1.kontrolltöö konspekt

faktidest. NB! Faktide puudumine tähendab faktide mittekehtimist so faktide puudumine ei tähenda määramatust! 4.2 Resolutsiooni meetod Resolutsioon - Horni lausete kujul oleva deduktiivse süsteemi tuletusreegel. Ø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.