7-ma'ruza. Sun’iy intellektda mantiqiy xulosalashlar Reja

Teskari deduksiylar tizimlari. Teskari deduksiylash tizimlarida yangi xususiy maqsadlarni qurish uchun xulosalar maqsadga yoki qoidalarga qo’llaniladi [1, 18]. Algoritm o’z ishini barcha xususiy maqsadlar faktlarga mos kelganda tugatadi. Bunday tizim mantiqiy nuqtai-nazaridan teskari deduksiyalash teoremasini qo’llaydigan tizim sifatida qaralsa, u holda uni quyidagicha ifodalash mumkin: agar F₁, F_2,….,F_n; G-mantiqiy ifodalar bo’lsa, u holda G faqat va faqat shundagina F₁, F_2,… F_n ning dizyunktlari bo’ladi, agarda aynan chin, ya’ni umumqiymatli ifoda bo’lsa.
Teskari dedyksiylash tizimlarida kelishuv qoidalarini (pravila soglasie) qo’llash uchun qoidalar va maqsadlar konyunktlarni almashtiradi. Kelishuv qoidalari rezolyutsiyalar qoidasiga ikkitaraflama. Agar ularni p ∧ c₁ va konyunksiyaga qo’llasak, u holda c₁∧ c₂ konyunksiyani hosil qilamiz.
Bu amallar mulohazalar algebrasi doirasida kiritilgan.
Misol.
1) Bosqich 1: Kelishuv qoidasidan foydalanib, Maqsad (1) va Qoida (1) ning inkoridan yangi Maqsad (2) ni hosil qilamiz:

Maqsad(1)	-(Qoida (1))
Imt (Jumanov 1, Maftuna 4)	Prof(x,y) ˄ Tal(z,w) ˄ - (Teng (x,z)) ˄-(Imt(y,w))

Maqsad (2): Prof ( x; Jumanov 1) ∧ Tal (z; Maftuna 4) ∧ - (Teng( x; z)).

2) Bosqich 2: Kelishuv qoidasidan foydalanib Maqsad(2) va fakt(1) ning inkoridan Maqsad(3) hosil qilamiz:

Maqsad(2)	-(Fakt (1))
Prof (х,Jumanov1) ˄ Tal (z,Maftuna4) ˄-(Teng (x,z)	-(Prof (Dast, Jumanov 1)

Maqsad(3): Tal(z; Maftuna 4)∧ -(Teng(dast; z).
3) Bosqich 3: Maqsad(3) va Fakt(2)ning inkoridan teoremani hosil qilamiz: