Iti0210ex7

Allikas: Lambda

Loogika ja järeldamine

Kasuta solverit http://logictools.org

Hoiatus: vali lahendusmeetodiks resolution või truth table, dpll võib olla bugine

Soojendus

Leia kõik väärtustused mil (A v B) & ~A on tõene

Lahendus

Sisesta see valem solveri valemikasti ja vajuta "Build" (a truth table).

"Result" kasti tekib:

A B | (A V B) & -A
––––––––––––––––––
0 0 |    0    0 1 
0 1 |    1    1 1 
1 0 |    1    0 0 
1 1 |    1    0 0 

Avaldise väärtus on sümboli "&" all, sest see on kõige viimane tehe, mis tehakse. Nagu näha, siis vastus on A=0, B=1. Võid seda käsitsi kontrollida.

Tõestus

Tõesta DeMorgani seadus

~(A & B) <=> ~A v ~B

Lahendus

Tegu on "seadusega" siis kui ta kehtib igal juhul. Sisesta valemikasti ~(A & B) <=> (~A v ~B), vajuta "Build" truth table ja kui näed et valemi väärtus alati 1, siis tegu ongi tõestusega (case by case).

Tõestus vastuolu kaudu

Loengus õppisime, et kui KB -> alpha, siis KB & -alpha peab olema vastuolu. See võimaldab meil järeldumist tõestada ilma täielikku tõeväärtustabelit tegemata.

Teadmine:

Rain -> Cloudy     # kui sajab vihma, siis on pilvine
Rain               # praegu sajab vihma

Tundub, et siit võiks järelduda fakt "Cloudy".

Kodeerime teadmise:

(Rain -> Cloudy) & Rain

Teadmusbaas on üks suur konjunktsioon ("&"-idega liidetud lause) faktidest ja reeglitest. Lisame järeldatava lause eitusega:

(Rain -> Cloudy) & Rain & -Cloudy

Vajuta "Solve", valides meetodiks "resolution".

Clause set is false for all possible assignments to variables.

Lahendust ei ole võimalik leida ehk tegu on vastuoluga. Antud fakt "Cloudy" järeldubki. Kui paned fakti "Rain" asemel "-Rain", siis saad:

Clause set is true for some assignment of values to variables.

Vastuolu enam ei ole ja midagi ei tõestatud.

Teadmusbaas

Tee teadmusbaas (lausearvutuses):

If the unicorn is mythical, then it is immortal, but if it is not mythical, then it is a mortal mammal. If the unicorn is either immortal or a mammal, then it is horned. The unicorn is magical if it is horned.

Küsi teadmusbaasist järgmiste asjade kehtivust:

unicorn is mythical

unicorn is magical

unicorn is horned

Lahendus

Üks võimalik viis teadmist kodeerida:

(Mythical -> Immortal) &
(-Mythical -> Mammal) &
((Immortal v Mammal) -> Horned) &
(Horned -> Magical)

Ja kontrollitav fakt lisandub lihtsalt & -Magical. Kui solver annab vastuseks, et lause ei lahendu, siis fakti Magical järeldumine tõestati.