5 Inteligentní usuzování Jak již bylo řečeno v předcházející kapitole, způsob reprezentování znalostí a způsob jejich využívaní pro usuzování spolu úzce souvisejí. Připomeňme zde tedy ještě jednou používaná teoretická východiska (pro reprezentování znalostí i inteligentní usuzování) a čelné představitele jednotlivých přístupů, tak jak to prezentují Davis, Shrobe a Szolovits (Davis, Shrobe, Szolovits, 1993). MATHEMATICAL LOGIC
PSYCHOLOGY
BIOLOGY
STATISTICS
ECONOMICS
Laplace
Bentham Pareto Friedman
Aristotle Descartes Boole
James
Frege Peano
Bernoulli
Goedel Post Church Turing Davis Putnam Robinson LOGIC PROLOG
Hebb Bruner Miller Newell, Simon
Lashley Bayes Rosenblatt Ashby Tversky, Lettvin Kahneman McCulloch, Pitts Heubel, Weisel
SOAR KBS, FRAMES
CONNECTIONISM
CAUSAL NETWORKS
Von Neumann Simon Raiffa
RATIONAL AGENTS
Tab. 5.1 Přístupy k inteligentnímu usuzování
5.1 Výroková logika 5.1.1 Pravdivost formulí Pravdivost formulí se vyhodnocuje na základě přiřazení pravdivostních hodnot (konstant 1 a 0) proměnným (tzv. interpretace). Z hlediska jejich pravdivosti můžeme formule dělit na: •
tautologie – formule, které jsou pravdivé pro libovolné přiřazení (např. ϕ ∨ ¬ϕ)
•
kontradikce (nesplnitelné formule) – formule, které nejsou pravdivé pro žádné přiřazení (např. ϕ ∧ ¬ϕ)
•
splnitelné formule – formule, pro které existuje interpretace taková, že formule je pravdivá
Pro zjišťování pravdivosti (splnitelnosti) formulí lze použít několik postupů: Tabulka pravdivostních hodnot Vyčíslíme pravdivostní hodnotu formule pro všechny možné interpretace (viz příklad tabulky pravdivostních hodnot pro formuli (ϕ ∨ ¬ψ) ⇒ ¬ψ). Nevýhodou tohoto přístupu je, že pro n proměnných obsažených ve formulí existuje 2n interpretací.
1
ϕ 0 0 1 1
ψ 0 1 0 1
¬ψ ϕ ∨ ¬ψ 1 1 0 0 1 1 0 1
(ϕ ∨ ¬ψ) ⇒ ¬ψ 1 1 1 0
Tab. 5.2 Tabulka pravdivostních hodnot
Tablová metoda Binární strom, v kořenu je formule A u které mě zajímá splnitelnost, v listech ohodnocené seznamy literálů (výroků a negací výroků) vyskytujících se ve formuli A. Strom je vytvářen tak, že aktuální uzel má jednoho následníka, pokud jednu formuli převádíme na konjunkci dvou formulí (tzv. α pravidla), nebo aktuální uzel má dva následníky, pokud jednu formuli převádíme na disjunkci dvou formulí (tzv. β pravidla). Ohodnocení listu je buď Ο, neobsahuje-li seznam výrok i jeho negaci (tzv. otevřená větev), nebo ×, obsahuje-li seznam výrok i jeho negaci (tzv. uzavřená větev). Formule je kontradikce, pokud její tablo obsahuje pouze uzavřené větve. α
α1
¬¬ψ
ψ
ϕ∧ψ
ϕ
¬(ϕ ∨ ψ)
α2
β
β1
β2
ϕ∨ψ
ϕ
ψ
ψ
¬(ϕ ∧ ψ)
¬ϕ
¬ψ
¬ϕ
¬ψ
ϕ⇒ψ
¬ϕ
ψ
¬(ϕ ⇒ ψ)
ϕ
¬ψ
¬(ϕ ⇔ ψ)
¬(ϕ ⇒ ψ)
¬(ψ ⇒ ϕ)
ϕ⇔ψ
ϕ⇒ψ
ψ⇒ϕ
Tab. 5.3 Alfa a beta pravidla pro tablo
Tedy, pro náš příklad (ϕ ∨ ¬ψ) ⇒ ¬ψ /
\
¬(ϕ ∨ ¬ψ)
¬ψ
|
Ο
¬ϕ, ψ Ο Def: Model formule ϕ je taková interpretace (přiřazení pravdivostních hodnot výrokovým proměnným), že formule ϕ je pravdivá.
2
5.1.2 Odvozování formulí Při odvozování nás zajímají logické důsledky formulí. Def: Formule ϕ je logickým důsledkem množiny formulí U, platí-li pro všechny modely množiny formulí U, že formule ϕ je interpretována pravdivostní hodnotou T. Logický důsledek zapisujeme dvěma možnými způsoby U |= ϕ
nebo
U
ϕ
Věta 1: Nechť U ={ϕ1, ϕ2 ,…, ϕn}. Formule ψ je logickým důsledkem množiny U právě když ϕ 1 ∧ ϕ 2 ∧ … ∧ ϕn ⇒ ψ je tautologie. Věta 2: Nechť U ={ϕ1, ϕ2 ,…, ϕn}. Formule ψ je logickým důsledkem množiny U právě když ϕ1 ∧ ϕ2 ∧ … ∧ ϕn ∧ ¬ψ je nesplnitelná formule. Pro odvozování ve výrokové logice se používá řada pravidel. Patří k nim: •
dedukční pravidlo (modus ponens) ϕ ⇒ ψ, ϕ |= ψ
•
modus tollens ϕ ⇒ ψ, ¬ψ |= ¬ϕ
•
rezoluční pravidlo ϕ ∨ ψ, ¬ϕ ∨ ρ |= ψ ∨ ρ
•
sylogismus ϕ ⇒ ψ, ψ ⇒ ρ |=
•
ϕ⇒ρ
disjunktivní inference ϕ ∨ ψ, ¬ϕ |= ψ
•
konjunktivní inference ϕ, ψ |=
•
ϕ ∧ ψ
zjednodušení ϕ ∧ ψ |=
•
disjunktivní součet ϕ
3
ϕ
|= ϕ ∨ ψ
Věta: Odvozovací pravidlo je korektní (sound), pokud platí: existuje-li model, ve kterém jsou splněny předpoklady pravidla, pak je v tomto modelu splněn i závěr odvozovacího pravidla. Příklad: Dokažte, že {ϕ ∨ ψ, ϕ ∨ ρ, ¬ψ ∨ ¬ ρ} |=
ϕ
Podle Věty 2 budeme dokazovat, že {ϕ ∨ ψ, ϕ ∨ ρ, ¬ψ ∨ ¬ ρ, ¬ϕ} je nesplnitelná množina formulí (tzv. důkaz sporem). Pro odvozování použijeme rezoluční pravidlo ϕ ∨ ψ \
¬ϕ /
ψ
¬ψ ∨ ¬ ρ \
ϕ ∨ ρ
/
\
¬ρ
¬ϕ /
ρ \
/ \
/ \
/ spor
Odvození s využitím tabla by mělo podobu:
ϕ ∨ ψ, ϕ ∨ρ, ¬ψ ∨ ¬ρ, ¬ϕ /
\
ϕ, ϕ ∨ρ, ¬ψ ∨ ¬ρ, ¬ϕ / ϕ, ϕ , ¬ψ ∨ ¬ρ, ¬ϕ / ϕ, ϕ , ¬ψ ,¬ϕ ×
\ ϕ, ϕ , ¬ρ, ¬ϕ ×
ψ, ϕ ∨ρ, ¬ψ ∨ ¬ρ, ¬ϕ
\
/
ϕ, ρ, ¬ψ ∨ ¬ρ, ¬ϕ / ϕ, ρ, ¬ψ, ¬ϕ ×
\ ϕ, ρ, ¬ρ, ¬ϕ ×
ψ, ϕ , ¬ψ ∨ ¬ρ, ¬ϕ / ψ, ϕ , ¬ψ, ¬ϕ ×
\ ψ, ϕ , ¬ρ, ¬ϕ ×
\ ψ, ρ, ¬ψ ∨ ¬ρ, ¬ϕ / ψ, ρ, ¬ψ,¬ϕ ×
\ ψ, ρ, ¬ρ, ¬ϕ ×
Pro aplikaci rezolučního odvozovacího pravidla musíme formule převést do klauzulárního tvaru: •
literál (výrok nebo negace výroku) je klauzule
•
disjunkce klauzulí je klauzule
Věta: Konečná množina klauzulí P nemá model právě tehdy, když lze z P pomocí konečného počtu resolučních kroků odvodit prázdnou klauzuli. Otázku logické dokazatelnosti lze tedy převést na otázku logické splnitelnosti. Je ale třeba mít na paměti skutečnost, že splnitelnost nějaké množiny formulí (tedy existence modelu) neznamená, že formule z této množiny ze sebe logicky vyplývají. 4
Gödelova věta o úplnosti: Formule je logicky platná v teorii T právě když je dokazatelná v teorii T. Věta o rozhodnutelnosti: Pro každou formuli v teorii T lze algoritmicky rozhodnout, zda formule je nebo není dokazatelná. Věta: Výroková logika je úplná a rozhodnutelná.
Příklad: Podezřelý může být vinen jen tehdy, byl-li v době činu v Praze. Podezřelý byl v době činu v Ostravě. Je nevinen? (převzato z Lukasová) Označme v výrok „podezřelý je vinen“, p výrok „podezřelý byl v Praze“ a o výrok „podezřelý byl v Ostravě“. Zadání úlohy pak můžeme formalizovat do podoby formulí v ⇔ p, o, ¬v. Z tabulky pravdivostních hodnot pro tyto formule (Tab. 5.4 ) vidíme, že uvedené tři formule jsou splnitelné (existují dokonce dva modely uvedené v řádcích 2 a 8), ale že z pravdivosti v ⇔ p, o se nedá odvodit jednoznačná pravdivostní hodnota výroku ¬v. To co pro danou úlohu intuitivně víme (sice pokud byl podezřelý v Ostravě, nemohl spáchat trestný čin v Praze) je potřeba přidat jako další formuli o ⇒¬p. Pak už bude mít množina formulí v ⇔ p, o, ¬v, o ⇒¬p jediný model a formule ¬v bude odvoditelná z formulí v ⇔ p, o a o ⇒¬p. # 1 2 3 4 5 6 7 8
v 0 0 0 0 1 1 1 1
p 0 0 1 1 0 0 1 1
o 0 1 0 1 0 1 0 1
v⇔p 1 1 0 0 0 0 1 1
¬v 1 1 1 1 0 0 0 0
¬p 1 1 0 0 1 1 0 0
o ⇒¬ p 1 1 1 0 1 1 1 0
Tab. 5.4 Pravdivostní hodnoty příkladu
Tablo pro splnitelnost původní množiny formulí v ⇔ p, o, ¬v | v ⇒ p, p ⇒ v, o, ¬v /
¬v, p ⇒ v, o, ¬v / ¬v, ¬p, o, ¬v Ο
5
\ ¬v, v, o, ¬v ×
\
p, p ⇒ v, o, ¬v / p,¬p, o, ¬v ×
\ p, v, o, ¬v ×
Tablo pro splnitelnost rozšířené množiny formulí v ⇔ p, o, o ⇒ ¬p , ¬v | v ⇒ p, p ⇒ v, o, o ⇒ ¬p, ¬v /
\
¬v, p ⇒ v, o, o ⇒ ¬p,¬v / ¬v, ¬p, o, o ⇒ ¬p,¬v ¬v, ¬p, o, ¬o, ¬v ×
p, p ⇒ v, o, o ⇒ ¬p,¬v
\ ¬v, v, o, o ⇒ ¬p, ¬v ×
/ p,¬p, o, o ⇒ ¬p,¬v ×
\ p, v, o, o ⇒ ¬p, ¬v ×
¬v, ¬p, o, ¬p, ¬v Ο
Tablo pro důkaz sporem původní množiny formulí v ⇔ p, o, v | v ⇒ p, p ⇒ v, o, v /
\
¬v, p ⇒ v, o, v ×
p, p ⇒ v, o, v / \ p,¬p, o, v p, v, o, v × Ο
Tablo pro důkaz sporem rozšířené množiny formulí v ⇔ p, o, o ⇒ ¬p, v | v ⇒ p, p ⇒ v, o, o ⇒ ¬p, v /
\
¬v, p ⇒ v, o, v ×
p, p ⇒ v, o, o ⇒ ¬p, v / \ p,¬p, o, o ⇒ ¬p, v p, v, o, o ⇒ ¬p, v × / \ p, v, o, p, v, o, ¬o, v ¬p, v × × Rezoluční princip pro důkaz sporem původní množiny formulí v ⇔ p, o, v |
| převod na klauzule ¬v ∨ p, v ∨ ¬p, o, v
p v 6
Rezoluční princip pro důkaz sporem rozšířené množiny formulí v ⇔ p, o, o ⇒ ¬p, v |
|
převod na klauzule ¬v ∨ p, v ∨ ¬p, o, ¬o ∨ ¬p, v p
¬p spor
5.2 Predikátová logika 5.2.1 Pravdivost formulí Podobně jako ve výrokové logice i zde můžeme jednotlivé formule interpretovat, neboli přiřazovat výrazům jazyka objekty z prvků nějaké struktury. Při této tzv. substituci můžeme nahradit proměnnou termem (a nikoliv pouze konstantou). Tedy nejen opice(judy) místo opice(x) ale i Q(f(a)) místo Q(x). Def: Unifikace je taková substituce, kdy navzájem si odpovídající termy v predikátu jsou nahrazeny stejně. Z hlediska pravdivosti můžeme opět dělit formule na tautologie, kontradikce a splnitelné formule. Pro zjišťování splnitelnosti tentokrát již nemůžeme použít tabulku pravdivostních hodnot (konstant, např. názvů zvířat v ZOO může být veliké množství), používá se tedy tablová metoda. K transformačním pravidlům pro konjunkci (α pravidla) a disjunkci (β pravidla) – viz se přidávají γ pravidla pro obecný kvantifikátor a δ pravidla pro existenční kvantifikátor (Tab. 5.5). γ(x)
γ(t)
δ(x)
δ(t)
∀x φ(x)
φ(t)
∃x φ(x)
φ(t)
¬∃x φ(x)
¬φ(t)
¬∀x φ(x)
¬φ(t)
Tab. 5.5 Gama a delta pravidla pro tablo
5.2.2 Odvozování formulí Opět nás budou zajímat logické důsledky množiny formulí a opět se dá použít řada odvozovacích pravidel. Ukažme si jen jedno z nich Rezoluční pravidlo má v predikátové logice podobu ϕ(x) ∨ ψ(t), ¬ϕ(y) ∨ ρ(z) |= ψ(t) ∨ ρ(t) kde x, y, z jsou proměnné a t je term. Použití tohoto pravidla opět předpokládá, že všechny formule jsou v klauzulární formě. Libovolnou formuli můžeme převést na klauzulární tvar následujícím postupem:
7
1. přejmenování proměnných 2. odstranění implikace (převedení ϕ ⇒ ψ na ¬ϕ ∨ ψ) 3. zmenšení oboru platnosti negace (přesunutí negace co nejblíže k atomické formuli, např. podle deMorganova pravidla) 4. vyloučení existenčního kvantifikátoru (tzv. skolemizace) 5. převod na prenexní normální tvar (přenesení všech obecných kvantifikátorů před formuli) 6. převod na konjunktivní normální tvar (konjunkce disjunkcí) 7. odstranění obecných kvantifikátorů Příklad (Lukasová): Každý, kdo má rád zvířata, nenosí kožichy. Každý, kdo jde s módou nosí kožichy. Brigitt Bardotová (BB) má ráda zvířata. Lze odvodit, že BB nejde s módou? Nejprve vyjádříme předcházející tvrzení jako formule predikátového počtu: P1: ∀x (má_rád(x,zvířata) ⇒ ¬nosí(x,kožichy)) P2: (∀x) móda(x) ⇒ nosí(x,kožichy) P3:
má_rád(BB,zvířata)
Závěr: ¬ móda(BB) Pak převedeme všechny formule na klauzule: ¬má_rád(x,zvířata) ∨ ¬nosí(x,kožichy) ¬ móda(x) ∨ nosí(x,kožichy) má_rád(BB,zvířata) ¬ móda(BB)
Odvození pak provedeme (s využitím rezolučního principu) jako důkaz sporem. Budeme tedy zjišťovat splnitelnost formulí ¬má_rád(x,zvířata) ∨ ¬nosí(x,kožichy), ¬móda(x) ∨ nosí(x,kožichy), má_rád(BB,zvířata), móda(BB) |
/
/
/
/
¬má_rád(x,zvířata) ∨ ¬móda(x) \
/
/ \
/
/
/ /
¬móda(BB) \
/ \
/ \
/ \
/
8
spor
Odvození založené na tablové metodě má podobu: P1, P2, P3, móda(BB) | má_rád(BB,zvířata) ⇒ ¬nosí(BB,kožichy), P2, P3, móda(BB) /
\
¬P3, P2, P3, móda(BB)
¬nosí(BB,kožichy), P2, P3, móda(BB) |
×
¬nosí(BB,kožichy), móda(BB) ⇒ nosí(BB,kožichy), P3, móda(BB) /
\
¬nosí(BB,kožichy), ¬móda(BB),
¬nosí(BB,kožichy), nosí(BB,kožichy),
P3, móda(BB)
P3, móda(BB)
×
×
Z obou odvození vyplývá, že za předpokladů P1, P2 a P3 BB skutečně nejde s módou.
5.3 Klauzulární logika Odvozování v klauzulární logice je založeno na modifikovaném rezolučním pravidle. Obecné klauzule mající podobu ¬p1 ∨ ¬p2 ∨ … ∨ ¬pn ∨ q1 ∨ q2 ∨ …∨ qm můžeme vyjádřit jako p1 ∧ p2 ∧ … ∧ ¬pn ⇒ q1 ∨ q2 ∨ …∨ qm Standardní rezoluční pravidlo ϕ ∨ ψ, ¬ϕ ∨ ρ |= ψ ∨ ρ je pak možno přepsat pomocí implikací jako ψ ⇒ ϕ, ϕ ⇒ ρ |= ψ ⇒ ρ
5.4 Deskripční logika V deskripční logice můžeme odvozovat na úrovni konceptů, nebo na úrovni individuí.
5.4.1 Odvozování pro koncepty Odvozování pro koncepty se provádí na základě TBoxů. •
splnitelnost koncept C je splnitelný, pokud CI je neprázdné, kde I je model TBoxu T, tedy T |≠ C ≡ ⊥
9
•
subsumpce (zahrnutí) koncept C je specializací konceptu D (C T D) právě když CI ⊆ DI pro každý model I T |= C D
•
ekvivalence koncepty C a D jsou ekvivalentní (C ≡T D) právě když CI = DI pro každý model I T |= C ≡ D
•
disjunktnost koncepty C a D jsou disjunktní právě když CI ∩ DI = ∅ pro každý model I
Všechna výše uvedená odvozování je možno redukovat na otázku splnitelnosti. Věta: Koncept C je zahrnut v konceptu D právě když C ¬D je nesplnitelné. Věta: Koncepty C a D jsou ekvivalentní právě když jak C ¬D tak ¬C D je nesplnitelné. Věta: Koncepty C a D jsou disjunktní, právě když C D je nesplnitelné. Jak víme z předcházejících oddílů, splnitelnost formulí lze dokazovat různým způsobem. V deskripční logice se používá dříve zmíněný tablový algoritmus. V případě deskripční logiky ALCN se (podobně jako u predikátové logiky) definují pravidla pro konjunkci, disjunkci, obecné omezení a existenční omezení. Navíc se přidávají pravidla pro omezení kardinality (Tab. 5.6). Pravidlo výchozí formule
výsledná formule
→
A={…,x: C D, …}
A ∪ {x:C, x:D}
→
A={…,x: C D, …}
A ∪{x:C}, A ∪{x:D}
→∃
A={…,x:∃R.C, …}
A ∪{y:C, (x, y):R}
→∀
A={..., x:∀R.C, (x, y):R, ...}
A ∪{y:C}
→≥
A={...,x: ≥n R, …}
A ∪{(x, yi):R, i=1..n}
→≤
A={...,x: ≤n R, …} Tab. 5.6 Tablová pravidla pro deskripční logiku
5.4.2 Odvozování pro individua Odvozování pro individua se provádí na základě ABoxů. •
konsistence přiřazení (ABox A) je konsistentní s koncepty (TBox T) pokud existuje interpretace I která je modelem pro A i T. T |= C(a)
10
5.5 Pravidla Hledání aplikovatelného pravidla se v expertních systémech může provádět dvojím způsobem: Zpětné řetězení (backward chaining) je typický způsob práce inferenčního mechanismu v diagnostických expertních systémech. Při odvozování metodou zpětného řetězení vycházíme cílů, které chceme odvodit a pokoušíme se nalézt pravidla umožňující tyto cíle potvrdit nebo vyvrátit. V bázi znalostí existují pravidla, která mají tento cíl ve svém závěru Tato pravidla se tedy pokoušíme aplikovat (za použití dedukce). Abychom zjistili, zda je pravidlo aplikovatelné, musíme vědět, zda platí jeho předpoklad. Pokud je v předpokladu dotaz (např. zvýšená_teplota), lze se na jeho pravdivost zeptat uživatele, Pokud je v předpokladu mezilehlý výrok (např. horní_cesty_ dýchací), musíme ho odvodit (podobně jako cíl) z pravidel, která k němu vedou. Celý proces se tak opakuje (viz Obr. 5.1 ).
Obr. 5.1 Zpětné řetězení
Při přímém řetězení (forward chaining) vycházíme z faktů, které jsou splněny a pokoušíme se nalézt aplikovatelná pravidla. Z aplikovatelných pravidel lze odvodit nějaký závěr, to umožní nalézt další aplikovatelná pravidla a v odvozování lze pokračovat. Podobně jako u zpětného řetězení, i zde lze využívat priority pravidel. Přímé řetězení v čisté podobě znamená, že systém už se uživatele na nic neptá; všechny odpovědi musí být zadány před začátkem konzultace.
Obr. 5.2 Přímé řetězení
11
Způsob použití vybraného pravidla pak vychází z dedukce známé z výrokové logiky - pokud platí předpoklad pravidla, platí i jeho závěr: ϕ ⇒ ψ, ϕ |= ψ
5.6 Rámce Vzhledem k tomu, že rámce obvykle vytvářejí hierarchickou strukturu, základní odvozovací mechanismus je dědění v rámci této hierarchie. V zásadě lze dědit položky i hodnoty položek. Standardní je přitom dědění směrem „shora dolů“, neboli od obecnějšího konceptu (např. auto) ke speciálnějšímu konceptu (osobní auto); dědit lze ale i zdola nahoru. Pokud je možné násobné dědění (pro nějaký rámec je více možností, jak dědit), dědění hodnot může vést k inkonsistencím (Obr. 5.3).
Obr. 5.3 Je nebo není Nixon pacifista?
Rámce můžeme použít i pro reprezentaci typických případů z dané aplikační oblasti. Pak mluvíme o případovém usuzování, které je založeno na podobnosti mezi případy. Pro vyjádření podobnosti resp. vzdálenosti se používá nějaká metrika, neboli funkce d splňující následující vlastnosti: 1. ∀x1,x2 ∈ X; d(x1,x2) ≥ 0 2. d(x1,x2) = 0 ⇔ x1 = x2 3. d(x1,x2) = d(x2,x1) 4. ∀x1,x2,x3 ∈ X; d(x1,x2) + d(x2,x3) ≥ d(x1,x3) V nejjednodušší situaci (jsou-li případy reprezentovány hodnotami numerických veličin) může být funkce d definována jako m
dE(x1,x2) =
∑δE(x1j,x2j) , kde δE(x1j,x2j) = (x1j - x2j)2 j=1
12
neboli jako eukleidovská vzdálenost. Odvozování je pak založeno na nalezení toho případu v bázi případů, který má nejmenší vzdálenost k uvažované rozhodovací situaci. Inferenční cyklus případového usuzování dle [Watson, Marir, 1994] vidíme na Obr. 5.4. V kroku retrieve se k danému problému hledá nejpodobnější případ v bázi případů. V kroku reuse se použije navržené řešení, které je možno případně revidovat v kroku revise. V kroku retain se uchovává nové řešení v bázi případů.
Obr. 5.4 Odvozování v systémech případového usuzování
13
Cvičení: 1) Prověřte splnitelnost formule (φ ⇒ (ψ ∨ ¬ρ)) ∧ (ψ ⇒ φ) 2) Kdykoliv jdou Anna, Bára a Cyril spolu na oběd, objednávají vždy takto: 1. Dá-li si Anna maso, pak má Bára vegetariánské jídlo. 2. Anna nebo Cyril si dají maso, ale ne současně. 3. Bára a Cyril nemají nikdy současně vegetariánský výběr. Přesvědčte se, že Cyril jí vždy maso. (použijte tabulku pravdivostních hodnot, tablo i rezoluční princip) 3) Tři zločinci Jones, Brown a Smith proti sobě vypovídají následujícím způsobem: 1. Brown: „Jones je vinen a Smith je nevinen“ 2. Jones: „Je-li vinen Brown, je vinen i Smith“ 3. Smith: „Já jsem nevinen, ale nejméně jeden ze zbývajících obviněných je vinen“ Zjistěte: •
zda obvinění vypovídají konzistentně
•
kdo je vinen
(použijte tabulku pravdivostních hodnot, tablo i rezoluční princip)
14
Literatura: 1. Baader F., Calvanese D., McGuinness D., Nardi D., Patel-Schneider P.: The Description Logic Handbook.Cambridge University Press 2003. 2. Berka P. a kol.: Expertní systémy. Skripta VŠE, 1998 3. Davis R., Shrobe H., Szolovits P.: What is a Knowledge Representation? AI Magazíne 14(1), 17-33, 1993. 4. Jirků P.: Logika. Neformální výklad základů formální logiky. Skripta VŠE, Praha 1993 5. Kelemen J. a kol.: Pozvanie do znalostnej společnosti. Iura Edition, Bratislava 2007 6. Lukasová A.: Formální logika v umělé inteligenci. Computer Press, Brno 2003 7. Watson,I. – Marir,F.: Case-based reasoning: An review. The Knowledge Engineering Review, Vol. 9:4, 1994, 327-354
15