Logika a logické programování Mgr. Šárka Vavrečková Ústav informatiky Filozoficko-přírodovědecká fakulta Slezské univerzity Opava
[email protected] www.fpf.slu.cz/~vav10ui Poslední aktualizace: 15. prosince 2005
Obsah 1 Základní znalosti 1.1 Základní pojmy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Důkazové metody sémantické analýzy . . . . . . . . . . . . . . . . . . . . .
3 3 4
2 Formální systémy 2.1 Důkazy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Logické systémy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Vlastnosti formálních důkazových metod a systémů . . . . . . . . . . . . .
7 7 8 9
3 Systém přirozené dedukce 3.1 Systém přirozené dedukce výrokové logiky . . . . . . . . 3.2 Formální důkazy . . . . . . . . . . . . . . . . . . . . . . 3.3 Vlastnosti Systému přirozené dedukce výrokové logiky . . 3.4 Systém přirozené dedukce predikátové logiky . . . . . . . 3.5 Vlastnosti Systému přirozené dedukce predikátové logiky
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
12 12 13 20 23 25
4 Hilbertovský axiomatický systém 4.1 Hilbertovský axiomatický systém výrokové logiky . . . . . . . . . . 4.2 Vlastnosti Hilbertovského axiomatického systému výrokové logiky . 4.3 Alternativní konstrukce důkazu . . . . . . . . . . . . . . . . . . . . 4.4 Hilbertovský axiomatický systém predikátové logiky . . . . . . . . . 4.5 Vlastnosti Hilbertovského axiomatického systému predikátové logiky
. . . . .
. . . . .
. . . . .
. . . . .
27 27 32 36 38 39
. . . .
41 41 43 45 45
6 Klauzulární logika 6.1 Hornovy klauzule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2 Syntaxe jazyka klauzulární logiky . . . . . . . . . . . . . . . . . . . . . . . 6.2.1 Jazyk klauzulární logiky . . . . . . . . . . . . . . . . . . . . . . . .
47 47 48 48
5 Gentzenovský formální systém 5.1 Dualizace . . . . . . . . . . . . . . . . . 5.2 Gentzenovský systém výrokové logiky . . 5.3 Korektnost a úplnost systému . . . . . . 5.4 Gentzenovský systém predikátové logiky
1
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . . .
. . . .
. . . . .
. . . .
. . . . .
. . . .
. . . . .
. . . .
. . . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . . . . . . . . . . . .
49 50 52 55 55 56 57 58 59 60 62 62 63 66
7 Klauzulární axiomatický systém 7.1 Definice systému . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2 Formální důkazy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.3 Korektnost systému . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
70 70 72 74
8 Logické programování 8.1 Logické programování v Prologu . . . . 8.1.1 Program a dotazy . . . . . . . . 8.1.2 Základní prvky syntaxe Prologu 8.2 Rezoluce v logickém programování . . . 8.3 Průběh výpočtu v Prologu . . . . . . .
75 75 76 78 81 84
6.3 6.4
6.5
6.2.2 Univerzální tvrzení . . . . . . . . . . . . . . . . 6.2.3 Existenční tvrzení . . . . . . . . . . . . . . . . . Sémantika jazyka klauzulární logiky . . . . . . . . . . . Vlastnosti klauzulí . . . . . . . . . . . . . . . . . . . . 6.4.1 Prázdná množina antecedentu nebo konsekventu 6.4.2 Konjunkce a disjunkce atomů v klauzuli . . . . 6.4.3 Negace atomů . . . . . . . . . . . . . . . . . . . 6.4.4 Negace klauzule . . . . . . . . . . . . . . . . . . 6.4.5 Predikát rovnosti . . . . . . . . . . . . . . . . . 6.4.6 Substituce . . . . . . . . . . . . . . . . . . . . . Vztahy mezi klauzulemi . . . . . . . . . . . . . . . . . 6.5.1 Odvození důsledku dvojice klauzulí . . . . . . . 6.5.2 Unifikace klauzulí . . . . . . . . . . . . . . . . . 6.5.3 Znalostní báze . . . . . . . . . . . . . . . . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . . . . . . . . . . .
. . . . .
. . . . .
A Příklady
91
B Řešení příkladů
97
Rejstřík
113
2
Kapitola 1 Základní znalosti Tato kapitola pouze uspořádává a připomíná znalosti získané v předchozím kurzu – Úvod do logiky. Jejím účelem je především definovat základní pojmy a metody, které budou používány v následujících kapitolách.
1.1
Základní pojmy
V následujícím textu budeme používat tyto základní pojmy (zde jsou definovány pro výrokovou logiku, pro predikátovou by byla zahrnuta interpretace): • Model formule F je takové ohodnocení (valuace) v, ve kterém má formule hodnotu true (když za výrokové proměnné dosadíme hodnoty true a false podle předpisu valuace v a vyhodnotíme, dostaneme true). • Formule F je splnitelná, jestliže má alespoň jeden model (také říkáme, že je pravdivá v tomto modelu). • Formule F je tautologie (logicky platná, splněna, logický zákon), jestliže je splnitelná pro všechny valuace, tedy všechny valuace jsou modely formule F . • Formule F je kontradikce (nesplnitelná), když nemá žádný model. • Množina formulí M je splnitelná, jestliže všechny formule této množiny mají alespoň jeden společný model, tedy když existuje alespoň jedna valuace, která je modelem pro všechny formule množiny. Takovou valuaci nazýváme model množiny formulí M. • Formule F logicky vyplývá z množiny formulí M (tedy je jejich logickým důsledkem), jestliže je pravdivá v každém modelu množiny M (tj. každý model množiny M je zároveň modelem formule F ). Značíme M |= F .
3
1.2
Důkazové metody sémantické analýzy
V předchozím semestru jsme se seznámili se základními metodami sémantické analýzy1 pro provádění důkazů. Probírali jsme 1. sémantické metody (pracujeme přímo s pravdivostními hodnotami jednotlivých částí formule): • sémantická tabulka • sémantický strom (Quinův algoritmus) 2. syntaktické metody (při analýze nepracujeme s pravdivostními hodnotami částí formule, ale používáme pouze syntaktickou skladbu formule – tvar podformulí, umístění jednotlivých logických spojek, kvantifikátory, . . . ): • sémantické tablo (slovo „sémantickéÿ v názvu znamená pouze ten fakt, že účelem metody je zjistit sémantickou hodnotu formule) • rezoluce (přímá a nepřímá) Dále se soustředíme především na syntaktické metody a možnosti jejich použití při dokazování. Princip důkazu vychází z deduktivního úsudku: Deduktivní úsudek zapisujeme schématem P1 , P2 , . . . , Pn |= Z, kde • P1 , P2 , . . . , Pn , Z jsou tvrzení, • P1 , P2 , . . . , Pn nazýváme předpoklady (premisy), • Z je závěr. Aby se jednalo o platný deduktivní úsudek, musí platit: • Z platnosti předpokladů usuzujeme na platnost závěru (tj. to, zda je závěr platný, vyplývá z toho, zda jsou či nejsou platné předpoklady). • Ve všech případech, kdy jsou platné zároveň všechny předpoklady, musí být platný i závěr (tedy nesmí nastat situace, ve které by všechny předpoklady byly pravdivé a závěr nepravdivý). „Ve všech případechÿ může znamenat například ve výrokové logice „při všech možných ohodnoceních výrokových symbolůÿ. 1
Sémantická analýza má za úkol určit, zda je analyzovaná formule tautologie, kontradikce či splnitelná, stanovujeme tedy pravdivostní (sémantickou) hodnotu formule.
4
Větu nesmí nastat situace, ve které by všechny předpoklady byly pravdivé a závěr nepravdivý můžeme symbolicky přepsat jako ¬ (P1 &P2 & . . . &Pn &¬Z) ¬ ((P1 &P2 & . . . &Pn ) &¬Z) (P1 &P2 & . . . &Pn ) → Z
(1.1) (1.2) (1.3)
Zapisujeme P1 , P2 , . . . , Pn |= Z. Odvozovací pravidlo je metoda, kterou lze použít pro odvození jednoho tvrzení z jiných. Musí splňovat vlastnosti deduktivního úsudku, tedy zachovávat platnost (závěr odvozený z platných předpokladů musí být také platný). Existuje mnoho odvozovacích pravidel, v následujícím textu se s některými seznámíme. Definice 1.1: Důkaz tvrzení T z předpokladů P1 , P2 , . . . , Pn je posloupnost tvrzení B1 , B2 , . . . , Bm , kde Bm = T a každý její člen Bi , 1 ≤ i ≤ m je: • jeden z předpokladů Pj nebo • vznikl uplatněním některého odvozovacího pravidla na předchozí členy posloupnosti. Pro připomenutí si na příkladech ukážeme použití metod sémantického tabla a rezoluce pro výrokovou logiku. Příklad 1.1: Ověřte sémantickým tablem, zda platí p ∨ q → r |= q → r Ověřujeme platnost formule (p ∨ q → r) → (q → r). Vytvoříme sémantické tablo pro negaci této formule a pokud se uzavře, znamená to, že negace formule je kontradikce, tedy původní formule je tautologie. Protože jde o formuli výrokové logiky, budeme používat pouze α a β pravidla. ¬ ((p ∨ q → r) → (q →)) α p ∨ q → r, ¬(q → r) α p ∨ q → r, q, ¬r ¬(q ∨ q), q, ¬r α ¬p, ¬q, q, ¬r
HH
β
HH
r, q, ¬r
× (přes r)
× (přes q) Obrázek 1.1: Příklad sémantického tabla pro výrokovou logiku Sémantické tablo se uzavřelo, proto negovaná formule je kontradikce a původní formule tautologie, tedy ověřovaný vztah platí. 5
Příklad 1.2: Ověřte nepřímou rezolucí platnost vztahu {p ∨ q, p → r, q → s} |= r ∨ s. Chceme použít nepřímou rezoluci, tedy dokazujeme, že následující formule je kontradikce: (p ∨ q)&(p → r)&(q → s)&¬(r ∨ s). Rezoluční odvozovací pravidlo pro výrokovou logiku je A ∨ B, ¬B ∨ C |= A ∨ C
(1.4)
Abychom mohli toto pravidlo používat, musíme mít formuli v konjunktivní normální formě – podformule obsahující pouze literály a disjunkce), mezi jednotlivými podformulemi je vztah konjunkce. Jednotlivé podformule rozepíšeme a postupně uplatňujeme rezoluční odvozovací pravidlo. 1. 2. 3. 4. 5. 6. 7. 8. 9.
p∨q ¬p ∨ r ¬q ∨ s ¬r ¬s ¬p q s 2
první konjunkt negace závěru druhý konjunkt negace závěru R(2,4) R(1,6) R(3,7) R(5,8)
Protože jsme došli k prázdné formuli (2, false), původní vztah je platný.
6
Kapitola 2 Formální systémy V této kapitole se budeme zabývat systémy, které pro dedukci využívají výhradně syntaktické důkazové metody. Výhodou těchto systémů je především to, že syntaktické metody se snadno programují, a proto je lze využít pro logické programování.
2.1
Důkazy
Jaké důkazy obvykle provádíme? 1. Zajímá nás, zda daná formule je tautologií. 2. Chceme vědět, jestli daný závěr vyplývá ze zadaných předpokladů. 3. Zjišťujeme, co by mohlo vyplývat ze zadaných předpokladů (nemáme konkrétní představu o tom, co dokazujeme, generujeme formule vyplývající z předpokladů). Je zřejmé, že první dva případy jsou vzájemně převeditelné (viz vztahy 1.1–1.3 na str. 5). Důkazy dělíme na: • Přímé – z množiny předpokladů odvozujeme závěr podle daných odvozovacích pravidel. • Nepřímé – formuli popřeme a dokážeme, že tato negace je kontradikce, tedy dojdeme ke sporu, jde o důkaz sporem. Dosud jsme se zabývali pouze nepřímými důkazy. Pomocí sémantického tabla i nepřímé rezoluce jsme dokazovali, že negace formule je kontradikce, a proto původní formule je tautologie.
7
2.2
Logické systémy
Ve výrokové a predikátové logice existují pro ověřování platnosti formulí sémantické i syntaktické postupy (zmíněné v kapitole 1.2), pokud však chceme využít logiku pro budování teorií, nebude nám to stačit. Proto vytváříme systémy s předem nadefinovanými stavebními kameny – axiomy, a metodami – odvozovacími pravidly. V rámci takto nadefinovaného systému pak pomocí odvozovacích pravidel odvozujeme další tvrzení, která nazýváme větami nebo teorémy. Odvozovací pravidla ve formálních systémech bývají syntaktická, při jejich používání se tedy nezabýváme přímo ohodnocením jednotlivých prvků jazyka, ale pracujeme se syntaktickou strukturou formulí. Tato pravidla obvykle vycházejí ze syntaktických metod sémantické analýzy nebo jsou odvozena z vlastností operátorů zvoleného jazyka (konjunkce, implikace, . . . ). Znak |= značí logické vyplývání, u formálních systémů budeme pro tytéž účely používat znak ` – symbol pro dokazatelnost. '
Syntaktické Sémantika, $ ' $ ' prvky význam Jazyk některé - Formální systém Teorie logiky (logický kalkul)
&
výroková, predikátová, ...
% &
% &
Hilbertovský, Gentzenovský, přirozené dedukce, ...
$ %
teorie uspořádání, teorie grup, růz. fyzikální teorie, ...
Obrázek 2.1: Postup vytváření logických systémů Syntaktické prvky jsou buď formule (nazýváme je obvykle logické axiomy) nebo odvozovací pravidla (ta určují, jak odvozovat další formule). Logické axiomy musí být vždy tautologie nad zvoleným jazykem formálního systému (např. nad výrokovou logikou), Odvozovací pravidla musí zachovávat pravdivost. U sémantických prvků již tento požadavek není. Přidáváme obvykle formule (nazývané obvykle speciální axiomy), které již nemusí být tautologiemi, stačí, když jsou platné pro požadovanou interpretaci (tj. za určitých okolností). Když začneme brát v úvahu interpretaci, systém přestává být univerzálně použitelný, ale přesto je užitečný, protože existují taková tvrzení, která platí v jedné teorii, ale v jiné nikoliv. Například v teorii grup platí tvrzení o neutrálním prvku (symbolem ◦ označme operaci grupy): ∃n∀x(x ◦ n = x & n ◦ x = x)
(2.1)
Toto tvrzení však neplatí v jiných teoriích včetně některých algebraických (existují algebraické struktury, které nemají neutrální prvek). Speciální axiomy jsou tvrzení, která 8
považujeme za platná v rámci této teorie (tj. v zamýšlené interpretaci), ale nemusí být platná v každé interpretaci (viz tvrzení 2.1 na str. 8). Formální systémy dělíme na axiomatické a předpokladové. Axiomatický systém je určen • jazykem (obvykle výroková nebo predikátová logika, příp. s omezením spojek), • logickými axiomy, • odvozovacími pravidly. Důkaz začíná axiomy (případně dokázanými větami), vytváříme přímé důkazy. Předpokladový formální systém je určen • jazykem, • dedukčními pravidly. Dedukční pravidla (jsou obdobou odvozovacích pravidel, musí splňovat jejich vlastnosti) bez předpokladů nazýváme axiomy. V důkazu můžeme používat různé druhy předpokladů, tedy přípustný je i nepřímý důkaz (důkaz sporem). Teorii vytvoříme tak, že k vybranému formálnímu systému přidáme speciální axiomy, tedy odvozovací (deduktivní) pravidla můžeme používat na logické axiomy, již odvozené věty a speciální axiomy.
2.3
Vlastnosti formálních důkazových metod a systémů
U metod sémantické analýzy (tablo, rezoluce) vyžadujeme tyto vlastnosti: • sémantická korektnost, • sémantická úplnost. U formálních systémů jsou obvykle důležité tyto vlastnosti: • sémantická korektnost, • sémantická úplnost, • bezespornost. Užitečnou vlastností může být také minimálnost. U formálních systémů se vyžaduje především korektnost a bezespornost. 9
Definice 2.1: Důkazová metoda je sémanticky korektní, je-li každá pomocí ní dokazatelná formule logicky platná (tedy pokud lze formuli dokázat pomocí této metody, musí být logicky platná). Definice 2.2: Důkazová metoda je sémanticky úplná, lze-li pomocí ní dokázat všechny logicky platné formule. Jaký je vztah mezi korektností a úplností? Označme M metodu, jejíž korektnost a úplnost zkoumáme, FM množinu všech formulí dokazatelných metodou M a P množinu všech logicky platných formulí. Pak platí: Korektnost: FM ⊆ P Úplnost: FM ⊇ P Pro metodu, která je zároveň korektní a úplná, platí FM ∼ = P, což znamená, že metodou lze dokázat právě ty formule, které jsou logicky platné, což je většinou u dokazovací metody nezbytné. Pomocí implikací můžeme tyto vlastnosti znázornit následovně: Korektnost: FM −→ P Úplnost: FM ←− P Pro metodu, která, je korektní a úplná, platí ekvivalence FM ←→ P. Příklad 2.1: Důkaz korektnosti a úplnosti metody si ukážeme na sémantickém tablu pro výrokovou logiku. 1. Korektnost Předpokládejme, že formule F je dokazatelná sémantickým tablem. =⇒ Sémantické tablo formule ¬F má všechny větve uzavřené. Dále použijeme důkaz matematickou indukcí podle hloubky h podstromu sémantického tabla: Báze indukce: h = 0 (list stromu) – protože je každá větev uzavřená, v každém listu stromu se nachází komplementární pár literálů, označme je například p, ¬p. Mezi nimi je vztah konjunkce a platí p &¬p = f alse =⇒ formule v každém listu je kontradikce (nesplnitelná)1 . Předpoklad indukce: Předpokládejme, že věta platí pro h = k, k ≥ 0. Krok indukce: mějme podstrom hloubky h = k + 1. Jeho kořen má jeden (α-pravidlo) nebo dva (β-pravidlo) následníky. α: kořen postromu je ohodnocen množinou formulí U ∪ {A1 &A2 }, jeho následník množinou formulí U ∪ {A1 , A2 }. Pro následníka platí indukční předpoklad (hloubka jeho 1 Přesněji jde o množinu formulí, která je pro dané ohodnocení splnitelná právě tehdy a jen tehdy, když jsou pro toto ohodnocení splnitelné všechny formule v množině, a množina {p, ¬p, . . .} není splnitelná pro žádné ohodnocení.
10
postromu je k), tedy U ∪ {A1 , A2 } je nesplnitelná, což znamená, že buď U nebo A1 nebo A2 je nesplnitelná. Proto při přesunu o uzel výše je buď U nebo A1 &A2 nesplnitelná, tedy množina formulí U ∪ {A1 &A2 } je nesplnitelná. β: kořen podstromu je ohodnocen množinou formulí U ∪ {A1 ∨ A2 }, jeden následník množinou formulí U ∪ {A1 } a druhý U ∪ {A2 }. Oba následníci mají hloubku podstromu menší nebo rovnu k, tedy pro ně platí indukční předpoklad a jsou ohodnoceny nesplnitelnými množinami formulí. Z toho vyplývá, že buď je nesplnitelná množina U a nebo jsou nesplnitelné obě formule A1 , A2 . Proto je nesplnitelná i množina formulí U ∪ {A1 ∨ A2 } v uzlu s podstromem hloubky k + 1. Pokud indukci uplatníme na celý strom sémantického tabla, zjistíme, že formule ¬F v kořeni tohoto stromu je nesplnitelná, z toho vyplývá, že formule F je tautologie. 2. Úplnost Pro důkaz korektnosti jsme použili techniku důkazu matematické indukce, zde použijeme důkaz sporem: abychom dokázali implikaci logicky platná −→ dokazatelná, stačí dokázat ekvivalentní implikaci ¬dokazatelná −→ ¬logicky platná. Předpokládejme tedy, že formule F není dokazatelná sémantickým tablem. To znamená, že sémantické tablo formule ¬F se neuzavře, v některém listu stromu tabla (nejméně jednom) je splnitelná množina formulí (stačí splnitelná pro nějakou valuaci, nemusí být logicky platná). Když budeme postupovat obdobně jako u předchozí části důkazu po stromě od listů ke kořenům, pak alespoň v jedné větvi (z onoho „splnitelného listuÿ ke kořeni stromu) budou všechny uzly ohodnoceny splnitelnými množinami formulí (to plyne z definice konjunkce a disjunkce), a tedy i kořen celého stromu je ohodnocen splnitelnou formulí, nikoliv kontradikcí (je to ¬F ), proto formule F nemůže být logicky platná, není to tautologie. Definice sémantické korektnosti a úplnosti pro formální systémy jsou obdobné definicím pro metody, proto je zde nebudeme uvádět. Definice 2.3: Formální systém je sporný, jestliže je v něm dokazatelná jakákoliv formule. Formální systém je bezesporný, když není sporný. Věta 2.1: Je-li U sporná množina formulí, pak U ` F i U ` ¬F . Ve sporném systému existuje formule F taková, že v tomto systému je dokazatelná jak formule F , tak i její negace. Důkaz:
je zřejmý, vyplývá z předchozí věty.
2
Definice 2.4: Nechť M je množina obsahující logické axiomy formálního systému a formule vzniklé uplatněním dedukce na odvozovací (dedukční) pravidla formálního systému. Formální systém je minimální, pokud jsou je množina M minimální, tedy, její prvky jsou navzájem nezávislé.
11
Kapitola 3 Systém přirozené dedukce V této kapitole se budeme zabývat Systémem přirozené dedukce, který je zástupcem předpokladových formálních systémů. Jako jazyk použijeme nejdřív výrokovou logiku a potom predikátovou logiku prvního řádu. Systém definujeme pro výrokovou logiku, dále probereme typy důkazů, které zde lze provádět a dokážeme korektnost a úplnost tohoto systému, a pak provedeme totéž pro predikátovou logiku. Systém přirozené dedukce predikátové logiky je vlastně rozšířením Systému přirozené dedukce výrokové logiky, proto ty části, důkazy a věty, které jsou stejné, nebudeme uvádět.
3.1
Systém přirozené dedukce výrokové logiky
Jazyk Systému přirozené dedukce výrokové logiky přejímáme z výrokové logiky. Dedukční pravidla jsou uvedena v tabulce 3.1. 1. 2. 3. 4. 5. 6. 7. 8. 9. 10.
` A ∨ ¬A A ` A→A A A, B ` A &B ZK A &B ` A nebo A &B ` B EK A ` A ∨ B nebo B ` A ∨ B ZD A ∨ B, ¬A ` B nebo A ∨ B, ¬B ` A ED B ` A→B ZI A → B, A ` B EI A → B, B → A ` A ↔ B ZE A ↔ B ` A → B nebo EE A↔B ` B→A
axiom axiom zavedení konjunkce eliminace konjunkce zavedení disjunkce eliminace disjunkce zavedení implikace eliminace implikace zavedení ekvivalence eliminace ekvivalence
Tabulka 3.1: Dedukční pravidla Systému přirozené dedukce výrokové logiky Pravidlo eliminace implikace (EI) je také nazýváno Modus Ponens a značí se MP. 12
Věta 3.1: (Věta o substituci) Nechť F je formule výrokové logiky, která obsahuje právě výrokové proměnné p1 , p2 , . . . , pn (a žádné další). Nechť dále A1 , A2 , . . . , An jsou jakékoliv formule výrokové logiky. Formuli F 0 vytvoříme tak, že pro každé i ∈ {1, . . . , n} nahradíme všechny výskyty výrokové proměnné pi ve formuli F formulí Ai . Pak jestliže F je tautologie, pak také F 0 je tautologie. Důkaz: Každá výroková proměnná pi může nabývat hodnot z množiny {0, 1}, každá formule Ai taktéž. Jestliže je F tautologie, pak je splnitelná pro jakékoliv ohodnocení, tedy ať za pi dosadíme cokoliv, vždy po vyhodnocení formule F dostaneme hodnotu 1 (true). Po dosazení Ai za pi můžeme totéž tvrdit o F 0 – ať je výsledkem vyhodnocení formulí Ai cokoliv, formule F 0 je vždy vyhodnocena s výsledkem 1 (true). 2 Věta 3.2: (Rozšířená věta o substituci) Nechť F je formule výrokové logiky, která obsahuje podformuli A. Dále nechť B je formule výrokové logiky ekvivalentní s formulí A. Formuli F 0 vytvoříme tak, že v F nahradíme podformuli A formulí B. Jestliže F je tautologie, pak i F 0 je tautologie. Důkaz: Formule A a B jsou ekvivalentní, tedy při vyhodnocení s použitím stejné valuace dávají stejné výsledky, proto jestliže F je tautologie, pak po záměně B za A je také formule F 0 tautologie. 2
3.2
Formální důkazy
Definice 3.1: Přímý důkaz formule F z předpokladů P1 , P2 , . . . , Pn je posloupnost formulí A1 , A2 , . . . , Am , kde F = Am a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • Ai ∈ {P1 , . . . , Pn } (tj. je to některý z předpokladů), • Ai je axiom, • Ai vznikla použitím některého dedukčního pravidla na předchozí členy posloupnosti. Přímý důkaz formule F (tj. bez předpokladů) je definován stejně, jen n = 0. Věta 3.3: (Věta o dedukci) P1 , P2 , . . . , Pn−1 , Pn ` Z Poznámka:
⇔
` P1 , P2 , . . . , Pn−1 ` Pn → Z
(3.1)
Pokud větu o dedukci použijeme rekurzívně n-krát, dostaneme ekvivalenci P1 , P2 , . . . , Pn−1 , Pn ` Z
⇔ 13
P1 → (P2 → . . . (Pn → Z) . . .)
(3.2)
Důkaz:
provedeme pro n=2, lze zobecnit pro jakékoliv n.
1) „⇐ÿ: Nechť platí ` P1 → (P2 → Z), dokážeme P1 , P2 ` Z. 1. 2. 3. 4. 5.
P1 → (P2 → Z) P1 P2 P2 → Z Z
Jako předpoklady důkazu použijeme celou první formuli a dále předpoklady druhé formule, závěrem, ke kterému chceme dospět, je Z. V důkazu použijeme pouze pravidlo eliminace implikace, a to dvakrát.
Předpoklad 1 Předpoklad 2 Předpoklad 3 EI(1,2) EI(3,4)
2) „⇒ÿ: Nechť platí P1 , P2 ` Z, dokážeme ` P1 → (P2 → Z). 1. 2. 3. 4. 5.
Pravidlo zavedení implikace vyžaduje pouze přítomnost druhého argumentu mezi předchozími členy posloupnosti. Toto pravidlo použijeme celkem dvakrát, Z jsme získali uplnatněním věty P1 , P2 ` Z.
P1 Předpoklad 1 P2 Předpoklad 2 Z Použití věty v předpokladu P2 → Z ZI(3) P1 → (P2 → Z) ZI(4)
Tento důkaz se týká vztahu 3.2, důkaz vztahu 3.1 by byl obdobný, jen trochu kratší.
2
Příklad 3.1: Dokažte platnost vztahu A → B, B → C, A ` C 1. 2. 3. 4. 5.
Př1 Př2 Př3 EI(1,3) EI(2,4)
A→B B→C A B C
Podle věty o dedukci jsme dokázali také například vztahy A → B, B → C A→B B→C
` ` ` ` `
A→C (B → C) → (A → C) (A → B) → (A → C) (A → B) → ((B → C) → (A → C)) (B → C) → ((A → B) → (A → C))
(3.3) (3.4) (3.5) (3.6) (3.7)
Vztah 3.4 se nazývá věta o tranzitivitě implikace. Často se používá v důkazech jako pomocné pravidlo, jeho použití značíme zkratkou TI. Poznámka: Věta o dedukci se často používá k úpravě formule, kterou chceme dokázat – formuli pomocí této věty rozdělíme na předpoklady a závěr, který pak dokazujeme z předpokladů. 14
Dále větu o dedukci použijeme, pokud chceme již dokázanou formuli použít jako pomocné pravidlo nebo dokázané pravidlo jako logicky platnou formuli, kterou lze také zařadit do důkazu. Příklad 3.2: Dokažte platnost vztahu A, ¬A ` B. 1. 2. 3. 4.
A ¬A A∨B B
Ze sporné množiny vyplývá cokoliv, toto pomocné pravidlo nazýváme pravidlo sporné množiny a značíme SM.
Př1 Př2 ZD(1) ED(2,3)
Definice 3.2: Nepřímý důkaz (sporem) formule F z předpokladů P1 , P2 , . . . , Pn je posloupnost formulí A1 , A2 , . . . , Am , kde • pro každé i ∈ {1, . . . , n} je Ai = Pi (tj. nejdřív do důkazu zařadíme předpoklady), • An+1 = ¬F , • pro každé i > (n + 1) pro Ai platí některá z těchto možností: – Ai ∈ {P1 , . . . , Pn } (tj. je to některý z předpokladů), – Ai je axiom, – Ai vznikla použitím některého dedukčního pravidla na předchozí členy posloupnosti, • Am = ¬Aj pro některé j < m (spor). Nepřímý důkaz formule F (tj. bez předpokladů) je definován stejně, jen n = 0 a prvním členem posloupnosti je negace formule F . Příklad 3.3: Dokažte větu ¬(A ∨ B) → (¬A &¬B). Použijeme větu o dedukci, tedy předpokladem pro nás bude část formule před implikací. Důkaz rozdělíme do tří částí. Nejdřív z předpokladu dokážeme závěr ¬A, potom ¬B, a v třetí části vše spojíme pravidlem zavedení konjunkce. 1. ¬(A ∨ B) 2. A 3. A ∨ B ⇒ ¬A
Př1 NZ (negace závěru) ZD(2), spor s 1.
1. ¬A 2. ¬B 3. ¬A &¬B
Př1 Př2 ZK(1,2)
1. ¬(A ∨ B) 2. B 3. A ∨ B ⇒ ¬B
15
Př1 NZ (negace závěru) ZD(2), spor s 1.
Příklad 3.4: Dokažte platnost vztahu (¬A → ¬B) ` (B → A) 1. 2. 3. 4.
¬A → ¬B B ¬A ¬B
Př1 Př2 NZ EI(1,3), spor s 2.
Toto pomocné pravidlo budeme nazývat pravidlo kontrapozice, značíme K.
Příklad 3.5: Dokažte platnost vztahů ¬¬A ` A 1. 2. 3. 4. 5. 6.
¬¬A Př1 1 ¬¬A → (¬A → ¬¬¬A) VD na SM ¬A → ¬¬¬A EI(1,2) (¬A → ¬¬¬A) → (¬¬A → A) VD na K ¬¬A → A EI(3,4) A EI(1,5)
1. A 2. ¬(¬¬A) 3. ¬A
Př1 NZ EN(2), spor s 1
a
A ` ¬¬A.
Toto pomocné pravidlo nazýváme pravidlo eliminace negace, značíme EN. Dále již budeme předpokládat jeho platnost a nemusíme uvádět v posloupnosti důkazu.
Toto je pomocné pravidlo zavedení negace, značíme ZN. Taktéž ho nemusíme uvádět v posloupnosti důkazu.
Příklad 3.6: Dokažte platnost vztahu A → B ` ¬B → ¬A. 1. A → B 2. ¬¬A → ¬¬B) 3. ¬B → ¬A
Př1 ZN(1) K(2)
Toto je pomocné pravidlo transpozice, značíme T.
Příklad 3.7: Dokažte platnost vztahu A &B ` ¬(¬A ∨ ¬B) 1. 2. 3. 4. 5.
A &B ¬A ∨ ¬B A B ¬B
Př1 NZ EK(1) EK(1) ED(2,3), spor s 4
Toto pomocné pravidlo nazýváme pravidlo převodu konjunkce na disjunkci, značíme KD.
V systému přirozené dedukce můžeme s výhodou používat také hypotetické předpoklady – hypotézy. Důležité je si uvědomit, že platnost důsledku, ke kterému pomocí hypotézy dojdeme, je podmíněna platností této hypotézy. 1
VD je zkratka pro „Věta o dedukciÿ.
16
Přímá hypotéza: Mimo hlavní posloupnost důkazu může být uvedena hypotéza H. Jestliže na základě této hypotézy a předchozích členů posloupnosti důkazu lze odvodit formuli A, pak formuli H → A můžeme připojit k hlavní posloupnosti důkazu (tj. k řádnému důkazu) jako větu. Příklad 3.8: Dokažte platnost věty (p &q → r) &q → ((p → r) ∨ (q → r)) 1. (p &q → r) &q 2. p &q → r 3. q (a) p (b) p &q (c) r 4. p → r 5. (p → r) ∨ (q → r)
Př1 EK(1) EK(1) H1 ZK(3,a) EI(2,b) (a → c) ZD(4)
Nepřímá hypotéza: Mimo hlavní posloupnost důkazu může být uvedena hypotéza H. Jestliže na základě této hypotézy a předchozích členů posloupnosti důkazu lze odvodit formuli A, která je ve sporu s některým členem posloupnosti řádného důkazu, pak k hlavní posloupnosti důkazu můžeme jako větu připojit formuli ¬H. Příklad 3.9: Dokažte platnost věty ¬(p ∨ q) → (¬p &¬q) 1. ¬(p ∨ q) (a) p (b) p ∨ q 2. ¬p (a) q (b) p ∨ q 3. ¬q 4. ¬p &¬q
Př1 H1 ZD(a), spor s 1 ¬ H1 H2 ZD(a), spor s 1 ¬ H2 ZK(2,3)
Přímý větvený důkaz s hypotézami: Jestliže se v posloupnosti důkazu nachází formule ve tvaru B1 ∨ B2 ∨ . . . ∨ Bm a formuli A lze dokázat ze všech hypotéz – podformulí Bi , i ∈ {1 . . . m}, pak k hlavní posloupnosti důkazu můžeme připojit formuli A. Toto je zkrácení postupu použití přímé hypotézy, kdy bychom dostali v hlavní posloupnosti důkazu věty Bi → A („formuli A lze dokázat ze všech hypotéz – podformulí Bi ÿ). Větu lze 17
zformulovat takto: Věta 3.4: Z platnosti formule B1 ∨B2 ∨. . .∨Bm a formulí B1 → A, B2 → A, . . . , Bm → A plyne platnost formule A. Důkaz: Větu dokážeme pro m = 2, a to nepřímým důkazem (předpoklady B1 → A a B2 → A byly získány uplatněním přímé hypotézy). 1. 2. 3. 4. 5. 6. 7. 8. 9.
B1 ∨ B2 B1 → A B2 → A ¬A → ¬B1 ¬A → ¬B2 ¬A ¬B1 ¬B2 B2
Př1 Př2 Př3 T(2) T(3) NZ (negace závěru) EI(4,6) EI(5,6) ED(1,7), spor s 8
Protože negace závěru ¬A byla popřena, dokázali jsme platnost závěru A. 2
Příklad 3.10: Dokažte platnost věty ((p &q) ∨ (p &r)) → (p & (q ∨ r)) 1. (p &q) ∨ (p &r)
Př1
(a) (b) (c) (d) (e)
p &q p q q∨r p & (q ∨ r)
H1 EK(a) EK(a) ZD(c) ZK(b,d)
(a) (b) (c) (d) (e)
p &r p r q∨r p & (q ∨ r)
H2 EK(a) EK(a) ZD(c) ZK(b,d)
Použijeme jako H1 ∨ H2.
2. p & (q ∨ r) Poznámka: Větvený důkaz z hypotéz můžeme uplatnit na jakoukoliv disjunkci podformulí, která je prvkem posloupnosti důkazu. Často se také používá axiom ` A ∨ ¬A, který můžeme přidat na kterékoliv místo v důkazu (viz definice důkazu) a použít pro tento účel. Nepřímý větvený důkaz s hypotézami: Jestliže se v posloupnosti nepřímého důkazu nachází formule ve tvaru B1 ∨B2 ∨. . .∨Bm a ze všech hypotéz – podformulí Bi , i ∈ {1 . . . m} 18
docházíme ke sporu s některým členem hlavní posloupnosti důkazu (tedy všechny Bi jsou vyvráceny), pak jsme dospěli ke sporu i v hlavní posloupnosti důkazu a původní formule je dokázána. Poznámka: Formule B1 ∨ B2 ∨ . . . ∨ Bm často bývá negací závěru. V tomto typu důkazu vlastně popřením všech větví důkazu přidáváme k hlavní posloupnosti důkazu formuli, která je ve sporu s některým předchozím členem posloupnosti. Příklad 3.11: Dokažte platnost věty ((p → q) & (r → s) &¬ (q ∨ s)) → ¬ (p ∨ r) 1. 2. 3. 4. 5.
(p → q) & (r → s) &¬ (q ∨ s) Př1 p→q EK(1) r→s EK(1) ¬ (q ∨ s) EK(1) p∨r NZ = H1 ∨ H2 (a) p (b) q (c) q ∨ s
H1 EI(2,a) ZD(b), spor s 4
(a) r (b) s (c) q ∨ s
H2 EI(3,a) ZD(b), spor s 4
⇒ spor s 4 Příklad 3.12: Dokažte, že platí A ∨ B, ¬B ∨ C 1. A ∨ B 2. ¬B ∨ C 3. B ∨ ¬B
Př1 Př2 Axiom
(a) B (b) C (c) A ∨ C
H1 ED(2,a) ZD(b)
(a) ¬B (b) A (c) A ∨ C
H2 ED(1,a) ZD(b)
4. A ∨ C
19
` A∨C
(pravidlo rezoluce)
3.3
Vlastnosti Systému přirozené dedukce výrokové logiky
Věta 3.5: (Věta o korektnosti Systému přirozené dedukce výrokové logiky) Každá formule dokazatelná v Systému přirozené dedukce výrokové logiky je logicky platná, tedy pro každou formuli A výrokové logiky platí: ` A
=⇒
(3.8)
|= A
Důkaz: Dokazujeme, že důkaz provedený v tomto systému je korektní, tedy že všechna dedukční pravidla zachovávají pravdivost (pro ohodnocení, při kterém jsou splnitelné předpoklady, je splnitelný i závěr), a dále že samotná konstrukce důkazu (řazení posloupnosti důkazu) je korektní. Korektnost dedukčních pravidel lze dokázat sémantickými tabulkami (zde například pro jeden axiom a dedukční pravidla ZK a EI): A 0 1
` A ∨ ¬A ¬A A ∨ ¬A 1 1 0 1
A, B ` A &B A B A &B 0 0 0 0 1 0 1 0 0 1 1 1
A 0 0 1 1
A → B, A ` B A→B 0 1 1 1 0 0 1 1
B A 0 0 1 1
B 0 1 0 1
Tabulka 3.2: Sémantické tabulky pro některá dedukční pravidla V případě pravidel bez předpokladů (axiomů) musí být v posledním sloupci pouze hodnoty 1, u dedukčních pravidel s předpoklady musí být v posledním sloupci (závěru pravidla) hodnoty 1 v těch řádcích, kde jsou hodnoty 1 ve všech sloupcích označených předpoklady pravidla (říkáme, že pravidlo zachovává splnitelnost – závěr je splnitelný v každém ohodnocení, ve kterém jsou splnitelné předpoklady). Pokud takto vyjdou tabulky pro všechna dedukční pravidla, pak je dokázána korektnost dedukčních pravidel systému. Korektnost přímého důkazu vyplývá z jeho definice. Protože se jedná o konečnou posloupnost formulí, použijeme důkaz matematickou indukcí. Jestliže jde o důkaz z předpokladů (máme alespoň jeden předpoklad), pak dokazujeme, že splnitelnost závěru je podmíněna splnitelností předpokladů, tedy v každém ohodnocení, ve kterém jsou předpoklady splnitelné, musí být splnitelný i závěr. Báze indukce: Z definice vyplývá, že první člen posloupnosti je axiom nebo předpoklad. Platnost axiomů jsme dokázali výše, splnitelností předpokladů je podmíněna splnitelnost závěru pro dané ohodnocení, proto nás dále zajímají pouze ta ohodnocení, ve kterých jsou všechny předpoklady splnitelné. Předpoklad indukce: předpokládejme, že je věta dokázána až ke k-tému členu posloupnosti důkazu, tedy až k této formuli včetně jsou členy posloupnosti buď předpoklady nebo logicky 20
platné formule (nebo formule, jejichž splnitelnost je podmíněna splnitelností předpokladů pro dané ohodnocení). Krok indukce: podívejme se na člen s indexem k + 1. Jestliže se jedná o axiom, pak je jeho logická platnost již dokázána. Pokud tento člen vznikl aplikací některého dedukčního pravidla na předchozí členy posloupnosti, pak toto pravidlo bylo použito na logicky platné formule nebo na formule splnitelné pro všechna ohodnocení, ve kterých jsou splnitelné všechny předpoklady. Výše bylo ukázáno, že všechna dedukční pravidla zachovávají splnitelnost, tedy v posloupnosti důkazu na místě k + 1 je formule, která je logicky platná nebo splnitelná ve všech ohodnoceních, ve kterých jsou splnitelné všechny předpoklady až dosud v důkazu uvedené. Pokud krok indukce použijeme postupně na celou posloupnost důkazu, zjistíme, že poslední člen posloupnosti je formule splnitelná ve všech ohodnoceních, ve kterých jsou splnitelné všechny předpoklady. Obdobně lze dokázat také korektnost nepřímého důkazu, důkazů z hypotéz a větvených důkazů. 2 Než dokážeme úplnost Systému přirozené dedukce výrokové logiky, budeme potřebovat dvě pomocné věty. Lemma 3.6: (Lemma o neutrální formuli) B ` A,
¬B ` A
=⇒
` A
(3.9)
Důkaz: 1. B → A 2. ¬B → A 3. B ∨ ¬B
VD na Př1 VD na Př2 A (H1 ∨ H2)
(a) B (b) A
H1 EI(1,a)
(a) ¬B (b) A
H2 EI(2,a)
4. A
(z větveného důkazu)
Tedy jestliže lze formuli dokázat z některé formule i její negace, pak tento předpoklad již nemusíme zapisovat. 2 Lemma 3.7: Nechť F je formule obsahující právě výrokové proměnné p1 , p2 , . . . , pn . Ve zvolené valuaci v označme: F 0 = F , pokud I(F, v) = 1, p0i = pi , pokud v(pi ) = 1, 0 F = ¬F , pokud I(F, v) = 0 p0i = ¬pi , pokud v(pi ) = 0 pro každé i ∈ {1, . . . , n} 21
Pak platí p01 , p02 , . . . , p0n ` F 0
(3.10)
Důkaz: Důkaz provedeme matematickou indukcí podle složitosti formule (tj. podle počtu logických spojek). Báze indukce: F = p (0 logických spojek) p0 ` p0 platí, protože jde o substituci do druhého dedukčního pravidla ( ` A → A). Předpoklad indukce: předpokládejme, že věta platí pro formule B, C o složitosti nejvýše k: p01 , p02 , . . . , p0n ` B 0 p01 , p02 , . . . , p0n ` C 0 Krok indukce: dokážeme, že věta platí pro formuli F hloubky k + 1. a) F = ¬B, B je formule o složitosti k Máme dokázat, že platí p01 , p02 , . . . , p0n ` (¬B)0 . Protože platí předpoklad indukce, dokazujeme B 0 ` (¬B)0 . Jsou dvě možnosti: 1) I(B) = 0 ⇒ dokazujeme ¬B ` ¬B, což platí (axiom) 2) I(B) = 1 ⇒ dokazujeme B ` ¬¬B, to je dokázáno na str. 16 jako pomocné pravidlo zavedení negace. b) F = B → C, B, C jsou formule složitosti nejvýše k. Pak pro jednotlivé valuace dokazujeme: B 0 0 1 1
C 0 1 0 1
B→C 1 1 0 1
dokazujeme (B 0 , C 0 ` A0 ): ¬B, ¬C ` B → C ¬B, C ` B → C B, ¬C ` ¬(B → C) B, C ` B → C
1
2
3
4
Tabulka 3.3: Určení tvrzení, která je třeba dokázat 1 : 2
, Dokazujeme ¬B ` B → C, neboli ¬B, B ` C (podle věty o dedukci) ⇒ dokázáno, pravidlo sporné množiny (viz str. 15). 3
: Dokážeme nepřímým důkazem:
1. 2. 3. 4.
B ¬C B→C C
Př1 Př2 NZ EI(1,3), spor s 2
4
: Dokážeme přímým důkazem:
1. C 2. B → C
Př1 ZI(1) 22
Platnost indukčního kroku jsme dokázali pro negaci a implikaci. Dále můžeme buď totéž provést pro ostatní logické spojky (konjunkci, disjunkci a ekvivalenci) nebo dokázat věty o existenci ekvivalentních formulí, které obsahují pouze logické spojky negace a implikace. 2 Věta 3.8: (Věta o úplnosti Systému přirozené dedukce výrokové logiky) Každá logicky platná formule výrokové logiky je dokazatelná v Systému přirozené dedukce výrokové logiky, tedy platí |= A =⇒ ` A (3.11) Důkaz:
Předpokládejme, že A je tautologie
⇒ A je vždy splnitelná, pro všechna ohodnocení platí p01 , p02 , . . . , p0n ` A ⇒ Pak platí zároveň tyto věty: p1 , p02 , . . . , p0n ¬p1 , p02 , . . . , p0n
` `
A A
⇒ Podle lemmatu o neutrální formuli (viz str. 21) pak platí p02 , . . . , p0n ` A Stejně budeme postupovat i pro další výrokové proměnné, po n uplatněních tohoto postupu získáme větu ` A. Tím je vztah 3.11 dokázán. 2 Věta 3.9: Systém přirozené dedukce výrokové logiky je bezesporný. Důkaz:
Větu dokážeme sporem.
Kdyby byl systém sporný, pak by existovala formule A taková, že ` A a zároveň ` ¬A. Potom ale podle věty o korektnosti Systému přirozené dedukce výrokové logiky (viz str. 20) platí |= A a zároveň |= ¬A, což ale není možné. Proto je Systém přirozené dedukce výrokové logiky bezesporný. 2
3.4
Systém přirozené dedukce predikátové logiky
Jazyk Systému přirozené dedukce predikátové logiky přejímáme z predikátové logiky prvního řádu (PL1 ). Dedukční pravidla přejímáme ze Systému přirozené dedukce výrokové logiky a přidáváme další čtyři pravidla, která jsou uvedena v tabulce 3.4. Narozdíl od pravidel pro výrokovou logiku tato pravidla mají svá omezení: 23
1.-10. 11. 12. 13. 14.
Dedukční pravidla A(x) ` ∀A(x) ∀A(x) ` A(x/t) A(x/t) ` ∃A(x) ∃A(x) ` A(c)
přejatá ze Systému přirozené dedukce VL, viz str. 12 Z∀ Zavedení obecného kvantifikátoru E∀ Eliminace obecného kvantifikátoru Z∃ Zavedení existenčního kvantifikátoru E∃ Eliminace existenčního kvantifikátoru
Tabulka 3.4: Dedukční pravidla Systému přirozené dedukce predikátové logiky 1) Pro pravidla E∀ a Z∃: term t musí být substituovatelný za x. 2) Pro pravidlo E∃: c je individuová konstanta, která v posloupnosti důkazu dosud ještě nebyla použita. 3) Pro pravidlo E∃: jestliže A obsahuje nějaké volné proměnné y1 , . . . , yn (a žádné jiné), pak má pravidlo formu ∃A(x, y1 , . . . , yn ) ` A(f (y1 , . . . , yn ), y1 , . . . , yn ), tedy volné proměnné ponecháme a místo vázané proměnné dosadíme funkční symbol o n proměnných (n je počet volných proměnných), který v posloupnosti důkazu dosud nebyl použit. Pokud je vázaných proměnných více, dosadíme funkční symbol za každou z nich, ale pokaždé jiný. To odpovídá procesu skolemizace (viz kurz Úvod do logiky). Další věty a definice přejímáme ze Systému přirozené dedukce výrokové logiky. Příklad 3.13: Dokažte větu ∀x (A(x) → B(x)) → (∀xA(x) → ∀xB(x)) 1. 2. 3. 4. 5. 6.
∀x (A(x) → B(x)) ∀xA(x) A(x) → B(x) A(x) B(x) ∀xB(x)
Př1 Př2 E∀(1) E∀(2) EI(3,4) Z∀(5)
x je substituovatelný za x
Příklad 3.14: Dokažte větu ¬∀xA(x) → ∃x¬A(x) 1. ¬∀xA(x) 2. ¬∃x¬A(x) (a) ¬A(x) (b) ∃xA(x) 3. 4. 5. 6.
Př1 NZ H1 Z∃(a)
¬A(x) → ∃x¬A(x) (a → b) ¬∃x¬A(x) → A(x) T(3) A(x) EI(2,4) ∀xA(x) Z∀(5), spor s 1.
24
Příklad 3.15: Dokažte větu ∃x¬A(x) → ¬xA(x) 1. 2. 3. 4.
3.5
∃x¬A(x) ∀xA(x) ¬A(c) A(c)
Př1 NZ E∃(1) E∀(2), spor s 3.
Vlastnosti Systému přirozené dedukce predikátové logiky
Věta 3.10: (Věta o korektnosti Systému přirozené dedukce predikátové logiky) Každá formule dokazatelná v Systému přirozené dedukce predikátové logiky je logicky platná, tedy pro každou formuli A predikátové logiky platí: ` A Důkaz:
=⇒
|= A
(3.12)
(nástin důkazu)
Oproti důkazu věty o korektnosti Systému přirozené dedukce výrokové logiky stačí dokázat korektnost přidaných dedukčních pravidel, zbytek důkazu můžeme přejmout. Pravidlo č. 11, A(x) ` ∀xA(x) (Z∀): Provedeme důkaz logickou úvahou podle interpretace ve struktuře S: pokud |= A(x)[S] (formule je splněna ve struktuře S při kterékoliv valuaci e), znamená to, že formule A je logicky platná pro jakékoliv ohodnocení a interpretaci (ať za x dosadíme cokoliv, výsledkem je vždy logicky platná formule), zapisujeme I(∀xA[S, e(x/a)] = true pro kterýkoliv prvek univerza diskurzu a, tedy platí také |= ∀xA(x). Pravidlo č. 12, ∀xA(x) ` A(x/t) (E∀): Předpoklad ∀xA(x) znamená, že po dosazení libovolného prvku univerza diskurzu do formule A za x dostaneme vždy formuli interpretovanou jako true, proto když za x dosadíme term t, který je substituovatelný za x (tedy pokud t není přímo individuová konstanta z univerza, pak při jakémkoliv ohodnocení t je výsledkem některý prvek univerza), je také formule A(x/t) interpretována s výsledkem true. Pravidlo č. 13, A(x/t) ` ∃xA(x) (Z∃): Jestliže po dosazení t za x je formule A interpretována vždy s výsledkem true, pak je takto interpretována alespoň jednou pro některou strukturu a valuaci, což znamená ∃xA(x). Pravidlo č. 14, ∃A(x) ` A(c) (E∃): Jestliže existuje prvek univerza diskurzu, který můžeme dosadit za x a formule A je pak ve zvolené struktuře S interpretována jako true, pak tento prvek můžeme „nějak nazvatÿ. 25
Víme, že tento prvek existuje, ale nevíme, který to je, proto musíme zvolit název, který jsme dosud nepoužili. Definice důkazů jsme přejali ze Systému přirozené dedukce výrokové logiky, proto důkaz jejich korektnosti již nemusíme provádět, stačí, že jsme dokázali korektnost přidaných dedukčních pravidel. 2 Věta 3.11: (Věta o úplnosti Systému přirozené dedukce predikátové logiky) Každá logicky platná formule predikátové logiky je dokazatelná v Systému přirozené dedukce predikátové logiky, tedy platí |= A
=⇒
` A
(3.13)
Důkaz: Pokud rozšíříme důkaz vztahu 3.10 na str. 22 o kvantifikátory, můžeme pro větu o úplnosti přejmout celý důkaz věty o úplnosti Systému přirozené dedukce výrokové logiky ze str. 23. 2 Poznámka:
Větu o bezespornosti můžeme také přejmout včetně celého důkazu.
Poznámka: Pokusme se odvodit vztahy mezi korektností, úplností a bezesporností (týká se všech formálních systémů, nejen Systému přirozené dedukce). Označme K korektnost, U úplnost a B bezespornost. • K⇒B Když je systém korektní, je také bezesporný. • U &¬K ⇒ ¬B Úplný systém, který není korektní, je sporný. • U &¬B ⇒ ¬K Úplný systém, který je sporný, není korektní. • U &B ⇒ K Úplný a bezesporný systém je korektní. • Úplný systém nemusí být bezesporný. • Bezesporný systém nemusí být korektní (například tehdy, pokud některý axiom není logicky platná formule). • Bezesporný systém nemusí být úplný. Důkazy těchto tvrzení vyplývají přímo z definice korektnosti, úplnosti a bezespornosti. Nejsou náročné, proto je přenecháme čtenáři.
26
Kapitola 4 Hilbertovský axiomatický systém Tato kapitola pojednává o jednom z axiomatických formálních systémů, Hilbertovském axiomatickém systému. Jeho autorem je významný matematik z přelomu 19. a 20. století, David Hilbert. Hilbert se sice narodil v Rusku (v Kaliningradu), ale pracoval především v Německu, kde také vznikla většina jeho prací. Hilbertovský axiomatický systém byl vytvořen spíše pro použití v algebře a disciplínách z ní odvozených přesto byl po dlouhou dobu jedním z nejznámějších a nejpoužívanějších axiomatických systémů své doby. Dodnes je známá Hilbertovská axiomatika geometrie. V Hilbertovském axiomatickém systému provádíme pouze přímé důkazy, proto zde najdeme pouze definici (přímého) důkazu (příp. důkazu z předpokladů). Důsledkem tohoto faktu a také toho, že máme pouze jediné odvozovací pravidlo, je, že konstrukce důkazů je náročnější a delší než u Systému přirozené dedukce. Proto se zde mnohem více používají pomocná odvozovací pravidla, z nichž některá budou také dokázána. Stejně jako u předchozí kapitoly, i zde se nejdřív budeme věnovat systému založeném na jazyce výrokové logiky, a pak teprve definujeme také Hilbertovský axiomatický systém predikátové logiky. Podíváme se také na alternativní definici důkazu, která je pro vytváření některých teorií výhodnější.
4.1
Hilbertovský axiomatický systém výrokové logiky
Jazyk Hilbertovského axiomatického systému výrokové logiky přejímáme z výrokové logiky, kromě spojek konjunkce a disjunkce (z logických spojek používáme pouze negaci a implikaci), značíme ho LH . Logické axiomy jsou tři, jsou uvedeny v tabulce 4.1 na str. 28. Odvozovací pravidlo je pouze jedno, nazývá se Modus Ponens (MP): A → B,
A 27
`
B
(4.1)
1. 2. 3.
` A → (B → A) A1 ` (A → (B → C)) → ((A → B) → (A → C)) A2 ` (¬B → ¬A) → (A → B) A3
Tabulka 4.1: Axiomy Hilbertovského axiomatického systému výrokové logiky Definice 4.1: Důkaz formule F z předpokladů P1 , P2 , . . . , Pn je konečná posloupnost formulí A1 , A2 , . . . , Am jazyka LH , kde F = Am a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • Ai ∈ {P1 , . . . , Pn } (tj. je to některý z předpokladů), • Ai je logický axiom, • Ai vznikla použitím odvozovacího pravidla Modus Ponens na některé dva předchozí členy posloupnosti. Důkaz formule F (tj. bez předpokladů) je definován stejně, jen n = 0. Pro následující důkaz potřebujeme tuto větu: Příklad 4.1: Dokažte platnost věty A → A. Tuto větu budeme nazývat věta o implikaci a budeme značit VI. 1. P → ((P → P ) → P )) 2.
3. 4. 5.
A1 [A = P , B = P → P] (P → ((P → P ) → P )) → ((P → (P → P )) → (P → P )) A2 [A = P , B = P → P, C = P] (P → (P → P )) → (P → P ) MP(1,2) P → (P → P )) A1 [A = P , B = P] P →P MP(3,4)
Věta 4.1: (Věta o dedukci) P1 , P2 , . . . , Pn−1 , Pn ` Z
⇔
P1 , P2 , . . . , Pn−1 ` Pn → Z
(4.2)
Důkaz: „⇐ÿ: Předpokládejme, že platí P1 , P2 , . . . , Pn−1 ` Pn → Z. Pak pro tento vztah existuje důkazová posloupnost A1 , A2 , . . . , Am , kde Am = Pn → Z. Důkaz výsledného vztahu vytvoříme přidáním několika členů na konec této posloupnosti:
28
1. ... m − 2. m − 1. m. m + 1. m + 2.
A1 Am−2 Am−1 Pn → Z Pn Z
předpoklad MP(m,m + 1)
„⇒ÿ: Jestliže P1 , P2 , . . . , Pn−1 , Pn ` Z, potom existuje důkaz formule Z z předpokladů P1 , P2 , . . . , Pn−1 , Pn . Tímto důkazem je nějaká posloupnost A1 , A2 , . . . , Am , kde Z = Am . Důkaz provedeme matematickou indukcí podle délky posloupnosti důkazu (budeme postupovat od prvního členu posloupnosti krokem indukce až k poslednímu) a dokážeme, že pravdivost všech členů této posloupnosti je podmíněna platností Pn . Báze indukce: První člen důkazu A1 je buď logický axiom nebo jeden z předpokladů Pi pro i ∈ {1, . . . , n − 1} nebo samotná formule Pn . Pokud je to Pn , stačí dokázat větu Pn → Pn , což bylo učiněno výše (viz str. 28). Jestliže je to logický axiom nebo jiný předpoklad, pak je důkaz následující: 1. A1 axiom nebo předpoklad 2. A1 → (Pn → A1 ) A1 3. Pn → A1 MP(1,2) Předpoklad indukce: Nechť věta platí pro všechny členy posloupnosti až po k-tý člen včetně, tedy všechny členy posloupnosti až ke k-tému mohou být podmíněny formulí Pn . Krok indukce: Formule Ak+1 je buď logickým axiomem, nebo některým předpokladem (včetně předpokladu Pn ), nebo vznikla uplatněním pravidla Modus Ponens na některé dva předchozí členy posloupnosti. Budeme řešit pouze tento poslední případ, protože předchozí se řeší stejně jako v bázi indukce. Nechť tedy formule Ak+1 vznikla uplatněním MP na některé dva předchozí členy posloupnosti. Označme tyto členy Ai a Aj , i 6= j, kde Aj = (Ai → Ak+1 ). Protože i, j ≤ k, pro formule Ai a Aj je věta již dokázána, tedy ji na ně uplatníme a vzniklé formule použijeme jako první členy důkazu: 1. 2. 3. 4. 5.
Pn → Ai Př1 Pn → (Ai → Ak+1 ) Př2 (Pn → (Ai → Ak+1 )) → ((Pn → Ai ) → (Pn → Ak+1 )) A2 (Pn → Ai ) → (Pn → Ak+1 ) MP(2,3) Pn → Ak+1 MP(1,4) 2 29
Poznámka: Stejně jako v Systému přirozené dedukce (viz str. 13), pokud větu o dedukci použijeme rekurzívně n-krát, dostaneme ekvivalenci P1 , P2 , . . . , Pn−1 , Pn ` Z
` P1 → (P2 → . . . (Pn → Z) . . .)
⇔
(4.3)
Příklad 4.2: Dokažte platnost vztahu B ` A → B 1. B 2. B → (A → B) 3. A → B
Př1 A1 MP(2,4)
Tento vztah je ekvivalentem dedukčního pravidla ZI v Systému přirozené dedukce. Zde ho budeme nazývat pomocné odvozovací pravidlo oslabení, značíme PO.
Příklad 4.3: Dokažte platnost vztahu A → B, B → C 1. 2. 3. 4. 5. 6. 7.
A→B B→C (B → C) → (A → (B → C)) A → (B → C) (A → (B → C)) → ((A → B) → (A → C)) (A → B) → (A → C) A→C
` A→C
Př1 Př2 A1 [A = (B → C), B = A] MP(2,3) A2 MP(4,5) MP(1,6)
Tento vztah je pomocné odvozovací pravidlo tranzitivity implikace, značíme TI. Pokud na toto pravidlo uplatníme větu o dedukci, máme také dokázánu platnost několika formulí, například ` (A → B) → ((B → C) → (A → C)). Příklad 4.4: Dokažte platnost vztahu ¬A → ¬B ` B → A Důkaz lze provést prostým uplatněním věty o dedukci na axiom A3. Tento vztah nazýváme pomocné odvozovací pravidlo kontrapozice, značíme K. Příklad 4.5: Dokažte platnost vztahu ¬¬P eliminace negace, značíme EN. 1. 2. 3. 4. 5. 6. 7.
` P . Jde o pomocné odvozovací pravidlo Př1 A1 MP(1,2) A3 MP(3,4) K(5) MP(1,6)
¬¬P ¬¬P → (¬¬¬¬P → ¬¬P ) ¬¬¬¬P → ¬¬P (¬¬¬¬P → ¬¬P ) → (¬P → ¬¬¬P ) ¬P → ¬¬¬P ¬¬P → P P 30
Příklad 4.6: Dokažte platnost vztahu P 1. 2. 3. 4.
` ¬¬P . Tento vztah nazýváme pomocné odvozovací pravidlo zavedení negace, značíme ZN.
P Př1 ¬¬¬P → ¬P VD na pravidlo EN P → ¬¬P K(2) ¬¬P MP(1,3)
Příklad 4.7: Dokažte platnost vztahu A, ¬A ` B 1. 2. 3. 4. 5. 6.
A ¬A ¬A → (¬B → ¬A) ¬B → ¬A A→B B
Tento vztah budeme nazývat obdobně jako v Systému přirozené dedukce, pomocné odvozovací pravidlo sporné množiny, značíme SM.
Př1 Př2 A1 MP(2,3) K(4) MP(1,5)
Příklad 4.8: Dokažte platnost vztahu P, ¬Q ` ¬(P → Q) 1. 2. 3. 4. 5. 6.
P Př1 ¬Q Př2 P → ((P → Q) → Q) VD na MP (P → Q) → Q MP(1,3) ¬Q → ¬(P → Q) ZN+K(4) ¬(P → Q) MP(2,5)
Věta 4.2: (Lemma o neutrální formuli) A → B, ¬A → B Důkaz:
`
B
(4.4)
Pokud platí věty v předpokladech, musí existovat jejich důkazy:
C1 , C2 , . . . , Cu−1 , Cu , kde Cu = A → B, D1 , D2 , . . . , Dr−1 , Dr , kde Dr = ¬A → B. Formule A může být interpretována jako true (a) nebo false (b). V prvním případě přidáme k prvnímu důkazu formuli A, která je v tomto ohodnocení splnitelná (interpretována jako true), v druhém případě přidáme k druhému důkazu formuli ¬A. (a) I(A) = true: důkazová posloupnost bude vypadat takto: C1 , C2 , . . . , Cu−1 , A → B, A, B (uplatníme pravidlo MP na A → B, A, dostaneme B). (b) I(A) = f alse: důkazová posloupnost bude vypadat takto: D1 , D2 , . . . , Dr−1 , Dr = ¬A → B, ¬A, B. 31
Můžeme si dovolit rozdělit důkaz na dva případy podle toho, ve kterých ohodnoceních je či není splnitelná, protože splnitelnost předpokladů podmiňuje splnitelnost závěru (stačí zjistit, zda je závěr splnitelný v ohodnoceních, ve kterých jsou splnitelné předpoklady). 2 Poznámka: Tato věta je obdobou stejně pojmenovaného lemmatu pro Systém přirozené dedukce na str. 21, také ji lze chápat jako „Jestliže lze formuli dokázat z některého předpokladu i jeho negace, můžeme z množiny předpokladů odstranit tento předpoklad i jeho negaci.ÿ
4.2
Vlastnosti Hilbertovského axiomatického systému výrokové logiky
Stejně jako u Systému přirozené dedukce, i zde budeme pro důkaz úplnosti potřebovat dvě pomocné věty. První z nich, lemma o neutrální formuli, jsme již dokázali na str. 31, druhá je následující: Lemma 4.3: Nechť F je formule obsahující právě výrokové proměnné p1 , p2 , . . . , pn . Ve zvolené valuaci v označme: F 0 = F , pokud I(F, v) = 1, p0i = pi , pokud v(pi ) = 1, p0i = ¬pi , pokud v(pi ) = 0 pro každé i ∈ {1, . . . , n} F 0 = ¬F , pokud I(F, v) = 0 Pak platí p01 , p02 , . . . , p0n ` F 0 (4.5) Důkaz: Důkaz provedeme matematickou indukcí podle složitosti formule, bude hodně podobný důkazu obdobné věty pro Systém přirozené dedukce. Báze indukce: F = p (0 logických spojek) p0 ` p0 platí, protože jde o větu o implikaci ( ` A → A, viz str. 28) s uplatněnou větou o dedukci. Předpoklad indukce: předpokládejme, že věta platí pro formule B, C o složitosti nejvýše k: p01 , p02 , . . . , p0n ` B 0 p01 , p02 , . . . , p0n ` C 0 Krok indukce: dokážeme, že věta platí pro formuli F hloubky k + 1. a) F = ¬B, B je formule o složitosti k Máme dokázat, že platí p01 , p02 , . . . , p0n ` (¬B)0 . Protože platí předpoklad indukce, dokazujeme B 0 ` (¬B)0 . Jsou dvě možnosti: 1) I(B) = 0 ⇒ dokazujeme ¬B ` ¬B, což je opět věta o implikaci, 32
2) I(B) = 1 ⇒ dokazujeme B ` ¬¬B, to je dokázáno na str. 31 jako pravidlo zavedení negace. b) F = B → C, B, C jsou formule složitosti nejvýše k. Pak pro jednotlivé valuace dokazujeme: B 0 0 1 1
C 0 1 0 1
B→C 1 1 0 1
dokazujeme (B 0 , C 0 ` A0 ): ¬B, ¬C ` B → C ¬B, C ` B → C B, ¬C ` ¬(B → C) B, C ` B → C
1
2
3
4
Tabulka 4.2: Určení tvrzení, která je třeba dokázat 1 : 2
, Dokazujeme ¬B ` B → C, neboli ¬B, B ` C (podle věty o dedukci) ⇒ dokázáno, pravidlo sporné množiny (viz str. 31). 3
: Tento vztah je dokázán na str. 31 jako věta P, ¬Q ` ¬(P → Q). 4
: Jedná se o uplatnění věty o dedukci na první axiom ve tvaru C → (B → C).
Protože v Hilbertovském axiomatickém systému výrokové logiky nepoužíváme žádné další spojky (resp. je možné tyto spojky dodefinovat pomocí negace a implikace), je důkaz hotov. 2 Korektnost a úplnost Hilbertovského systému výrokové logiky jsou shrnuty v následující větě: Věta 4.4: (Postova věta) Formule dokazatelné v Hilbertovském axiomatickém systému výrokové logiky jsou právě logicky platné formule, tedy pro každou formuli výrokové logiky platí ` A
⇔
|= A
(4.6)
Důkaz: „⇒ÿ – korektnost Je třeba dokázat korektnost logických axiomů a odvozovacího pravidla MP, a potom korektnost konstrukce důkazu (tedy definice důkazu). Korektnost logických axiomů a odvozovacího pravidla můžeme stejně jako v Systému přirozené dedukce dokázat sémantickými tabulkami, například pro první axiom a odvozovací pravidlo jsou tabulky v tab. 4.3. Tyto tabulky je potřeba vytvořit i pro axiomy A2 a A3, to necháme na čtenáři. Logický axiom je korektní, pokud jsou v posledním sloupci pouze hodnoty 1 (true), u odvozovacího pravidla (příp. u odvozovacích pravidel) stačí, když jsou v posledním sloupci 33
A B 0 0 0 1 1 0 1 1
` A → (B → A) B → A A → (B → A) 1 1 0 1 1 1 1 1
A 0 0 1 1
A → B, A ` B A→B 0 1 1 1 0 0 1 1
B A 0 0 1 1
B 0 1 0 1
Tabulka 4.3: Sémantické tabulky pro první axiom a odvozovací pravidlo MP hodnoty 1 na řádcích odpovídajících valuacím, ve kterých jsou splnitelné předpoklady (v případě Modus Ponens je to poslední řádek), odvozovací pravidlo tedy zachovává splnitelnost. Korektnost konstrukce důkazu dokážeme matematickou indukcí podle pořadí členů v posloupnosti důkazu. Dokazujeme korektnost posloupnosti důkazu A1 , A2 , . . . , An podle definice na str. 28. Báze indukce: První člen posloupnosti důkazu je podle definice buď logický axiom nebo předpoklad. Pokud je to logický axiom, jeho korektnost jsme již dokázali, předpoklad pouze omezuje nutnost splnitelnosti závěru pro daná ohodnocení. Předpoklad indukce: Nechť je důkaz korektní až ke k-tému členu, tedy až po formuli Ak . To znamená, že všechny formule Ai pro i ≤ k jsou buď logicky platné nebo alespoň splnitelné ve všech ohodnoceních, ve kterých je splnitelná množina až dosud v posloupnosti uvedených předpokladů. Krok indukce: Formule Ak+1 je podle definice důkazu buď logický axiom nebo předpoklad nebo vznikla z předchozích členů posloupnosti uplatněním pravidla MP. První dvě možnosti jsou řešeny stejně jako v bázi indukce, pro třetí možnost předpokládejme, že Ak+1 byla odvozena pravidlem MP z i-tého a j-tého členu posloupnosti, kde i, j ≤ k, i 6= j, tedy pro oba tyto členy dokazovaný vztah již platí. Korektnost pravidla MP již byla dokázána, proto i formule Ak+1 je splnitelná ve všech ohodnoceních, ve kterých je splnitelná množina až dosud v posloupnosti uvedených předpokladů. Krok indukce budeme uplatňovat postupně na všechny členy důkazu až k poslednímu, kterým je dokazovaná věta. „⇐ÿ – úplnost Předpokládejme, že formule A je logicky platná. pak podle vztahu na str. 32 platí p01 , p02 , . . . , p0n ` A Potom platí zároveň tyto věty: p1 , p02 , . . . , p0n ¬p01 , p02 , . . . , p0n 34
` `
A A
Podle lemmatu o neutrální formuli (viz str. 31) pak platí p02 , . . . , p0n ` A Toto provedeme postupně pro všechny výrokové proměnné, které se ve formuli A vyskytují, důsledkem je pak dokazatelnost formule A v Hilbertovském systému. 2 Věta 4.5: (bezespornost systému) Hilbertovský axiomatický systém výrokové logiky je bezesporný. Důkaz: sporem.
Bezespornost formálního systému je definována na str. 11. Důkaz povedeme
Kdyby byl tento systém sporný, pak by v něm pro některou formuli A byla dokazatelná A i ¬A. Podle Postovy věty by pak platilo |= A i |= ¬A, což není možné. Tedy Hilbertovský systém výrokové logiky je bezesporný. 2 Věta 4.6: (minimálnost systému) Hilbertovský axiomatický systém výrokové logiky je minimální. Důkaz:
(nástin)
Minimálnost formálního systému je definována na str. 11. Množina M bude obsahovat axiomy A1, A2 a A3 a dále formuli A → ((A → B) → B)), která je uplatněním věty o dedukci na pravidlo Modus Ponens. Jeden prvek množiny, nazvěme ho P , znegujeme (tedy formuli P nahradíme v množině její negací ¬P ) a zjistíme, zda je takto upravená množina formulí nesplnitelná. Pokud ano, znamená to, že formule P je odvoditelná z ostatních formulí množiny M (odvozená formule P je ve sporu s přidanou formulí ¬P ) a je tedy nadbytečná. Nesplnitelnost zjišťujeme metodami sémantické analýzy. Tento krok provedeme postupně pro všechny formule v množině M. Když ani jedna z upravených množin formulí není nesplnitelná, pak je systém minimální. 2 Poznámka: Při používání axiomatického systému obvykle stačí, aby byla minimální množina axiomů. Pak se minimálnost může dokazovat „uvnitř systémuÿ tak, že v množině axiomů jeden nahradíme jeho negací, a pak odvozujeme formální teorii1 pomocí odvozovacích pravidel systému. Pokud dojdeme ke sporu, nahrazovaný axiom je nadbytečný a můžeme ho vyřadit (protože je odvoditelný z ostatních axiomů pomocí odvozovacích pravidel systému). 1
Formální teorie je teorie budovaná bez speciálních axiomů, tedy pouze nad formálním systémem. Je to množina všech vět dokazatelných v tomto formálním systému, tedy včetně jeho axiomů.
35
4.3
Alternativní konstrukce důkazu
Při vytváření teorií může být výhodnější trochu jiný způsob konstrukce důkazu. Definice 4.2: Důkaz formule F z dokazatelných formulí je konečná posloupnost formulí A1 , A2 , . . . , Am dokazatelných v Hilbertovském axiomatickém systému výrokové logiky, kde F = Am a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • • • • •
Ai je logický axiom, Ai je předpoklad, Ai je věta (pravidlo) Hilbertovského axiomatického systému výrokové logiky, Ai vznikla použitím věty o dedukci na některý předchozí člen posloupnosti, Ai vznikla použitím odvozovacího pravidla Modus Ponens na některé dva předchozí členy posloupnosti.
Pod pojmem formule dokazatelná v Hilbertovském systému výrokové logiky zde budeme chápat vztah P1 , P2 , . . . , Pn ` F , tedy nejen samotnou formuli, ale i předpoklady určující její splnitelnost. Na každém řádku musí být právě jeden symbol dokazatelnosti ` . Pokud použijeme kterékoliv pravidlo na předchozí členy posloupnosti důkazu, včetně pomocných (kromě věty o dedukci), musíme do množiny takto vytvořené formule zařadit předpoklady všech formulí, na které jsme pravidlo použili. V tomto typu důkazu se s výhodou používá věta o dedukci, což si ukážeme na následujícím příkladu (je to důkaz pomocného odvozovacího pravidla tranzitivity implikace): Příklad 4.9: Dokažte platnost vztahu A → B, B → C ` A → C (viz str. 30, pomocné odvozovací pravidlo tranzitivity implikace TI) 1. ` (B → C) → (A → (B → C)) 2. B → C ` → A → (B → C) 3. ` (A → (B → C)) → ((A → B) → (A → C)) 4. B → C ` (A → B) → (A → C) 5. A → B, B → C ` A → C
A1 VD(1) A2 MP(2,3) VD(4)
Příklad 4.10: Tentýž vztah můžeme dokázat také jinak, pouze s pomocí již dokázané formule P ` P , věty o dedukci a pravidla Modus Ponens: 1. 2. 3. 4. 5.
dokázaná formule dokázaná formule VD(1) MP(2,3) VD(4)
A→B ` A→B B→C ` B→C A → B, A ` B A → B, A, B → C ` C A → B, B → C ` A → C
36
Příklad 4.11: Dokažte platnost vztahu U ` B ⇒ U, A ` B (viz str. 30, pomocné odvozovací pravidlo oslabení PO) Druhá možnost: První možnost: 1. U ` B 2. ` B → (A → B) 3. U ` A → B 4. U, A ` B
1. 2. 3. 4. 5.
Př1 A1 MP(1,2) VD(3)
U ` B Př1 ` B → (A → B) A1 U ` A→B MP(1,2) A ` A dokázaná formule U, A ` B MP(3,4)
Věta 4.7: Ke každému důkazu formule z dokazatelných formulí existuje ekvivalentní důkaz z předpokladů. Důkaz:
Důkaz provedeme matematickou indukcí.
Báze indukce: Prvním členem posloupnosti může být buď logický axiom, nebo předpoklad nebo již dokázaná věta (pravidlo). Logický axiom je dokazatelný (sám ze sebe), také pro každou dokázanou větu existuje důkaz z předpokladů, uvedení této věty je pouze zkrácením celého důkazu. Předpoklady stejně jako u důkazu z předpokladů pouze omezují množinu valuací, ve kterých musí být výsledná formule splnitelná. Předpoklad indukce: Předpokládejme, že věta platí až ke k-tému členu posloupnosti důkazu z dokazatelných formulí. Krok indukce: Pro k + 1-ní člen této posloupnosti platí jedna z těchto možností: • je to logický axiom, předpoklad nebo již dokázaná věta. Zde postupujeme jako u báze indukce. • tato formule vznikla uplatněním věty o dedukci na některý předchozí člen posloupnosti. Korektnost použití věty o dedukci vyplývá z důkazu této věty a z Postovy věty (z dokazatelné formule vznikne uplatněním VD opět dokazatelná formule). • formule vznikla uplatněním pravidla Modus Ponens na některé předchozí dva členy posloupnosti. Protože MP zachovává splnitelnost, platí: jestliže U1 ` A → B a zároveň U2 ` A, pak také U1 ∪ U2 ` B (sjednocení množin předpokladů omezí množinu valuací, ve kterých musí být B splnitelná, na pouze ty valuace, ve kterých jsou splnitelné všechny předpoklady z obou množin). 2 Tím je dokázána korektnost tohoto typu důkazu, tedy pokud je jeho použití pro danou formuli výhodnější, můžeme ho volně použít.
37
4.4
Hilbertovský axiomatický systém predikátové logiky
Jazyk Hilbertovského axiomatického systému predikátové logiky přejímáme z predikátové logiky prvního řádu, kromě spojek konjunkce a disjunkce a existenčního kvantifikátoru (existenční kvantifikátor lze definovat pomocí obecného kvantifikátoru a negace), značíme ho LH1 . Logických axiomů je pět. První tři přejímáme z Hilbertovského systému výrokové logiky, zbývající dva jsou uvedeny v tabulce 4.4 na str. 38. A1,A2,A3 Axiomy přejaté z Hilbertovského systému výrokové logiky, viz str. 28 A4 ` ∀xA → A(x/t) A4 (axiom specifikace) A5 ` ∀x(A → B) → (A → ∀xB) A5 (axiom kvantifikace implikace) Tabulka 4.4: Axiomy Hilbertovského axiomatického systému predikátové logiky Narozdíl od axiomů pro výrokovou logiku tyto axiomy mají svá omezení: 1) Pro axiom A4: term t musí být substituovatelný za x. 2) Pro axiom A5: x nesmí být volná proměnná v A. Odvozovací pravidla jsou dvě – Modus Ponens definované vztahem 4.1 na str. 27, a dále odvozovací pravidlo generalizace (značíme G): A
`
∀xA
(4.7)
Definice 4.3: Důkaz formule F z předpokladů P1 , P2 , . . . , Pn je konečná posloupnost formulí A1 , A2 , . . . , Am jazyka LH1 , kde F = Am a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • Ai ∈ {P1 , . . . , Pn } (tj. je to některý z předpokladů), • Ai je logický axiom, • Ai vznikla použitím odvozovacího pravidla Modus Ponens na některé dva předchozí členy posloupnosti, • Ai vznikla použitím odvozovacího pravidla generalizace na některý předchozí člen posloupnosti. Důkaz formule F (tj. bez předpokladů) je definován stejně, jen n = 0. Vše, co jsme dále definovali a dokázali v Hilbertovském axiomatickém systému výrokové logiky, přejímáme. Dále se budeme zabývat pouze větami, které se týkají predikátové logiky. 38
Příklad 4.12: Dokažte platnost vztahu A → B ` ∀xA → ∀xB 1. 2. 3. 4. 5. 6.
A→B Př1 ∀xA → A A4 ∀xA → B TI(1,2) ∀x(∀xA → B) G(3) ∀x(∀xA → B) → (∀xA → ∀xB) A5 ∀xA → ∀xB MP(4,5)
Příklad 4.13: Tentýž vztah dokážeme důkazem z dokazatelných formulí: 1. 2. 3. 4. 5. 6.
A → B ` A → B dokázaná ` ∀xA → A A → B ` ∀xA → B A → B, ∀xA ` B A → B, ∀xA ` ∀xB A → B ` ∀xA → ∀xB
formule A4 TI(1,2) VD(3) G(4) VD(5)
Příklad 4.14: Dokažte platnost vztahu A → B ` A → ∀xB (x není volná v A) 1. 2. 3. 4.
4.5
A→B ∀x(A → B) ∀x(A → B) → (A → ∀xB) A → ∀xB
Př1 G(1) A5 MP(2,3)
Toto je pomocné odvozovací pravidlo zavedení obecného kvantifikátoru, značíme Z∀.
Vlastnosti Hilbertovského axiomatického systému predikátové logiky
Věta 4.8: Formule dokazatelné v Hilbertovském axiomatickém systému predikátové logiky jsou právě logicky platné formule predikátové logiky, tedy pro každou formuli predikátové logiky platí ` A
⇔
|= A
(4.8)
Důkaz: „⇒ÿ – korektnost Korektnost logických axiomů A1, A2 a A3 a odvozovacího pravidla MP již byla dokázána pro výrokovou logiku, rozšíření důkazu na predikátovou by bylo možné provést nepřímým 39
důkazem. Dále je potřeba dokázat korektnost axiomů A4 a A5 a odvozovacího pravidla Generalizace. Důkaz korektnosti konstrukce důkazu můžeme také přejmout. Axiom A4, ∀xA(x) ` A(x/t) (důkaz sporem): Označme a prvek univerza diskurzu, který vznikne vyhodnocením termu t ve struktuře S. Jestliže ∀xA(x) ` A(x/t) neplatí, znamená to, že formule ∀xA(x) má v této struktuře hodnotu true a formule A(x/t) hodnotu false (vyplývá z definice implikace). V tom případě ale I(A(x/t)) = I(A(x/a)) = f alse, což je ve sporu s platností formule ∀xA(x). Obdobně lze dokázat také platnost axiomu A5 a odvozovacího pravidla Generalizace. „⇐ÿ – úplnost Máme dokazatelnou formuli predikátové logiky ` A. Podle této formule vytvoříme výrokovou formuli B tak, že provedeme skolemizaci, převedeme formuli A do klauzulární formy, oddělíme prefix s kvantifikátory a za atomické formule s (vázanými) predikátovými proměnnými dosadíme (substituujeme) výrokové proměnné. Pokud za různé atomické formule (lišící se predikátem nebo predikátovými proměnnými) dosadíme různé výrokové proměnné, stačí dokázat úplnost pro takto získanou formuli B, což jsme učinili dříve pro Hilbertovský axiomatický systém výrokové logiky. Důkaz úplnosti Hilbertovského systému predikátové logiky jsme tedy tímto způsobem převedli na důkaz úplnosti Hilbertovského systému výrokové logiky. 2 Poznámka: Pravidlo Generalizace se má správně psát takto: ` A[S] ⇒ ` ∀xA[S], tedy splnitelnost A se vztahuje k určité struktuře. Neplatí však věta ` A → ∀xA, viz důkaz níže. Proč tedy můžeme používat pravidlo Generalizace? Protože toto pravido sice nezachovává splnitelnost, ale zachovává alespoň logickou pravdivost – dokazatelnost (z dokazatelné formule vytvoří dokazatelnou formuli), což nám stačí. Jen si musíme dávat pozor na kombinování věty o dedukci a pravidla Generalizace. Věta 4.9: Neplatí ` A → ∀xA. Důkaz: Nechť univerzum diskurzu obsahuje prvky a, b (a případně i další) takové, že I(A(x/a)) = true a I(A(x/b)) = f alse.2 Pak ale není platná formule ∀xA (protože A není interpretována jako true pro všechny hodnoty x, jen pro některé), a dokonce je kontradiktorická, tedy I(∀A) = f alse pro jakékoliv ohodnocení. Ze sémantického významu implikace vyplývá, že I((A → ∀xA)(x/b)) = f alse, tedy A → ∀xA nemůže být logicky platná. 2
2
Pro připomenutí: zápis I(A(x/a)) znamená, že ve formuli A dosadíme (substituujeme) za všechny výskyty predikátové proměnné x hodnotu a (zde se jedná o prvek univerza diskurzu).
40
Kapitola 5 Gentzenovský formální systém Autorem Gentzenovského formálního systému je matematik Gerhard Gentzen (vlastně Gerhard Karl Erich Gentzen). Gentzen byl po několik let asistentem Davida Hilberta, po Hilbertově odchodu pokračoval v jeho práci a kromě jiného vytvořil formální systém postavený na odlišné bázi než původní Hilbertův. Gentzenovský systém je uváděn jako předpokladový, v jiné literatuře jako axiomatický. Pokud jde o to, zda můžeme používat i jinou formu důkazu než důkaz přímý, pak v Gentzenovském systému je sice používán pouze přímý důkaz (příp. z předpokladů), ale protože postup důkazu formule bez předpokladů je vlastně duální k postupu konstrukce sémantického tabla dokazované formule, lze jako pomůcku nejdřív zkonstruovat tablo coby nepřímý důkaz a pak dualizací vytvořit přímý důkaz v Gentzenovském systému. Možná proto se tento systém pohybuje „na pomezíÿ mezi předpokladovými a axiomatickými systémy. V této kapitole si nejdřív připomeneme proces dualizace, potom definujeme Gentzenovský systém výrokové logiky, dokážeme jeho korektnost a úplnost a pak totéž provedeme pro predikátovou logiku.
5.1
Dualizace
Podívejme se na následující dvě tabulky: A 0 0 1 1
B 0 1 0 1
A &B 0 0 0 1
U 1 1 0 0
V 1 0 1 0
U ∨V 1 1 1 0
Tabulka 5.1: Sémantická tabulka pro konjunkci a disjunkci
41
Jsou to tabulky pro konjunkci a disjunkci, které jistě každý zná. Když se pozorněji podíváme na obsah tabulek, zjistíme, že tam, kde je v první tabulce 0, je v druhé tabulce 1 a naopak. Proto o logických spojkách konjunkce a disjunkce říkáme, že jsou navzájem duální. Pod pojmem dualizace obecně rozumíme dvojici prvků, které mají stejnou základní strukturu, ale jednotlivé odpovídající části této struktury jsou v určitém smyslu navzájem inverzní s tím, že podle jednoho prvku dokážeme sestrojit druhý a naopak. Dualizovaný prvek budeme odlišovat horním indexem D . V případě duálních logických spojek konjunkce a disjunkce v tabulce 5.1 je dualizační operací (faktorem) operace negace. V tabulce pro disjunkci můžeme provést substituce U = AD = ¬A, V = B D = ¬B, (U ∨ V ) = (A &B)D = ¬(A &B) = (¬A ∨ ¬B) = (AD ∨ B D ). K formuli A &B je duální formule ¬A ∨ ¬B. Pokud postup, který jsme použili na druhou tabulku, použijeme na tabulku první, zjistíme, že k formuli U ∨ V je duální formule ¬U &¬V . Jak k dané formuli vytvořit duální formuli? Můžeme tuto formuli prostě znegovat. Pokud ale je formule v konjunktivní normální formě1 , máme práci mnohem jednodušší. Stačí všechny literály znegovat a zaměnit navzájem logické spojky konjunkce a disjunkce. Výsledná formule je v disjunktivní normální formě2 . V případě predikátové logiky také můžeme dualizaci provést prostým znegováním formule. Příklad 5.1: K formuli (A ↔ B) &C &(C → ¬B) &A najděte duální formuli. Formuli převedeme do KNF: (¬A ∨ B) &(¬B ∨ A) &C &(¬C ∨ ¬B) &A Provedem dualizaci: (A &¬B) ∨ (B &¬A) ∨ ¬C ∨ (C &B) ∨ ¬A Všimněme si, že zatímco původní formule byla kontradikce, formule k ní duální, kterou jsme vytvořili, je tautologie (můžeme ověřit například sémantickým stromem). Věta 5.1: Pro každou formuli A platí: je-li A logicky platná, pak je AD nesplnitelná, je-li A nesplnitelná, pak je AD logicky platná. Důkaz: Platnost věty plyne ze samotného procesu dualizace, kdy formuli znegujeme. Negace logicky platné formule je formule nesplnitelná, negace nesplnitelné formule je formule logicky platná. 2 1
Fromule výrokové logiky je v KNF, pokud je tvořena podformulemi spojenými konjunkcemi, v podformulích se vyskytují pouze disjunkce, a negace jsou pouze přímo u literálů. Pod pojmem literál rozumíme výrokovou proměnnou nebo její negaci. 2 Formule výrokové logiky je v DNF, pokud je tvořena podformulemi spojenými disjunkcemi, v podformulích se vyskytují pouze konjunkce, a negace jsou pouze přímo u literálů.
42
5.2
Gentzenovský systém výrokové logiky
Gentzenovský systém budeme probírat pouze v základní formě, jako ukázku toho, že existují systémy s poněkud jednodušším způsobem konstrukce důkazu. Z toho důvodu si definujeme pouze přímý důkaz bez předpokladů, protože předpoklady znemožňují jednodušší metodu konstrukce důkazu a je potřeba postupovat „klasickou cestouÿ stejně jako u dříve definovaných formálních systémů. Jazyk Gentzenovského systému výrokové logiky budeme značit LG , přejímáme jazyk výrokové logiky včetně všech logických spojek. Kromě formulí samotných zde budeme pracovat s množinami formulí. Prvky množiny formulí jsou pochopitelně formule (může být ale i prázdná množina), ze syntaktického a sémantického hlediska je mezi formulemi v množině vztah disjunkce. Logický axiom (schéma) je jediný, je to množina formulí U obsahující některou výrokovou proměnnou i její negaci – ∃p : (p ∈ U) & (¬p ∈ U). Protože je mezi prvky množiny formulí vztah disjunkce, znamená, že množina U představuje formuli p ∨ ¬p ∨ . . ., která je tautologie. Odvozovací pravidla jsou v tab. 5.2. Název
Předpis
α= α-pravidlo U ∪ {α1 , α2 } ` U ∪ {α} = = β= β-pravidlo U1 ∪ {β1 }, U2 ∪ {β2 } ` U1 ∪ U2 ∪ {β} = =
α1 ∨ α2 ¬(¬α1 &¬α2 ) ¬α1 → α2 β1 &β2 ¬(¬β1 ∨ ¬β2 ) ¬(β1 → ¬β2 )
Tabulka 5.2: Odvozovací pravidla v Gentzenovském systému výrokové logiky Není náhoda, že odvozovací pravidla Gentzenovského systému jsou nazvána stejně jako pravidla používaná v sémantickém tablu. Konstrukce přímého důkazu je totiž v tomto systému duální ke konstrukci nepřímého důkazu pomocí sémantického tabla. Odvozovací pravidla systému jsou duální k pravidlům tabla (je zaměněna konjunkce a disjunkce a literály jsou znegovány – to znegování se v obecném předpisu neobjeví), a totéž platí i o axiomu a obecně o množinách formulí (zde jsou prvky množiny spojeny disjunkcí, v tablu je to konjunkce, zde vyžadujeme, aby byl axiom logicky platná množina, v listech sémantického tabla musí být nesplnitelná množina formulí). Definice 5.1: Důkaz formule F je konečná posloupnost množin formulí A1 , A2 . . . , Am jazyka LG , kde Am = {F } a pro každé i ∈ {1, . . . , m} platí pro Ai některá z možností: • Ai je logický axiom, • Ai vznikla použitím odvozovacího pravidla (α, β) na předchozí členy posloupnosti. 43
Při konstrukci důkazu můžeme jako pomůcku využít sémantické tablo: • vytvoříme nepřímý důkaz formule pomocí sémantického tabla (tj. formuli negujeme a vytvoříme sémantické tablo pro tuto negaci), • sestavíme duální tablo – sémantické tablo obrátíme listy vzhůru a kořenem dolů a všechny množiny formulí v uzlech tabla znegujeme (provedeme dualizaci formulí v množinách v uzlech tabla), • množiny formulí v duálním tablu přepíšeme do řádkového důkazu tak, že postupujeme od listů stromu a množinu formulí každého uzlu zařadíme do důkazu tak, aby byla uvedena až po množinách formulí z předchůdců tohoto uzlu (tedy postupujeme od listů ke kořeni stromu). Příklad 5.2: Dokažte větu (A ∨ B) ∨ ((A ∨ ¬B) &¬A). Nejdřív sestavíme pomocné struktury – sémantické tablo a duální tablo. ¬((A ∨ B) ∨ ((A ∨ ¬B) &¬A))
A, B, A, ¬B
α
α
¬(A ∨ B), ¬((A ∨ ¬B) &¬A)
A, B, A ∨ ¬B @
α ¬A, ¬B, ¬((A ∨ ¬B) &¬A) @
¬A, ¬B, ¬(A ∨ ¬B)
@
@
@
A, B, ¬A β
@
A, B, (A ∨ ¬B) &¬A
β
α A ∨ B, (A ∨ ¬B) &¬A
¬A, ¬B, A
α
α (A ∨ B) ∨ ((A ∨ ¬B) &¬A)
¬A, ¬B, ¬A, B
Obrázek 5.1: Sémantické tablo negace formule a duální tablo formule Řádkový důkaz: 1. A, B, A, ¬B 2. A, B, A ∨ ¬B 3. A, B, ¬A
axiom α1 axiom
4. A, B, (A ∨ ¬B) &¬A 5. A ∨ B, (A ∨ ¬B) &¬A 6. (A ∨ B) ∨ ((A ∨ ¬B) &¬A) 44
β2,3 α4 α5
5.3
Korektnost a úplnost systému
Věta 5.2: Formule dokazatelné v Gentzenovském systému výrokové logiky jsou právě logicky platné formule, tedy pro každou formuli výrokové logiky platí ` A
⇔
|= A
(5.1)
Důkaz: „⇒ÿ – korektnost Předpokládejme, že formule A je dokazatelná v G. Potom existuje její řádkový důkaz a také duální tablo formule a sémantické tablo negace formule. Korektnost konstrukce popírajícího sémantického tabla negace formule je dokázána v kap. 2.3 na str. 10. Dále využijeme větu na str. 42, která říká, že formule duální k nesplnitelné formuli je logicky platná. Sémantické tablo konstruujeme tak, že v jeho kořeni je negace dokazované formule. Pokud jsou v listech stromu nesplnitelné formule, dokázali jsme, že formule v kořeni stromu (tj. negace formule, se kterou pracujeme), je nesplnitelná. Dualizací získáme duální tablo, které má ve svém kořeni dokazovanou formuli. Jestliže v listech sémantického tabla byly nesplnitelné formule, pak v listech duálního tabla jsou logicky platné formule a v jeho kořeni logicky platná formule. Důkaz můžeme provést přímo pro řádkový důkaz v Gentzenovském systému. Pak stačí dokázat korektnost logického axiomu (již bylo naznačeno u jeho definice) a odvozovacích pravidel, a pak matematickou indukcí korektnost konstrukce přímého důkazu vycházející z jeho definice, stejně jako u dříve definovaných formálních systémů. „⇐ÿ – úplnost Jestliže A je logicky platná, pak ¬A je nesplnitelná a sémantické tablo formule ¬A se uzavře. Potom existuje duální tablo, v jehož kořeni je formule A, a je ekvivalentní některému řádkovému důkazu formule A. Proto platí, že formule A je dokazatelná v G. 2
5.4
Gentzenovský systém predikátové logiky
Jazyk Gentzenovského systému predikátové logiky přejímáme z jazyka predikátové logiky prvního řádu včetně všech logických spojek, stejně jako u výrokové logiky zde budeme pracovat s množinami formulí, ve kterých je mezi prvky (formulemi) vztah disjunkce. Logický axiom (schéma) množina formulí U obsahující komplementární pár literálů některé atomické formule p(x1 , x2 , . . . , xn ), tedy (p(a1 , a2 , . . . , an ) ∈ U) & (¬p(a1 , a2 , . . . , an ) ∈ U). 45
Odvozovací pravidla jsou v tab. 5.3. Název
Předpis
α-pravidlo U ∪ {α1 , α2 } ` U ∪ {α}
β-pravidlo
U1 ∪ {β1 }, U2 ∪ {β2 } ` U1 ∪ U2 ∪ {β}
γ-pravidlo
U ∪ {∃A(x), A(a)} ` U ∪ {∃A(x)}
α= = = β= = =
α1 ∨ α2 ¬(¬α1 &¬α2 ) ¬α1 → α2 β1 &β2 ¬(¬β1 ∨ ¬β2 ) ¬(β1 → ¬β2 )
U ∪ {¬∀A(x), ¬A(a)} ` U ∪ {¬∀A(x)} δ-pravidlo
U ∪ {A(a)} ` U ∪ {∀A(x)} U ∪ {¬A(a)} ` U ∪ {¬∃A(x)}
Tabulka 5.3: Odvozovací pravidla v Gentzenovském systému predikátové logiky Definice 5.2: Důkaz formule F je konečná posloupnost množin formulí A1 , A2 . . . , Am , kde Am = {F } a pro každé i ∈ {1, . . . , m} platí pro Ai některá z možností: • Ai je logický axiom, • Ai vznikla použitím odvozovacího pravidla (α, β, γ, δ) na předchozí členy posloupnosti. Příklad 5.3: Dokažte větu ∀x(A(x) → B(x)) → (∀xA(x) → ∀xB(x)). Uvedeme zde pouze řádkový důkaz, sémantické a duální tablo si čtenář může sestavit sám. 1. 2. 3. 4. 5. 6. 7. 8.
A(m), ¬∀x(A(x) → B(x)), ¬A(m), ¬∀xA(x), B(m) ¬B(m), ¬∀x(A(x) → B(x)), ¬A(m), ¬∀xA(x), B(m) ¬(A(m) → B(m)), ¬∀x(A(x) → B(x)), ¬A(m), ¬∀xA(x), B(m) ¬∀x(A(x) → B(x)), ¬A(m), ¬∀xA(x), B(m) ¬∀x(A(x) → B(x)), ¬∀xA(x), B(m) ¬∀x(A(x) → B(x)), ¬∀xA(x), ∀xB(x) ¬∀x(A(x) → B(x)), ∀xA(x) → ∀xB(x) ∀x(A(x) → B(x)) → (∀xA(x) → ∀xB(x))
axiom axiom β(1,2) γ(3) γ(4) δ(5) α(6) α(7)
Věta 5.3: Formule dokazatelné v Gentzenovském systému predikátové logiky jsou právě logicky platné formule predikátové logiky prvního řádu. Důkaz:
Je obdobný důkazu věty pro Gentzenovský systém výrokové logiky.
46
2
Kapitola 6 Klauzulární logika Až dosud jsme formální systémy stavěli na výrokové logice nebo predikátové logice prvního řádu. Později budeme definovat další formální systém, ale tentokrát nad klauzulární logikou. Protože klauzulární logika a na ní postavený Klauzulární axiomatický systém budou přímo navrženy tak, aby byly použitelné pro logické programování, budeme s tím počítat již při definování syntaxe a sémantiky klauzulární logiky. Využijeme to, co nabízí predikátová logika, ale syntaxi a sémantiku upravíme a přidáme další mechanismy.
6.1
Hornovy klauzule
V klauzulární logice budeme pracovat s klauzulemi ve speciálním tvaru, které budeme nazývat Hornovy klauzule. Definice 6.1: Klauzule jsou definovány induktivně: Báze: Literály predikátů jsou klauzule. Indukce: Jestliže A a B jsou klauzule, pak A ∨ B je také klauzule. Zobecnění: Všechny formule, které jsou utvořeny použitím konečného počtu pravidel v bázi a indukci, jsou klauzule, žádná jiná formule není klauzule. Definice 6.2: Hornovy klauzule jsou klauzule s nejvýše jedním pozitivním literálem (tj. literálem bez negace). Můžeme je psát v následujících tvarech: ¬A1 ∨ ¬A2 ∨ . . . ∨ ¬An ∨ B (A1 , A2 , . . . , An ) → B
(6.1) (6.2)
V klauzulární logice (ale ne ve všech logických jazycích) používáme zobecněné Hornovy klauzule s jakýmkoliv počtem pozitivních literálů (tedy obecně klauzule): ¬A1 ∨ ¬A2 ∨ . . . ∨ ¬An ∨ B1 ∨ B2 ∨ Bm (A1 &A2 & . . . &An ) → (B1 ∨ B2 ∨ . . . ∨ Bm ) 47
(6.3) (6.4)
6.2
Syntaxe jazyka klauzulární logiky
Syntaxe jazyka klauzulární logiky je podobná syntaxi jazyka predikátové logiky prvního řádu. Hlavním rozdílem je používání jediné logické spojky – implikace. Nepoužíváme dokonce ani negaci, samotnou negaci reprezentujeme jiným způsobem. Nejsou definovány také žádné kvantifikátory, pro reprezentaci univerzálních a existenčních tvrzení opět budeme používat jiné mechanismy.
6.2.1
Jazyk klauzulární logiky
Definice 6.3: Abeceda jazyka klauzulární logiky zahrnuje následující symboly: • Proměnné – začínají velkým písmenem, například X, Prom, Matka, Pocet, Soucet, Zvire, Smer cesty, . . . • Individuové konstanty – čísla nebo začínají malým písmenem, například 28, 3.14159, jaguár, lenka, . . . (pozor, i vlastní jména a jiné názvy musí začínat malým písmenem, pokud jsou to konstanty) • Logické konstanty – true (t, 1), false (f, 0) • Existenční (Skolemovy) konstanty – začínají vždy symbolem @, například @a, @e, @x, @neco, . . . • Funkční symboly (funktory) – začínají obvykle malým písmenem, každý funktor má přiřazenu aritu – přirozené číslo (včetně nuly) určující počet argumentů funktoru, např. soucet(X,Y,S) má aritu 3, zapisujeme soucet/3 • Existenční (Skolemovy) funktory – také mají aritu, například @f /3 • Predikátové symboly – začínají písmenem, taktéž mají aritu • Logická spojka – implikace (→) • Pomocné symboly – čárky, závorky Definice 6.4: Termy jazyka klauzulární logiky definujeme induktivně: Báze: Každá proměnná, individuová konstanta a existenční konstanta je term. Indukce: Každý funkční symbol, jehož argumenty jsou termy, je term. Každý existenční funktor, jehož argumenty jsou termy, je term. 48
Zobecnění: Každý term vznikne pouze konečným počtem použití pravidel stanovených v bázi a indukci, nic jiného není term. Atomy jazyka klauzulární logiky jsou logické konstanty a dále predikátové symboly, jejichž argumenty jsou termy. Bázový term je term, v němž se nevyskytuje žádná proměnná ani existenční term. Bázový atom je atom, jehož atributy jsou bázové termy. Definice 6.5: Klauzuli reprezentujeme předpisem {p1 , p2 , . . . , pn } → {q1 , q2 , . . . , qm } |
{z
}
|
antecedent(A)
{z
(6.5)
}
konsekvent(K)
Kde pi , i ∈ {1, 2, . . . , n} a qj , j ∈ {1, 2, . . . , m} jsou atomy jazyka klauzulární logiky. Mezi atomy v antecedentu je vztah konjunkce, mezi atomy v konsekventu je vztah disjunkce. Je to přepis zobecněných Hornových klauzulí definovaných na str. 47 vzorcem 6.4. Protože podle vzorce 6.5 jsou množiny antecedentu a konsekventu jednoznačně odděleny, je zvykem zapisovat klauzule bez množinových závorek, tedy vzorec bude p1 , p2 , . . . , pn |
{z
→
}
q1 , q2 , . . . , qm |
antecedent(A)
{z
(6.6)
}
konsekvent(K)
Formy klauzulí: p 1 , p 2 , . . . p n → q1 , q2 , . . . qm → q1 , q2 , . . . qm p1 , p2 , . . . pn →
(6.7) (6.8) (6.9)
(6.7): základní forma, (6.8): A = ∅ ⇒ FAKT, pravdivost tvrzení v konsekventu není ničím podmíněna, (6.9): K = ∅ ⇒ NEPLATNÉ tvrzení, neexistuje nic, co by z předpokladů vyplývalo, je to tedy sporná množina.
6.2.2
Univerzální tvrzení
Pod pojmem univerzální tvrzení rozumíme taková tvrzení, kde by v přepisu do predikátové logiky všechny proměnné byly vázány univerzálně, a tedy nevyskytují se zde žádné existenční konstanty ani existenční funktory. Přepis z predikátové do klauzulární logiky je ukázán na následujících příkladech. 49
Příklad 6.1: V přirozeném jazyce:
V létě mají všichni školáci prázdniny.
V predikátové logice:
∀x (rocni obdobi(leto) &skolak(x)) → ma(x, prazdniny))
V klauzulární logice:
rocni obdobi(leto), skolak(X)) → ma(X, prazdniny)
Příklad 6.2: Převeďte z přirozeného jazyka do klauzulární logiky následující věty: 1. 2. 3. 4. 5.
Psi štěkají (všichni psi štěkají, každý pes štěká). V létě má listí zelenou barvu, zatímco na podzim má listí žlutou nebo červenou barvu. Stůl je tvrdý. Když je hezké počasí, děti jdou na procházku. Musím do školy, protože píšu písemku.
1. pes(X) → steka(X) 2. rocni obdobi(leto), listi(X) → barva(X, zelena) rocni obdobi(podzim), listi(X) → barva(X, zluta), barva(X, cervena) 3. stul(X) → tvrdy(X) nebo → tvrdy(stul) 4. pocasi(hezky), dite(X) → jde(X, prochazka) 5. pise(ja, pisemka) → musi do(ja, skola) nebo ja(X), pise(X, pisemka) → musi do(X, skola) Na příkladech je vidět, že obvykle stačí „předsunoutÿ kvantifikátory do prefixu formule, formuli převést do tvaru, kdy hlavní spojkou je implikace, nalevo od ní jsou konjunkce a napravo disjunkce, a pak konjunkce a disjunkce nahradit čárkami. Pokud se nedaří uspořádat konjunkce a disjunkce tak, aby odpovídaly schématu 6.6, je třeba formuli rozdělit na více formulí (viz bod 2 předchozího příkladu). Postup si lépe ukážeme v následujících kapitolách o sémantice.
6.2.3
Existenční tvrzení
Existenční tvrzení jsou tvrzení obsahující existenční termy, tedy existenční konstanty nebo existenční funktory. Ve formě formule predikátové logiky jsou tyto termy vázány existenčním kvantifikátorem. Na příkladech si ukážeme, jak se používají existenční konstanty, pak existenční funktory. 50
Příklad 6.3: → → → modry(@c) → (6.10): (6.11): (6.12): (6.13):
vlastni(jana, @neco) jde kudy(@nekdo, les) bavi(@nekdo, logika) vidi(ja, @c)
(6.10) (6.11) (6.12) (6.13)
Jana něco vlastní (existuje něco, co vlastní Jana). Někdo jde lesem. Existuje někdo, koho baví logika (někoho baví logika). Vidím něco modrého.
Příklad 6.4: Převeďte do jazyka klauzulární logiky větu „Každý zaměstnanec má svého (nějakého) nadřízenéhoÿ. Když se pokusíme větu převést jako univerzální tvrzení, dostaneme klauzuli zamestnanec(X) → nadrizeny(Y, X), což ale znamená „Každý zaměstnanec má všechny jako své nadřízenéÿ, což není dobře. Proto je jasné, že nadřízený je „vázánÿ existenčně. Když teď použijeme existenční konstantu jako v předchozím příkladu, dostaneme klauzuli zamestnanec(X) → nadrizeny(@c, X), což znamená „Existuje nadřízený všech zaměstnancůÿ neboli „Existuje někdo, kdo je nadřízený každého zaměstnanceÿ, což opět není správně. Potřebujeme, aby se nadřízený vztahoval k určitému zaměstnanci. Správně je klauzule s existenčním funktorem: zamestnanec(X) → nadrizeny(@f (X), X) Funktor @f (X) přiřazuje vždy konkrétnímu zaměstnanci konkrétního nadřízeného, to, že je existenční, znamená, že pro každý argument musí tento funktor vrátit alespoň jednu hodnotu. Jak poznat, kdy použít existenční konstantu a kdy existenční funktor? Pomůckou může být pozice existenčního kvantifikátoru v ekvivalentní formuli predikátové logiky. V našem příkladě je proměnná X vázána univerzálním kvantifikátorem (každý zaměstnanec, všichni zaměstnanci), nadřízený tohoto zaměstnance je vázán existenčním kvantifikátorem. Jestliže je v predikátové formuli nejdřív univerzální a pak existenční kvantifikátor (pro každého zaměstnance existuje nadřízený), použijeme existenční funktor, když je nejdřív existenční a pak univerzální (existuje nadřízený všech zaměstnanců), použijeme existenční konstantu. Příklad 6.5: Převeďte do jazyka klauzulární logiky následující věty: 1. Každé muzeum má nějaký bezpečnostní systém. 2. Existují bezpečnostní systémy pro muzea. 51
3. Někteří studenti nosí čepici. 4. Každý student nosí nějakou čepici. 1. 2. 3. 4.
6.3
muzeum(X) → bezpecnostni system(X, @f (X)) muzeum(X) → bezpecnostni system(X, @c) student(@s) → nosi(@s, cepice) student(X) → nosi(X, @cepice(X)), @cepice je existenční funktor přiřazující lidem čepice.
Sémantika jazyka klauzulární logiky
Definice 6.6: V klauzulární logice je sémantika dána strukturou S = (W, F, R), kde F = {F1 , F2 , . . . , Fu }, R = {R1 , R2 , . . . , Rv }. W nazýváme univerzum diskurzu, F je množina funkcí, R je množina relací. Struktura je aplikovatelná na množinu klauzulí, jestliže všechny prvky, které se vyskytují v této množině klauzulí, lze interpretovat některým z prvků struktury (tedy individuovým konstantám můžeme přiřadit některý prvek univerza diskurzu, funktorům funkci, predikátům relaci). Označme Fn množinu všech n-árních funkcí, tedy funkcí arity n, Fn ⊆ F. Denotační zobrazení D je definováno následovně: • • • • •
D(c) = c ∈ W , c je individuová konstanta, D(@c) = W , existenční konstantě přiřazujeme celé univerzum diskurzu, D(fk ) = Fk , 1 ≤ k ≤ u, každému funktoru přiřadíme funkci z množiny F, D(@f /n) = Fn , existenčnímu funktoru přiřadíme množinu všech funkcí dané arity, D(pk ) = Rk , každému predikátu přiřadíme některou relaci z množiny R.
Ohodnocení (valuace) proměnné X je zobrazení e, které každé proměnné přiřadí prvek z univerza diskurzu, tedy pro každou proměnnou X je e(X) ∈ W . Pokud ohodnotíme všechny proměnné nacházející se v nějakém termu t, potom se tento term stane bázovým termem. Pokud toto zobrazení přiřazuje svým argumentům pouze prvky univerza diskurzu struktury S, mluvíme o valuaci aplikovatelné na strukturu S. Ohodnocení (valuace) termu t je zobrazení e0 definované následovně: • e0 (c) = D(c), c je individuová konstanta, • e0 (X) = e(X), X je proměnná, • e0 (f (t1 , t2 , . . . , tn )) = F (e0 (t1 ), e0 (t2 ), . . . , e0 (tn )), kde f je funktor, jeho denotát je D(f ) = F , t1 , t2 , . . . , tn jsou termy. 52
Definice 6.7: Interpretace atomu je zobrazení I, které v dané struktuře S a pro danou valuaci e přiřadí každému atomu hodnotu true (t, 1) nebo f alse (f , 0) takto: • logické konstantě je vždy přiřazena hodnota jejího denotátu, • n-árnímu predikátu p, v jehož argumentech se nevyskytují žádné exitenční termy (ve tvaru p(t1 , t2 , . . . , tn )), je přiřazena hodnota true, pokud pro n-tici vzniklou ohodnocením e0 termů v jeho argumentech platí (e0 (t1 ), e0 (t2 ), . . . , e0 (tn )) ∈ R, kde R = D(p) (tj. relace R je denotátem predikátu p), jinak je přiřazena hodnota f alse, • n-árnímu predikátu p, v jehož argumentech se nachází existenční term @t (predikát ve tvaru p(t1 , . . . , @t, . . . , tn )), je přiřazena hodnota true, pokud se v denotátu existenčního termu D(@t) nachází prvek t0 , po jehož dosazení do argumentů predikátu místo existenčního termu platí (e0 (t1 ), . . . , e0 (t0 ), . . . , e0 (tn )) ∈ R, kde R = D(p), jinak je přiřazena hodnota f alse. Atom je splnitelný (pravdivý) ve struktuře S při ohodnocení e, jestliže v této struktuře a ohodnocení interpretován hodnotou true. Zapisujeme I(p)[S, e] = true. Fakt, že atom p je interpretován hodnotou true ve struktuře S (při jakémkoliv ohodnocení), zapisujeme I(p)[S] = true. Definice 6.8: Klauzule je nepravdivá ve struktuře S při ohodnocení e, jestliže v tomto ohodnocení je její antecedent pravdivý a konsekvent nepravdivý, tedy když jsou všechny atomy antecedentu interpretovány jako true a všechny atomy konsekventu jako f alse. V opačném případě je klauzule pravdivá ve struktuře.
A K 0 0 0 1 1 0 1 1
A→K 1 1 0 1
Poznámka: Tato definice je pouhým přepisem pravdivosti formule v predikátové logice. To zjistíme, když si uvědomíme způsob interpretace formule s logickou spojkou implikace, konjunkce nebo disjunkce. Z definice vyplývá, že klauzule je pravdivá v dané struktuře a ohodnocení, pokud je alespoň jeden atom v antecedentu nepravdivý nebo alespoň jeden atom v konsekventu pravdivý. Definice 6.9: Klauzule je platná (splněna) ve struktuře S, když je splnitelná pro jakoukoliv valuaci aplikovatelnou ve struktuře S. Jestliže klauzule není splnitelná v žádné valuaci aplikovatelné v dané struktuře, pak je nesplnitelná (není platná) v dané struktuře. Klauzule je logicky platná (logický zákon), jestliže je platná v jakékoliv struktuře. Příklad 6.6: Chceme interpretovat klauzuli C = p(X), q(X, a) → r(X, f (b)), r(X, c). Pro interpretaci použijeme postupně strukturu S1 . S1 = (W1 , F1 , R1 ), kde W1 = {listi, zluta, hneda, zelena, modra, kuratko, jasan, dub, buk}, F1 = {barva/1}, R1 = {strom/1, ma/2, barva listi/2}, barva(kuratko) = zluta, barva(nebe) = modra, barva(zeme) = hneda, 53
strom/1 = {(jasan), (dub), (buk)}, ma/2 = {(jasan, listi), (buk, listi)}, barva listi = {(jasan, zluta), (dub, hneda), (buk, zelena)} D(a) = listi, D(b) = kuratko, D(c) = modra, D(f ) = barva, D(p) = strom, D(q) = ma, D(r) = barva listi Uplatníme denotační zobrazení D na atomy v klauzuli: strom(X), ma(X, listi) → barva listi(X, barva(kuratko)), barva listi(X, modra) Funkce barva má konstantní argument, proto tuto funkci můžeme vyhodnotit: strom(X), ma(X, listi) → barva listi(X, zluta), barva listi(X, modra) Interpretujeme se zvolenou valuací e1 (X) = jasan: I(strom(jasan))[S1 , e1 ] = true I(ma(jasan, listi))[S1 , e1 ] = true I(barva listi(jasan, zluta))[S1 , e1 ] = true I(barva listi(jasan, modra))[S1 , e1 ] = f alse I(C)[S1 , e1 ] = I(true, true → true, f alse) = true Pro valuaci e2 (X) = buk je I(C)[S1 , e2 ] = f alse. Příklad 6.7: Při interpretaci téže klauzule nyní použijeme strukturu S2 : S2 = (W2 , F2 , R2 ), kde W2 = {skola, index, sesit, student, kladivko, jana, pepa, karel}, F2 = {prukaz/1}, R2 = {je student/1, jde do/2, ma/2}, prukaz(student) = index, je student/1 = {(pepa), (jana)}, jde do/2 = {(pepa, skola), (jana, kino), (karel, skola)}, ma/2 = {(pepa, sesit), (jana, index), (karel, kladivko)} D(a) = skola, D(b) = student, D(c) = sesit, D(f ) = prukaz, D(p) = je student, D(q) = jde do, D(r) = ma Uplatníme denotační zobrazení D na atomy v klauzuli: je student(X), jde do(X, skola) → ma(X, prukaz(student)), ma(X, sesit) Po vyhodnocení funkce prukaz: je student(X), jde do(X, skola) → ma(X, index), ma(X, sesit) Interpretujeme se zvolenou valuací e3 (X) = pepa: I(je student(pepa))[S2 , e3 ] = true I(jde do(pepa, skola))[S2 , e3 ] = true I(ma(pepa, index))[S2 , e3 ] = f alse I(ma(pepa, sesit))[S2 , e3 ] = true 54
I(C)[S2 , e3 ] = I(true, true → f alse, true) = true Narozdíl od struktury S1 , ve struktuře S2 je formule C interpretována vždy jako true, proto můžeme psát I(C)[S2 ] = true.
6.4
Vlastnosti klauzulí
6.4.1
Prázdná množina antecedentu nebo konsekventu
Antecedent i konsekvent jsou množiny, a množiny mohou být také prázdné. Klauzuli pak interpretujeme následovně: 1. {} → {q1 , q2 , . . . , qm } (antecedent je prázdná množina): protože mezi atomy v antecedentu je vztah konjunkce, pravdivostní hodnota klauzule se nezmění, když do antecedentu přidáme atom true. V případě prázdné množiny antecedentu proto interpretujeme formuli {true} → {q1 , q2 , . . . , qm }. Klauzuli s prázdnou množinou antecedentu nazýváme FAKT. Pokud je klauzule v dané struktuře a ohodnocení považována za splnitelnou, je splnitelná i disjunkce atomů v konsekventu. 2. {p1 , p2 , . . . , pn } → {} (konsekvent je prázdná množina): protože mezi atomy v konsekventu je vztah disjunkce, pravdivostní hodnota klauzule se nezmění, když do konsekventu přidáme atom f alse. V případě prázdné množiny konsekventu proto interpretujeme formuli {p1 , p2 , . . . , pn } → {f alse}. Jestliže je klauzule v dané struktuře a ohodnocení považována za splnitelnou, je konjunkce atomů v antecedentu nesplnitelná, tedy alespoň jeden atom je interpretován jako f alse. Toho se využívá k reprezentaci negace atomů. 3. {} → {} (antecedent i konsekvent jsou prázdná množina, nazýváme prázdná klauzule): interpretujeme klauzuli {true} → {f alse}, která podle definice implikace je vždy interpretována jako f alse, tedy jde o nesplnitelnou klauzuli. Toho využíváme při důkazu sporem (dokazovaný závěr znegujeme a odvozováním se snažíme získat prázdnou klauzuli). Příklad 6.8: → kulaty(zeme) (Země je kulatá.) → pocet nohou(clovek, 2), pocet nohou(clovek, 4) (Člověk má dvě nebo čtyři nohy.) barva(pisek, f ialova) → (Písek není fialový.) 55
vrah(zahradnik), vrah(domovnik) → (Buď zahradník není vrah nebo domovník není vrah (nebo žádný z nich není vrah).)
6.4.2
Konjunkce a disjunkce atomů v klauzuli
Vycházíme z obecného tvaru klauzule klauzulární logiky p1 , p2 , . . . , pn → q1 , q2 , . . . , qm , která je do predikátové logiky překládána na formuli p1 &p2 & . . . &pn → q1 ∨ q2 ∨ . . . ∨ qm s univerzálním vázáním proměnných. Konjunkce v antecedentu je tam, kde má být, takže ji není třeba řešit. Atomy spojené konjunkcemi prostě oddělíme čárkou. Příklad 6.9: Když to má pruhy a kopyta, je to zebra. ma(X, pruhy), ma(X, kopyta) → zebra(X) Disjunkci v antecedentu, tedy formuli F1 ∨ F2 → K, řešíme podle věty Věta 6.1: (F1 ∨ F2 → K) ⇔ ((F1 → K) &(F2 → K)) Důkaz:
(6.14)
lze provést například sémantickým tablem, je triviální.
2
V množině klauzulí je mezi klauzulemi stav konjunkce, proto je tento přepis použitelný. Znamená to, že vytvoříme dvě klauzule, které budou mít stejný konsekvent, a antecedent se do klauzulí rozdělí v místě disjunkce. Atomů spojených disjunkcí může být v antecedentu jakýkoliv počet, pak samozřejmě vytvoříme tolik klauzulí, kolik je atomů antecedentu spojených disjunkcemi. Příklad 6.10: Kdo nosí index nebo skripta, je student. nosi(X, index) → student(X) nosi(X, skripta) → student(X) Konjunkce v konsekventu nemá co dělat, proto formuli A → F1 &F2 řešíme podle věty Věta 6.2: (A → F1 &F2 ) ⇔ ((A → F1 ) &(A → F2 )) Důkaz:
lze opět provést například sémantickým tablem.
(6.15) 2
Stejně jako v případě disjunkce v antecedentu, i zde vytvoříme tolik klauzulí, kolik je atomů v konsekventu spojených konjunkcí, všechny klauzule budou mít stejný antecedent. Příklad 6.11: Kočky mají ostré zuby, ostré drápy a dobrý zrak. kocka(X) → ma(X, ostre zuby) kocka(X) → ma(X, ostre drapy) kocka(X) → vidi(X, dobre) 56
Disjunkce v konsekventu je tam, kde má být, proto ji pouze nahradíme čárkami: Příklad 6.12: Kdo je v nemocnici, je buď nemocný nebo přišel někoho navštívit. nemocnice(N ), je kde(X, N ) → nemocny(X), navstivil(X, @f (X))
6.4.3
Negace atomů
Jestliže chceme v klauzuli použít negativní literál pro bázový atom, nemůžeme použít atom s negací (protože symbol negace nepatří do syntaxe jazyka klauzulární logiky), ale použijeme jednu z následujících formulí: Věta 6.3: p &¬q → r ⇔ p → q ∨ r p → ¬q ∨ r ⇔ p &q → r
(6.16) (6.17)
Důkaz: Logická platnost těchto formulí je snadno dokazatelná například Quinovým algoritmem nebo sémantickým tablem. 2 To znamená, že v případě bázových atomů (bez existenčních termů a proměnných!!!) stačí odstranit negaci a převést atom na opačnou stranu implikace. Příklad 6.13: Když nefouká vítr, drak spadne. (podle 6.16) → pocasi(vitr), pozice(drak, pada) V neděli bratr nejde do školy. (podle 6.17) den v tydnu(nedele), jde(bratr, skola) → Když na mě zaútočí medvěd a nemám zbraň, neutíkám. (podle 6.16 a 6.17) utok(medved, ja), utika(ja) → ma(ja, zbran) V případě atomů s proměnnými a existenčními konstantami vycházíme opět z predikátové logiky, především z DeMorganových zákonů: ∃c(¬A) ⇔ ¬(∀cA) ∀x(¬A) ⇔ ¬(∃xA) ∀x(p(x) → ¬(∃u q(x, u))) ⇔ ∀x∀u(p(x) → ¬q(x, u))
(6.18) (6.19) (6.20)
Tedy podle (6.18) negujeme atom s existenční konstantou tak, že existenční konstantu nahradíme novou proměnnou a pak stejně jako bázový atom převedeme na druhou stranu implikace. Podle (6.19) negujeme atom s proměnnou tak, že tuto proměnnou nahradíme novou existenční konstantou a převedeme na druhou stranu implikace. 57
Podle příkladu ve vztahu (6.20) řešíme negaci atomu, kde se popření týká existenčního funktoru. Atom převedeme na druhou stranu implikace a existenční funktor nahradíme proměnnou. Poznámka: Negace atomu, který obsahuje proměnné nebo existenční termy, je věc ošidná. Musíme především vědět, co chceme negací říci, protože nemusí být jednoznačná. V predikátové logice to můžeme demonstrovat na příkladu, kdy se před předikátem s více proměnnými nachází několik kvantifikátorů (na různých úrovních – v různých vzdálenostech od predikátu, třeba až před celou formulí) a my negaci umístíme někam mezi ně (například mezi druhý a třetí kvantifikátor). Pak se negace projeví pouze na proměnných vázaných kvantifikátory, které jsou až za negací. Proto když si nejsme jisti, zda máme při negaci zaměnit proměnné a existenční termy, můžeme si pomoci přepisem do predikátové logiky. Příklad 6.14: Vyjádřete klauzulemi tyto věty: 1. Někdo nemá jedničku z logiky. (negujeme atom ve větě Všichni mají jedničku z logiky.) 2. Nikdo nemá jedničku z logiky. (negujeme ve větě Někdo má jedničku z logiky.) 3. Nikdo v neděli nechodí do školy. 4. Rostliny, které nejsou byliny ani keře, jsou stromy. 5. Pro každého zaměstnance existuje nadřízený, který není jeho. (negujeme ve větě Každý zaměstnanec má svého nadřízeného.), také znamená Když je někdo zaměstnanec, pak není pravda, že všichni jsou jeho nadřízení. 1. predikátová logika: ¬(∀c znamka(c, logika, 1)) ⇔ ∃c ¬znamka(c, logika, 1) klauzulární logika: znamka(@c, logika, 1) → 2. predikátová logika: ¬(∃x znamka(x, logika, 1)) ⇔ ∀x ¬znamka(x, logika, 1) klauzulární logika: znamka(X, logika, 1) → 3. den v tydnu(nedele), jde(X, skola) → 4. rostlina(X) → bylina(X), ker(X), strom(X) 5. zamestnanec(X), nadrizeny(Y, X) →
6.4.4
Negace klauzule
Když chceme popřít klauzuli, použijeme již dříve naznačené postupy pro řešení konjunkcí a disjunkcí atomů a negace atomu. Označme A antecedent, K konsekvent, A = p1 &p2 & . . . &pn , K = q1 ∨ q2 ∨ . . . ∨ qm .
58
Pak platí tato posloupnost ekvivalencí:
¬(A → K)
⇔
(A &¬K)
⇔
→ A → ¬K
⇔
q1 q2 qm
→ p1 → p2 ... → pn → → ... →
(6.21)
Znamená to, že všechny atomy negujeme do důsledků (všechny proměnné zaměníme za existenční konstanty atd.) s přehozením na druhou stranu implikace a osamostatníme do jednotlivých klauzulí. Množina výsledných klauzulí se nazývá popírající množina původní klauzule. Příklad 6.15: Vyjádřete negace těchto vět (klauzulí): 1. věta: Každé vadné zboží je reklamováno. klauzule: zbozi(X), vadny(X) → reklamace(X) negovaná klauzule: → zbozi(@c) → vadny(@c) reklamace(@c) → negovaná věta: Některé vadné zboží není reklamováno. 2. věta: Některé hračky mají rády všechny děti. klauzule: dite(X), hracka(@h) → rad(X, @h) predikátová logika: ¬(∃h∀d(dite(d) &hracka(h) → rad(d, h)) ⇔ ∀h∃d(dite(d) &hracka(h) &¬rad(d, h)) negovaná klauzule: → dite(@f (Y )) → hracka(Y ) rad(@f (Y ), Y ) negovaná věta: Pro každou hračku existuje dítě, které ji nemá rádo. Negace druhé věty je zároveň ukázkou toho, jak postupujeme při přepisu do klauzulární logiky při negaci formule s posloupností kvantifikátorů odpovídající existenčnímu funktoru.
6.4.5
Predikát rovnosti
Predikát rovnosti pracuje jako jakýkoliv jiný predikát – vrací hodnotu true nebo f alse. Jestliže jsou jeho oba argumenty shodné, je výsledek true, jinak f alse. Rozdíl oproti jiným predikátům je ve způsobu zápisu. Zatímco predikáty obecně se zapisují postfixově (nejdřív 59
název, pak argumenty), většina logických programovacích jazyků umožňuje používat predikát rovnosti (i nerovnosti a relačních operátorů <, >) v infixovém zápisu. U predikátu rovnosti je třeba dávat pozor především na to, aby byl v případě funktorů použit jen pro případy testování jednoznačného přiřazení. Příklad 6.16: Vyjádřete klauzulemi uvedené věty. 1. Slepic je 25. → pocet(slepice) = 20 2. Barva zralých jahod je červená. jahoda(X), zraly(X) → barva(X) = cervena nebo jahoda(X), zraly(X) → barva(X, cervena) nebo X = jahoda, zraly(X) → barva(X) = cervena 3. Kuchařka potřebuje vařechu. kucharka(X) → potrebuje(X, varecha) nebo X = kucharka → potrebuje(X, varecha) ŠPATNĚ: kucharka(X) → potrebuje(X) = varecha (protože kuchařka potřebuje i jiné věci než vařechu) 4. Pes má uši. pes(X) → ma(X, usi) nebo X = pes → ma(X, usi) ŠPATNĚ: pes(X) → ma(X) = usi (pes má taky oči, čumák, ocásek, . . . ) V příkladu je většina vět přepsána několika způsoby. Pokaždé jsou použity buď predikáty nebo funktory s různou aritou. Vhodný způsob volíme tak, abychom ve všech klauzulích používali predikáty a funktory stejné arity a se stejným významem argumentů. Například pokud v případě 2 použijeme název barva pro funktor s jedním argumentem vracející barvu svého argumentu, nemůžeme v jiné klauzuli použít tento název pro predikát.
6.4.6
Substituce
V klauzulích se obvykle nacházejí proměnné a exitenční termy. Při používání těchto klauzulí pro účely odvozování důsledků budeme chtít s těmito prvky dále pracovat, a to se dělá pomocí substituce. Definice 6.10: Substituce termů t1 , t2 , . . . , tn za proměnné X1 , X2 , . . . , Xn do klauzule C, kde každý term ti je substituovatelný za proměnnou Xi , 1 ≤ i ≤ n, je dána množinou ϕ = {t1 /X1 , t2 /X2 , . . . , tn /Xn }, značíme C[ϕ]. Substituce je tedy definována prakticky stejně jako v predikátové logice, za proměnnou dosazujeme term, který může být funktor, existenční term nebo opět proměnná. 60
Definice 6.11: Existenční substituce dosud nepoužitého existenčního termu @m za bázový term t se zapisuje ϕ = (@m/t; k1 , k2 , . . . , kr ), a znamená nahrazení k1 ., k2 ., . . . a kr . výskytu termu t existenčním termem @m v dané klauzuli. Narozdíl od klasické substituce v existenční substituci nahrazujeme individuové konstanty a nikoliv proměnné, navíc můžeme substituci omezit pouze na některé výskyty konstanty, nemusíme nutně nahrazovat všechny výskyty konstanty v klauzuli. Umožňuje nám to fakt, že když je v některém parametru dosazena konstanta, znamená to, že nějaká vyhovující hodnota pro tento parametr určitě existuje (je to vlastně ta konstanta), proto lze tvrzení zobecnit na existenční term. Příklad 6.17: Na dané klauzule proveďte uvedené substituce: 1. C1 = p(a, X), q(f (X), b, Z) → q(f (a), g(b, a), Y ) ϕ1 = {a/X, g(a, Z)/Y, Z/Z} C1 [ϕ1 ] = p(a, a), q(f (a), b, Z) → q(f (a), g(b, a), g(a, Z)) ϕ2 = (@c/a; 1, 3) C1 [ϕ2 ] = p(@c, X), q(f (X), b, Z) → q(f (a), g(b, @c), Y ) C1 [ϕ1 ][ϕ2 ] = p(@c, a), q(f (@c), b, Z) → q(f (a), g(b, a), g(a, Z)) 2. C2 = dum(@f (Y )), vlastni(@f (Y ), Y ) → ma(Y, bydliste) (Kdo vlastní nějaký dům, má kde bydlet.) ϕ3 = {X/X, pavel/Y } C2 [ϕ3 ] = dum(@f (pavel)), vlastni(@f (pavel), pavel) → ma(pavel, bydliste) (Jestliže Pavel vlastní nějaký dům, má kde bydlet.) ϕ4 = (@c/pavel; 4) C2 [ϕ3 ][ϕ4 ] = dum(@f (pavel)), vlastni(@f (pavel), pavel) → ma(@c, bydliste) (Pokud Pavel vlastní nějaký dům, někdo má kde bydlet.) 3. C3 = clovek(X) → umi(X, zpivat), hraje na(X, @nastroj(X)) (Každý člověk umí zpívat nebo hrát na nějaký hudební nástroj.) ϕ5 = {ucitel(X, hudebni v)/X} C3 [ϕ5 ] = clovek(ucitel(X, hudebni v)) → umi(ucitel(X, hudebni v), zpivat), hraje na(ucitel(X, hudebni v), @nastroj(ucitel(X, hudebni v))) (Pro každého člověka, který je něčí učitel v předmětu Hudební výchova, platí, že buď umí zpívat nebo hraje na nějaký hudební nástroj.) ϕ6 = {honza/X} C3 [ϕ5 ][ϕ6 ] = clovek(ucitel(honza, hudebni v)) → umi(ucitel(honza, hudebni v), zpivat), hraje na(ucitel(honza, hudebni v), @nastroj(ucitel(honza, hudebni v))) (Každý člověk, kdo je Honzův učitel v předmětu Hudební výchova, buď umí zpívat nebo hraje na nějaký hudební nástroj.) 61
ϕ7 = (@c/ucitel(honza, hudebni v); 1 − 4) C3 [ϕ5 ][ϕ6 ] = clovek(@c) → umi(@c, zpivat), hraje na(@c, @nastroj(@c)) (Existuje člověk, který umí zpívat nebo hraje na nějaký hudební nástroj.) Poznámka: Jestliže máme jistotu, že při interpretaci bude vždy použita neprázdná množina univerza diskurzu, můžeme uplatnit existenční substituci také na termy, ve kterých se vyskytují proměnné (takový funktor však nesmí obsahovat jako argumenty žádné existenční termy, opravdu pouze proměnné!). Za proměnnou dokonce lze dokonce v takovém případě dosadit i takovou existenční konstantu, která se již v bázi vyskytuje (když to platí pro všechny a alespoň někdo existuje, pak můžeme dosadit kohokoliv, kdo existuje). Existenční substituci provádíme tehdy, když nám ulehčí navržení klauzule nebo během odvozování důsledku klauzulí, pokud ve výsledné klauzuli má být existenční term.
6.5
Vztahy mezi klauzulemi
Pro logické programování budeme potřebovat možnost odvozování závěru, proto si definujeme odvozovací pravidlo a ukážeme si způsob jak toto pravidlo použít.
6.5.1
Odvození důsledku dvojice klauzulí
V klauzulární logice používáme rezoluční odvozovací pravidlo, které lze odvodit z rezolučního odvozovacího pravidla predikátové logiky. Předpis pravidla je následující: A1 , p → K1 ,
A2 → p, K2
`
A1 , A2 → K1 , K2
(6.22)
Znamená to, že ve dvojici klauzulí najdeme tentýž atom (stejný včetně argumentů) p, a to v jedné klauzuli v antecedentu, v druhé v konsekventu, a výslednou klauzuli utvoříme z antecedentů a konsekventů obou klauzulí s vyjímkou „spojovacíhoÿ společného atomu p. Tento atom „odříznemeÿ, proto se toto pravidlo také nazývá odvozovací pravidlo rezolučního řezu. Odvození z rezolučního pravidla predikátové logiky je následující: C ∨ ¬p, (¬A1 ∨ K1 ) ∨ ¬p, ¬A1 ∨ ¬p ∨ K1 , A1 &p → K1 ,
p∨D p ∨ (¬A2 ∨ K2 ) ¬A2 ∨ p ∨ K2 A2 → p ∨ K2
|= |= |= |=
C (¬A1 ∨ K1 ) ¬A1 ∨ ¬A2 A1 &A2
∨ ∨ ∨ →
D (¬A2 ∨ K2 ) K1 ∨ K2 K1 ∨ K2
Všechny zde použité operace vycházejí z ekvivalentních úprav pro formule predikátové logiky, je zde také použita substituce (pro C a D). 62
Příklad 6.18: Z uvedených klauzulí se pokusíme vyvodit závěr Monika je matkou Honzy., a to tak, že pravidlo rezoluce uplatníme nejdřív na první a druhou klauzuli, pak na výsledek a třetí klauzuli. 1. otec(pavel, honza), manzele(pavel, monika) → matka(monika, honza) 2. → otec(pavel, honza) 3. → manzele(pavel, monika) 4. manzele(pavel, monika) → matka(monika, honza) 5. → matka(monika, honza)
R(1,2) R(3,4)
Při prvním použití pravidla rezoluce je p = otec(pavel, honza), při druhém použití je p = manzele(pavel, monika).
6.5.2
Unifikace klauzulí
Rezoluční odvození můžeme použít jen tehdy, pokud dvojice atomů, které chceme vyříznout, je absolutně stejná (včetně parametrů). Pokud jsou parametry individuové konstanty, není problém. Jestliže jsou parametry proměnné nebo existenční konstanty a my ještě nechceme provést bázovou substituci zvlášť pro každou z klauzulí, musíme počítat s tím, že obecně v různých klauzulích se jedná o různé termy, i když jsou stejně pojmenované. Jak to řešit: 1. pokud je to nutné, přejmenujeme v jedné klauzuli proměnné a existenční konstanty, které mají v obou klauzulích stejné názvy, 2. najdeme vhodnou substituci, kterou lze použít na obě klauzule, 3. aplikujeme tuto substituci, 4. provedeme rezoluční odvození. Substituce vhodná pro obě klauzule, po jejíž aplikaci lze použít rezoluční odvození (tj. mají stejný atom, jedna v antecedentu, druhá v konsekventu) se nazývá unifikátor . Pro jednu dvojici klauzulí může existovat více různých unifikátorů. Pokud unifikátor zvolíme nevhodně, lze sice rezoluční řez provést, ale výsledná klauzule může být pro další odvozování nevhodná (např. dosadíme konstantu někam, kam bychom potřebovali později dosazovat za proměnnou). Unifikátor ϕ je obecnější než unifikátor σ, pokud σ lze dostat tak, že na klauzuli po aplikaci ϕ uplatníme ještě nějakou další substituci – unifikaci (tj. čím méně konstant – konkrétních hodnot, tím obecnější). 63
Definice 6.12: Nechť σ a ϕ jsou unifikátory dvojice klauzulí. ϕ je obecnější než σ, jestliže existuje substituce λ taková, že platí ϕ ◦ λ = σ, tedy je možno σ odvodit z ϕ. ϕ je nejobecnější unifikátor, jestliže pro každý unifikátor γ existuje substituce λ taková, že platí ϕ ◦ λ = γ – jakýkoliv unifikátor pro stejnou dvojici klauzulí je možno odvodit z ϕ. Z hlediska dalšího odvozování je samozřejmě nejvýhodnější použít nejobecnější unifikátor. Algoritmus pro zjištění nejobecnějšího unifikátoru: 1) Vytvoříme množinu neshod Z obou klauzulí, které chceme unifikovat, vezmeme atomy, přes které má být provedeno rezoluční odvození: p(t1 , t2 , . . . , tn ), p(r1 , r2 , . . . , rn ), a vytvoříme z nich rovnice: t1 = r1 t2 = r2 ... tn = rn 2) Následující body algoritmu provádíme na tuto množinu neshod tak dlouho, dokud rovnice nejsou ve tvaru Proměnná=výraz, kde – Proměnná se nevyskytuje na pravé straně žádné rovnice množiny, – pro každou Proměnnou je zde nejvýše jeden výraz. Nejobecnější unifikátor je pak ϕ = {vyraz1 /P rom1 , vyraz2 /P rom2 , . . . , vyrazk /P romk }. Opakujeme následující kroky: 1. Vyřadíme rovnice, které mají stejnou levou a pravou stranu (např. X = X nebo f (a, Y ) = f (a, Y )). 2. Rovnice ve tvaru výraz=Proměnná nahradíme rovnicemi Proměnná=výraz (přehodíme Proměnnou doleva). 3. Rovnice ve tvaru t1 = t2 , kde t1 a t2 nejsou proměnné: (a) jsou to různé funkční symboly (např. f (X) = g(Y )) ⇒ KONEC, množina neshod nemá řešení. (b) jinak: tuto rovnici nahradíme množinou neshod pro tyto termy. Např. p(X, a) = p(f (Y, b), Y ) nahradíme rovnicemi X = f (Y, b), a = Y . 4. Rovnice ve tvaru Proměnná=t, t je jakýkoliv term: (a) jestliže se Proměnná vyskytuje v t (např. jako parametr funktoru) ⇒ KONEC, množina neshod nemá řešení. (b) jinak všechny výskyty Proměnné v ostatních rovnicích nahradíme termem t, samotnou rovnici neměníme. 64
Příklad 6.19: Unifikujte dvojici klauzulí: C1 = p(g(Y ), f (X, h(X), Y )), r(Y, h(Y )) → m(X, Y ) C2 = r(a, h(Z)) → p(M, f (g(Z), W, Z)) Rezoluční odvození bude provedeno přes predikát p. Množina neshod: g(Y ) = M f (X, h(X), Y ) = f (g(Z), W, Z) Na množinu neshod budeme rekurzívně uplatňovat výše uvedený algoritmus. 1) g(Y ) = M f (X, h(X), Y ) = f (g(Z), W, Z) 2) M = g(Y ) X = g(Z) h(X) = W Y =Z
podle bodu 2 algoritmu podle bodu 3 podle bodu 3 podle bodu 3
3) M = g(Z) X = g(Z) W = h(X) Y =Z
podle bodu 4 na Y = Z
4) M = g(Z) X = g(Z) W = h(g(Z)) Y =Z
podle bodu 2
podle bodu 4
ϕ = {g(Z)/X, Z/Y, Z/Z, g(Z)/M, h(g(Z))/W } C1 [ϕ] = p(g(Z), f (g(Z), h(g(Z)), Z)), r(Z, h(Z)) → m(g(Z), Z) C2 [ϕ] = r(a, h(Z)) → p(g(Z), f (g(Z), h(g(Z)), Z)) Po uplatnění rezolučního odvozovacího pravidla dostaneme klauzuli C = r(Z, h(Z)), r(a, h(Z)) → m(g(Z), Z) Poznámka: V některých případech lze pro unifikaci použít existenční substituci. Musíme však brát v úvahu to, že při substituci musíme vždy použít nový (v bázi dosud nepoužitý) existenční term (obvykle existenční konstantu). Ve skutečnosti lze použít i takovou existenční konstantu, která již v bázi je (i v téže klauzuli), ale pouze tehdy, když je univerzum diskurzu neprázdná množina a nahrazujeme proměnnou (tj. jestliže klauzule platí pro každý prvek a alespoň jeden prvek existuje, pak 65
platí i pro tento existující prvek). V následujících příkladech je ukázáno, kdy dvojice klauzulí není a kdy je unifikovatelná pomocí existenční substituce. Příklad 6.20: 1. rozbije(f erda, okno) → provede(otec(f erda), zaskleni(okno)) (Když Ferda rozbije okno, Ferdův otec zařídí zasklení tohoto okna.) 2. → rozbije(@c, okno) (Někdo rozbil okno.) 3. rozbije(@d, okno) → provede(otec(@d), zaskleni(okno)) . . . při substituci jsme museli použít dosud nepoužitou existenční konstantu ⇒ klauzule jsou neunifikovatelné. Příklad 6.21: 1. rozbije(X, okno) → provede(otec(X), zaskleni(okno)) (Když někdo rozbije okno, jeho otec zařídí zasklení tohoto okna.) 2. → rozbije(f erda, okno) (Ferda rozbil okno.) 3. rozbije(@c, okno) → provede(otec(@c), zaskleni(okno)) 4. → rozbije(@c, okno) Vidíme, že druhou dvojici klauzulí se podařilo unifikovat tak, že lze použít rezoluční pravidlo (v univerzu diskurzu je například konstanta f erda). Tento příklad je zároveň ukázkou toho, jak je důležité volit klauzule a substituce tak, aby byly co nejobecnější.
6.5.3
Znalostní báze
Definice 6.13: Znalostní báze je neprázdná množina klauzulí jazyka klauzulární logiky, tyto klauzule nazýváme speciální axiomy báze (předpoklady důkazu). Mezi klauzulemi báze je vztah konjunkce. Báze pro nás bude množina tvrzení o uzavřeném modelovaném světě. To, že je modelovaný svět uzavřený, znamená, že při odvozování budeme brát v úvahu pouze obsah báze, co v ní nebude, to se neobjeví ani v odvozovaných závěrech (jako by to neexistovalo). Poznámka:
Znalostní bázi si můžeme představit jako formuli (A1 → K1 )
& (A2 → K2 )
&
...
& (Ar → Kr )
(6.23)
Znalostní báze nám především slouží v logickém programování ke stanovení prostředí, ve kterém chceme odvozovat a zjišťovat odpovědi na otázky, je to jakási množina předpokladů důkazu. Je to obdoba báze znalostních systémů, které pracují na podobném principu. 66
Bázi vytvoříme takto: 1. 2. 3. 4.
zavedeme vhodné predikáty, zavedeme vztahy mezi predikáty, tedy vytvoříme klauzule, přidáme fakty o konkrétní situaci podle interpretační struktury, můžeme začít testovat pravdivost některé klauzule.
Ve znalostní bázi se budou nacházet dva druhy klauzulí: pravidla a fakty. Pravidla nám říkají, co platí, když platí určité předpoklady, jsou to takové klauzule, se kterými jsme až dosud pracovali. Obvykle obsahují proměnné nebo existenční termy (nebo obojí). Fakty o konkrétní situaci jsou klauzule reprezentující funkce a relace struktury a valuaci, vztahují se tedy k interpretaci klauzulí. Postupujeme takto: X1 a11 a21 ...
X2 a12 a22 ...
... ... ... ...
Xn a1n a2n ...
f (X1 , X2 , . . . , Xn ) b1 b2 ...
Tabulka 6.1: Funkce ze struktury pro interpretaci klauzulí V případě přepisu funkce použijeme predikát rovnosti, obecně pro funkci s předpisem f : (X1 , X2 , . . . , Xn ) −→ Y , danou tabulkou 6.1 vytvoříme množinu klauzulí → f (a11 , a12 , . . . , a1n ) = b1 → f (a21 , a22 , . . . , a2n ) = b2 ... Předpokladem je, že n-tice (ai1 , ai2 , . . . , ai,n ) z řádků tabulky funkce jsou vždy po dvou různé. Pokud tento předpoklad není splněn, musíme vytvořit novou relaci (arity n + 1), kterou použijeme pro definování faktů a vhodně upravíme klauzule báze. R:
X1 a11 a21 ...
X2 a12 a22 ...
... ... ... ...
Xn a1n a2n ...
Tabulka 6.2: Relace ze struktury pro interpretaci klauzulí Při přepisu relace jednoduše dosadíme do argumentů příslušného predikátu všechny řádky relace a z každého takového atomu vytvoříme jednu klauzuli. Pro relaci R z tabulky 6.2 vzniknou klauzule
67
→ R(a11 , a12 , . . . , a1n ) → R(a21 , a22 , . . . , a2n ) ... Tento postup lze použít také pro přepis valuace (ohodnocení) proměnných, ale pouze tehdy, když stejně pojmenované proměnné v různých klauzulích jsou považovány za tytéž proměnné. Většina logických programovacích jazyků však takové proměnné obecně považuje za různé, o tutéž proměnnou jde pouze v rámci jedné klauzule. Příklad 6.22: Vytvořte znalostní bázi obsahující klauzule podle následujících vět a v této bázi odvoďte odpověď na otázku „Má Hanička dobrou náladu?ÿ • O vánocích děti zpívají všechny (známé) koledy. • Kdo zpívá radostnou písničku, má dobrou náladu, kdo zpívá smutnou písničku, je smutný. • Někdo není smutný. • Dětské písničky jsou radostné, a taky všechny písničky, které jsou stejného typu jako „Nesem vám novinyÿ, jsou radostné. • Jsou vánoce. • Hanička je dítě. • Písnička „Nesem vám novinyÿ je koleda. Navrhneme predikáty a funktory, sestavíme bázi a odvodíme potřebnou klauzuli: doba(< jaka >) typ pisne(< nazev pisne >, < typ >) pisnicka(< nazev pisne >, < nalada pisne >) dite(< jmeno >) nalada(< kdo >, < jaka >) zpiva(< kdo >, < co >) 1. 2. 3. 4. 5. 6. 7. 8. 9.
doba(vanoce), dite(X), typ pisne(Y, koleda) → zpiva(X, Y ) zpiva(X, Y ), pisnicka(Y, radostna) → nalada(X, dobra) zpiva(X, Y ), pisnicka(Y, smutna) → nalada(X, smutna) nalada(@c, smutna) → typ pisne(X, detska) → pisnicka(X, radostna) typ pisne(nesem vam noviny, X), typ pisne(Y, X) → pisnicka(Y, radostna) → doba(vanoce) → dite(hanicka) → typ pisne(nesem vam noviny, koleda)
10. rezoluce na 1 a 7: dite(X), typ pisne(Y, koleda) → zpiva(X, Y ) 11. substituce do 10, {hanicka/X, nesem vam noviny/Y }: dite(hanicka), typ pisne(nesem vam noviny, koleda) → zpiva(hanicka, nesem vam noviny) 68
12. rezoluce na 8 a 11: typ pisne(nesem vam noviny, koleda) → zpiva(hanicka, nesem vam noviny) 13. rezoluce na 9 a 12: → zpiva(hanicka, nesem vam noviny) 14. substituce do 6, {koleda/X, nesem vam noviny/Y }: typ pisne(nesem vam noviny, koleda), typ pisne(nesem vam noviny, koleda) → pisnicka(nesem vam noviny, radostna) 15. rezoluce na 9 a 14 (dvakrát): → pisnicka(nesem vam noviny, radostna) 16. substituce do 2, {hanicka/X, nesem vam noviny/Y }: zpiva(hanicka, nesem vam noviny), pisnicka(nesem vam noviny, radostna) → nalada(hanicka, dobra) 17. rezoluce na 13 a 16: pisnicka(nesem vam noviny, radostna) → nalada(hanicka, dobra) 18. rezoluce na 15 a 17: → nalada(hanicka, dobra) Většinu pojmů souvisejících s interpretací znalostní báze (struktura, denotace, ohodnocení, atd.) jsme probrali v kapitole 6.3 na str. 52. V následujících definicích nalezneme ostatní potřebné pojmy. Definice 6.14: Struktura aplikovatelná na znalostní bázi je taková struktura, která umožňuje přiřadit každé individuové konstantě vyskytující se v klauzulích báze některý prvek univerza diskurzu struktury, každému funktoru funkci z množiny funkcí struktury a každému predikátu relaci z množiny relací struktury. Model znalostní báze je taková struktura aplikovatelná na bázi, ve níž jsou všechny klauzule báze platné. Klauzule je logickým důsledkem znalostní báze, jestliže je platná ve všech modelech této báze. V předchozím příkladu je aplikovatelná struktura přímo součástí znalostní báze. Trochu to sice komplikuje případné změny struktury a tím i interpretace, ale ulehčuje to odvozování a tento postup odpovídá metodám používaným v logickém programování.
69
Kapitola 7 Klauzulární axiomatický systém Klauzulární axiomatický systém je založen na klauzulární logice. Provádění důkazů v tomto systému odpovídá postupům používaným v logických programovacích jazycích. Narozdíl od dříve probíraného Hilbertovského axiomatického systému, zde můžeme používat jak přímé, tak i nepřímé důkazy. V této kapitole definujeme formální systém obdobně jako v kapitolách věnovaných Systému přirozené dedukce, Hilbertovskému systému a Gentzenovskému systému, ale pouze v základech. Naznačíme také důkaz korektnosti a úplnosti tohoto systému.
7.1
Definice systému
Jazyk Klauzulárního axiomatického systému přejímáme z klauzulární logiky. Logické axiomy (A) jsou takové klauzule klauzulární logiky, ve kterých se tentýž atom (včetně argumentů) vyskytuje v antecedentu i v konsekventu, tedy formule p1 , p2 , . . . , pn , p → p, q1 , q2 , . . . , qm
(7.1)
Speciální axiomy (SA) jsou klauzule znalostní báze. Znalostní báze nesmí být sporná množina. Odvozovací pravidla jsou tři: 1. Odvozovací pravidlo substituce (S): Jestliže ϕ = {t1 /X1 , t2 /X2 , . . . , tn /Xn } je substituce a C je klauzule, pak platí C ` C[ϕ] (7.2) 2. Rezoluční odvozovací pravidlo (odvozovací pravidlo rezolučního řezu, R): Označme p atom a A1 , A2 , K1 , K2 množiny atomů. Pak platí A1 , p → K1 ,
A2 → p, K2 70
`
A1 , A2 → K1 , K2
(7.3)
3. Odvozovací pravidlo existenční substituce (ES): Jestliže ϕ = (@c/a; k1 , k2 , . . . , kn ) je existenční substituce a C je klauzule, pak platí (7.4)
C ` C[ϕ] V klauzulární logice používáme také tato pomocná odvozovací pravidla:
1. Logické zákony pro predikát rovnosti: Jestliže t, r, s jsou termy a A je predikát, pak platí • • • •
→t=t t=r→r=t t = r, r = s → t = s t = r, A(t) → A(r) (A(t), A(r) jsou bázové atomy)
reflexivita predikátu rovnosti (RR) symetrie predikátu rovnosti (SR) tranzitivita predikátu rovnosti (TR) bázová substituce (BS)
2. Pomocné odvozovací pravidlo kontrakce (KK): • p, p, A → K • A → p, p, K
` `
p, A → K A → p, K
Více výskytů téhož atomu (shodných včetně argumentů) v antecedentu můžeme zredukovat na jeden výskyt, totéž platí i o konsekventu. Pravidlo lze rovněž použít na odstranění atomu true z antecedentu nebo f alse z konsekventu. 3. Pomocné odvozovací pravidlo přeuspořádání atomů (PA): Atomy v antecedentu lze přeuspořádat (změnit jejich pořadí). Atomy v konsekventu lze přeuspořádat. Příklad 7.1: Odvoďte pravidla Modus Ponens (MP) a Modus Tolens (MT). MP : MT : 1. → P 2. P → Q 3. → Q Poznámka: • • • •
SA1 SA2 R(1,2)
→P , Q→,
P →Q P →Q
` `
(7.5) (7.6)
→Q P →
1. Q → 2. P → Q 3. P →
SA1 SA2 R(1,2)
Substituci můžeme provést v těchto případech:
substituce substituce substituce substituce
bázového termu (například konstanty) za proměnnou, nové (v klauzuli se dosud nevyskytující) proměnné za proměnnou, termu, v němž se vyskytují pouze nové proměnné, za proměnnou, existenční konstanty za bázový term.
Poslední bod se týká existenční substituce. Podmínky dané zbylými body splňuje mj. nejobecnější unifikátor, který lze nalézt podle algoritmu na str. 64 v kap. 6.5.2. 71
7.2
Formální důkazy
V Klauzulárním axiomatickém systému můžeme provádět jak přímé, tak i nepřímé důkazy. Logické programovací jazyky obvykle pracují na principu nepřímého důkazu, protože tento způsob je jednodušší, lépe technicky realizovatelný. Definice 7.1: Přímý důkaz klauzule C z ze znalostní báze (množiny speciálních axiomů) B je posloupnost klauzulí A1 , A2 , . . . , Am , kde C = Am a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • Ai ∈ B (tj. je to některý ze speciálních axiomů báze), • Ai je logický axiom, • Ai vznikla použitím některého odvozovacího pravidla na předchozí členy posloupnosti. Příklad 7.2: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a odvoďte podle ní odpověď na dotaz „Jede Honza lodí?ÿ přímým důkazem. Znalostní báze: • • • •
Když země leží za mořem, každý, kdo do ní cestuje, jede lodí nebo letadlem. Německo neleží za mořem, ale Anglie ano. Honza cestuje do Anglie. Honza nejezdí letadlem.
Řešení: 1. 2. 3. 4. 5.
lezi(X, za morem), cestuje(Y, X) → jede(Y, lod), jede(Y, letadlo) lezi(nemecko, za morem) → → lezi(anglie, za morem) → cestuje(honza, anglie) jede(honza, letadlo) →
SA1 SA2 SA3 SA4 SA5
6. lezi(anglie, za morem), cestuje(honza, anglie) → jede(honza, lod), jede(honza, letadlo) S(1){anglie/X, honza/Y } 7. cestuje(honza, anglie) → jede(honza, lod), jede(honza, letadlo) R(3,6) 8. → jede(honza, lod), jede(honza, letadlo) R(4,7) 9. → jede(honza, lod) R(5,8) Prvních pět klauzulí je ze znalostní báze, další klauzule jsou již odvozeny s použitím odvozovacích pravidel substituce a rezoluce. 72
Definice 7.2: Nepřímý důkaz klauzule C z ze znalostní báze B = {SA1 , SA2 , . . . , SAn } je posloupnost klauzulí A1 , A2 , . . . , Am , kde Am = → (prázdná klauzule, vždy interpretovná jako f alse) a pro každé i ∈ {1, . . . , m} platí pro Ai některá z těchto možností: • • • •
Ai patří do popírající množiny klauzule C, Ai ∈ B (tj. je to některý ze speciálních axiomů báze), Ai je logický axiom, Ai vznikla použitím některého odvozovacího pravidla na předchozí členy posloupnosti.
Postup je následující: • vytvoříme popírající množinu pro klauzuli, kterou chceme dokázat (viz kap. 6.4.4, str. 59), • tuto popírající množinu (PM) přidáme k znalostní bázi, • odvozujeme s použitím odvozovacích pravidel, • jestliže odvodíme prázdnou klauzuli (→), klauzule je dokázána (vyplývá ze znalostní báze). Příklad 7.3: Zadání předchozího příkladu vyřešte nepřímým důkazem. 1. 2. 3. 4. 5.
lezi(X, za morem), cestuje(Y, X) → jede(Y, lod), jede(Y, letadlo) lezi(nemecko, za morem) → → lezi(anglie, za morem) → cestuje(honza, anglie) jede(honza, letadlo) →
6. jede(honza, lod) →
SA1 SA2 SA3 SA4 SA5 PM
7. lezi(anglie, za morem), cestuje(honza, anglie) → jede(honza, lod), jede(honza, letadlo) S(1){anglie/X, honza/Y } 8. cestuje(honza, anglie) → jede(honza, lod), jede(honza, letadlo) R(3,7) 9. → jede(honza, lod), jede(honza, letadlo) R(4,8) 10. → jede(honza, lod) R(5,9) 11. → R(6,10)
73
7.3
Korektnost systému
Korektnost Klauzulárního axiomatického systému budeme dokazovat převedením problému do predikátové logiky. Věta 7.1: Klauzulární axiomatický systém je korektní. Důkaz: Logický axiom je každá klauzule, jejíž množiny antecedentu a konsekventu mají neprázdný průnik (tedy existuje alespoň jeden atom, který je v antecedentu i v konsekventu). Je to tedy klauzule ve tvaru A, p → p, K. Po převodu do predikátové logiky platí tato posloupnost ekvivalencí: (A &p) → (p ∨ K) ⇔ (¬A ∨ ¬p) ∨ (p ∨ K) ⇔ ¬A ∨ (¬p ∨ p) ∨ K ⇔ ¬A ∨ 1 ∨ K ⇔ 1 Tedy axiom je logicky platná formule. Rezoluční odvozovací pravidlo přepsané do predikátové logiky je odvoditelné z rezolučního pravidla pro predikátovou logiku, jak je uvedeno v kap. 6.5.1 na str. 62. To je snadno dokazatelné s použitím sémantických metod predikátové logiky, dokazovali jsme si také ekvivalent pro Systém přirozené dedukce v kap. 3.2 na str. 19 (máme dokázáno, že Systém přirozené dedukce je korektní, tedy důkaz v tomto systému má stejnou váhu jako důkaz sémantickými metodami predikátové logiky). Odvozovací pravidla substituce a existenční substituce jsou také převeditelná do predikátové logiky, v definici substituce pro klauzulární logiku na str. 60 je dán požadavek na substituovatelnost termů za proměnné. V případě existenční substituce se dá korektnost dokázat jednoduše s použitím interpretace klauzule: jestliže něco platí pro nějaký konkrétní prvek univerza diskurzu (tj. tento prvek je použit jako term v klauzuli), pak existuje takový prvek univerza diskurzu, pro který to platí (tento prvek můžeme ve všech nebo některých jeho výskytech nahradit novou existenční konstantou). Korektnost posloupnosti důkazu se dokazuje stejně jako v případě předchozích probíraných formálních systémů. 2
74
Kapitola 8 Logické programování V této kapitole se budeme zabývat jedním z programovacích jazyků pro logické proramování, Prologem. Naučíme se s Prologem pracovat, tedy vytvářet programy a používat je. V druhé části kapitoly probereme možné způsoby implementace rezoluce v logických programovacích jazycích a podíváme se na způsob implementace použitý v Prologu.
8.1
Logické programování v Prologu
Prolog je jedním z jazyků pro logické programování. Vznikl ve Francii v roce 1973 (prof. A. Colmerauer) a jeho název je zkratka z francouzského PROgramation à LOGic („programování v logiceÿ). Je to interpretační deklarativní (neprocedurální) jazyk. Existuje mnoho Prologů. K nejznámějším patří • SWI Prolog šířený pod GNU licencí a používaný v Unixech, Linuxu a Windows, • LPA Win Prolog je komerční program pro Windows považovaný za jeden z nejlepších pro tuto platformu, • GNU Prolog pro Unixy a Linux, • OpenProlog pro MacOS, • Amzi! Prolog, • Visual Prolog, • Strawbery Prolog, atd. Odkazy na stránky uvedených Prologů a odkazy na další informace jsou k nalezení na stránce www.fpf.slu.cz/~vav10ui/vyukaprol.html. Jednotlivé Prology se liší nejen vzhledem a vybaveností svého editoru (každý Prolog má vlastní editor, se kterým je provázán), ale bohužel v některých případech také syntaxí programovacího jazyka. Rozdíly jsou například v práci se soubory. 75
Definice 8.1: Program v Prologu je konečná neprázdná množina Hornových klauzulí (viz kap. 6.1 na str. 47). Je to ekvivalent znalostní báze klauzulární logiky a množiny speciálních axiomů Klauzulárního axiomatického systému. V programu lze použít dva druhy klauzulí: • pravidla – obecná tvrzení ve tvaru „Závěr platí, pokud platí všechny jeho předpoklady zároveň.ÿ • fakty – konstantní tvrzení Používání programu spočívá v zadávání dotazů (cílových klauzulí) – Hornových klauzulí bez pozitivních literálů. Prolog dotazy vyhodnocuje podle programu a podle vnitřních pravidel (obdoba logických axiomů). Jednotlivé elementy zapisujeme následovně: Pravidlo Fakt Dotaz
Klauzulární logika Množinový zápis B, C, D → A {A, ¬B, ¬C, ¬D} →A {A} B, C, D → {¬B, ¬C, ¬D}
Zápis v Prologu A :- B, C, D. A. ?- B, C, D.
Tabulka 8.1: Zápis elementů v Prologu V případě dotazu dvojznak ?- nezapisujeme, jde o prompt (výzvu) Prologu. V pravidle rozlišujeme tělo pravidla (podle tabulky 8.1 to je B, C, D) a hlavu pravidla (A), tedy pravidlo je ve tvaru hlava :- tělo. Pro přehlednost se v delším pravidle cíl s oddělujícím dvojznakem zapisuje na samostatný řádek, tělo může být i na více řádcích.
8.1.1
Program a dotazy
Když píšeme program, postupujeme takto: 1. Vytvoříme textový soubor s příponou .pl, do kterého uložíme program (fakty a pravidla). Každý příkaz musí být na samostatném řádku (nebo na více řádcích), končí tečkou, komentáře jsou řádky začínající znakem %. 2. Načteme tento soubor (po uložení) do editoru Prologu (příkazem consult, případně některé Prology mají menu, ve kterém volíme položku consult nebo compile s tím, že před volbou v menu je vhodné soubor s programem v editoru Prologu otevřít). 3. Na výzvu Prologu (prompt, je to dvojznak ?-, znamená „zadej dotazÿ) zadáváme dotazy, Prolog vypisuje odpovědi. Načtení (přeložení, konzultování) programu je nutné, protože Prolog si program udržuje v interním kódu, se kterým se mu pracuje jednodušeji a především rychleji, navíc interní 76
kód bývá obvykle bez syntaktických chyb (kontrola se provádí při načítání a sestavování interní reprezentace programu). Při každé změně v souboru programu musíme (samozřejmě po uložení těchto změn) program znovu načíst, aby si Prolog mohl tento interní kód obnovit. Příklad 8.1: Sestavíme program obsahující zadané klauzule. Zadání programu: Petr má rád květiny, Ivanu a televizi. Jan má rád jitrnice a televizi. Věra má ráda všechno, co má rád Jan. V klauzulární logice: → ma rad(petr, kvetiny) → ma rad(petr, ivana) → ma rad(petr, televize) → ma rad(jan, jitrnice) → ma rad(jan, televize) ma rad(jan, X) → ma rad(vera, X) Program v Prologu (uložíme do .pl souboru): ma_rad(petr,kvetiny). ma_rad(petr,ivana). ma_rad(petr,televize). ma_rad(jan,jitrnice). ma_rad(jan,televize). ma_rad(vera,X):-ma_rad(jan,X). Dotazy mohou obsahovat jeden nebo více atomů, argumenty predikátů mohou být i proměnné. Pokud jsou všechny atomy dotazu bázové, Prolog odpoví pouze YES nebo NO, podle toho, zda klauzule dotazu vyplývá z programu (znalostní báze), jestliže však jsou použity proměnné, Prolog vypíše všechny možné hodnoty proměnné (kombinace proměnných), pro které je dotaz splnitelný. Po vypsání každé kombinace se zastaví a čeká na reakci uživatele. Pokud uživatel stiskne klávesu ; , hledá další kombinaci hodnot, jinak (klávesa ENTER ) odpoví buď YES nebo NO podle toho, zda ještě nějaké další kombinace existují. Příklad 8.2: Po načtení programu z předchozího příkladu zadáme následující dotazy a získáme uvedené odpovědi. Má rád Petr televizi?
?- ma_rad(petr,televize). yes
Má rád Jan květiny?
?- ma_rad(jan,kvetiny). no 77
Co má rád Jan?
?- ma_rad(jan,X). X = jitrnice ; X = televize ; no
Kdo má rád jitrnice?
?- ma_rad(X,jitrnice). X = jan ; X = vera ; no
Co má rád Petr a zároveň Jan?
?- ma_rad(petr,X),ma_rad(jan,X) X = televize ; no
Kdo má co (koho) rád?
?- ma_rad(Kdo,Co). Kdo Kdo Kdo Kdo Kdo Kdo Kdo no
8.1.2
= = = = = = =
petr , Co = kvetiny ; petr , Co = ivana ; petr , Co = televize ; jan , Co = jitrnice ; jan , Co = televize ; vera , Co = jitrnice ; vera , Co = televize ;
Základní prvky syntaxe Prologu
Existenční termy v Prologu nepoužíváme, místo nich máme k dispozici anonymní proměnnou (zapisuje se znakem podtržítka). Pro argument, ve kterém je použita, existuje hodnota, kterou tam lze dosadit, ale tato hodnota nás nezajímá (kdyby nás zajímala, pak bychom použili konstantu nebo proměnnou). Anonymní proměnnou také použijeme místo „běžnéÿ proměnné, pokud se tato proměnná vyskytuje v těle pravidla pouze jednou. Příklad 8.3: Máme následující program: Liška loví zajíce. Orel loví myš. Orel loví vrabce. Honza loví rybu. Kdo někoho loví, je dravec.
lovi(liska,zajic). lovi(orel,mys). lovi(orel,vrabec). lovi(honza,ryba). dravec(X) :- lovi(X,_). Budeme zadávat dotazy:
Existují nějací dravci?
?- dravec(_). yes 78
Loví někoho liška?
?- lovi(liska,_). yes
Kdo někoho loví?
?- lovi(X,_). X = liska ; X = orel ; X = honza ; no
Vzhledem k tomu, že v Prologu lze využívat pouze Hornovy klauzule, jsou omezeny možnosti řešení negace přesunem atomu z antecedentu do konsekventu a naopak (i když je lze použít, pokud vyjde Hornova klauzule). Proto Prology obsahují speciální predikát not. Predikát not je vyhodnocován jako negace svého argumentu (je vyhodnocen argument, pak je jeho pravdivostní hodnota znegována). Je to totéž, jako bychom provedli úplnou negaci argumentu včetně proměnných (to můžeme vidět také v predikátové logice). Predikátem not ve skutečnosti ani tak nepopíráme atom, jako spíše sdělujeme, že tento atom není odvoditelný z programu (znalostní báze). To přináší některé problémy, jejichž důsledkem může být nepředpokládané chování systému. Změní se charakter proměnné a ta po provedení negace přestává být totožná s ostatními (dříve uvedenými) proměnnými téhož jména v těle pravidla nebo v dotazu. Řešením tohoto problému je uvádění negovaných atomů jako posledních atomů těla pravidla nebo dotazu (rozhodně až za všemi atomy, které obsahují stejné proměnné, pokud je to možné). Příklad 8.4: Máme následující program: osobni(autoPepy). osobni(autoJany). nakladni(autoStandy). ma_vozik(autoJany). auto(X) :- osobni(X). Každé osobní auto je auto. auto(X) :- nakladni(X). velky_naklad(X) :- nakladni(X). Nákladní auta uvezou velký náklad. velky_naklad(X) :- osobni(X),ma_vozik(X). Osobní auta s vozíkem uvezou velký náklad. maly_naklad(X) :- auto(X),not(velky_naklad(X)). Auta, která neuvezou velký náklad, uvezou malý náklad. Zadáváme dotazy: Která auta jsou nákladní?
?- nakladni(X). X = autoStandy ; no 79
Která auta jsou osobní kromě auta Jany?
?- osobni(X),not(X=autoJany). X = autoPepy ; no
Při použití negace bychom měli mít na vědomí, že musíme Prologu umožnit proměnnou nejdřív unifikovat v „pozitivnímÿ atomu, a teprve pak by měl následovat atom negovaný predikátem not. V předchozím příkladu jsme mohli vidět i použití predikátu rovnosti. Predikát rovnosti se také používá pro stanovení interpretace funktorů. Příklad 8.5: Máme následující program: matka(pepa)=jana. otec(pepa)=honza. matka(jana)=jitka. matka(honza)=emilka. otec(jana)=albert. otec(honza)=karel. matka(albert)=katerina. babicka(Vnouce,Babicka) :- X=matka(Vnouce),Babicka=matka(X). babicka(Vnouce,Babicka) :- X=otec(Vnouce),Babicka=matka(X). dedecek(Vnouce,Dedecek) :- X=matka(Vnouce),Dedecek=otec(X). dedecek(Vnouce,Dedecek) :- X=otec(Vnouce),Dedecek=otec(X). prababicka(Vnouce,Prababicka) :X=matka(Vnouce),babicka(X,Prababicka). prababicka(Vnouce,Prababicka) :X=otec(Vnouce),babicka(X,Prababicka). Zadáváme dotazy: Kdo je Pepovým dědečkem?
?- dedecek(pepa,X). X = albert ; X = karel ; no
Kdo je Pepova prababička?
?- prababicka(pepa,X). X = katerina ; no
Poznámka: Prolog obsahuje další užitečné syntaktické prvky, kterými se zde nebudeme zabývat. Jsou to například aritmetické operátory, kromě predikátu rovnosti také predikát nerovnosti a další relační operátory, dynamické seznamy, řetězce, možnost reprezentace disjunkce, pro řízení výpočtu lze použít tzv. řez (cut), máme k dispozici mnoho vestavěných predikátů (jeden z nich je i not). Lze pracovat také se vstupy a výstupy programu. 80
8.2
Rezoluce v logickém programování
Definice 8.2: Nechť M je množina klauzulí klauzulární logiky. Označíme R(M ) množinu klauzulí, pro kterou platí: • M ⊆ R(M ) (zařadíme zde všechny klauzule původní množiny), • Jestliže klauzule C vznikne uplatněním rezolučního odvozovacího pravidla na klauzule Ci a Cj , kde Ci ∈ M, Cj ∈ M , pak C ∈ R(M ) (na každou unifikovatelnou dvojici klauzulí z M uplatníme rezoluční pravidlo a výslednou rezolventu zařadíme do R(M )). Rezoluční uzávěr množiny klauzulí M n-tého stupně je množina klauzulí Rn (M ) definovaná rekurzívně: R0 (M ) = M, Ri (M ) = R (Ri−1 (M )) , 1 ≤ i ≤ n
(8.1)
Věta 8.1: (Robinsonův rezoluční princip) Množina klauzulí klauzulární logiky M je nesplnitelná, jestliže existuje přirozené číslo n takové, že Rn (M ) obsahuje prázdnou klauzuli →. Důkaz: logiky.
Důkaz provedeme zpětnou matematickou indukcí s převodem do predikátové
Množinu klauzulí klauzulární logiky lze převést na formuli predikátové logiky v klauzulární normální formě (klauzule převedeme do predikátové logiky a spojíme konjunkcí). Z množiny M klauzulí klauzulární logiky tak sestrojíme ekvivalentní formuli C(M ) predikátové logiky. Již dříve bylo dokázáno, že • prázdná klauzule má vždy hodnotu f alse (je kontradiktorická, nepravdivá), přepisujeme ji do predikátové logiky jako true → f alse, • rezoluční pravidlo zachovává splnitelnost (je korektní), a to i po převodu do predikátové logiky, • jestliže množina klauzulí obsahuje nesplnitelnou podmnožinu, je nesplnitelná (mezi klauzulemi je vztah konjunkce), tedy po převodu do predikátové logiky platí vztah X &f alse ⇔ f alse. Rezoluční odvozovací pravidlo převedeme do predikátové logiky jako pravidlo F1 &(A1 &p → K1 ) &(A2 → p ∨ K2 ) &F2 ` F1 &(A1 &A2 → K1 ∨ K2 ) &F2
(8.2)
Dá se dokázat, že také toto pravidlo zachovává splnitelnost, je přímo odvoditelné z rezolučního odvozovacího pravidla. 81
Báze indukce: Množina klauzulí Rn (M ) obsahuje prázdnou klauzuli, proto formule predikátové logiky C(Rn (M )) je nesplnitelná. Předpoklad indukce: Předpokládejme, že formule C(Ri (M )), i > 0 je nesplnitelná. Krok indukce: Jestliže formule C(Ri (M )), i > 0 je nesplnitelná a byla získána z formule C(Ri−1 (M )), i > 0 uplatněním pravidla 8.2, pak také C(Ri−1 (M )), i > 0 musí být nesplnitelná, protože použité pravidlo zachovává splnitelnost. Když krok indukce uplatníme n-krát, zjistíme, že R0 (M ) = M je nesplnitelná. 2 Důsledek: Důsledkem této věty je princip nepřímého rezolučního odvozování v klauzulární logice, v predikátové logice a také v logických programovacích jazycích – závěr znegujeme, přidáme k množině klauzulí (programu) a dokazujeme, že takto rozšířená množina je nesplnitelná, a pro důkaz nesplnitelnosti stačí, když odvodíme prázdnou klauzuli. Účelem logického programování založeného na nepřímém rezolučním odvozování je tedy při uplatňování rezolučního odvozovacího pravidla najít prázdnou klauzuli. Pokud volíme postup naznačený výše uvedenou větou (metoda generování do šířky), je často již pro celkem malé číslo i množina Ri (M ) hodně velká, proto tento postup není moc vhodný. Jinou možností jsou metody generování do hloubky, kdy generujeme pouze ty klauzule, které potřebujeme pro postupné odvození prázdné klauzule. Metody generování do hloubky mají výhodu větší efektivnosti, ale jejich úspěšnost závisí na vhodné volbě klauzulí, na které uplatníme rezoluční odvozovací pravidlo. Různé metody používají pro tento výběr různé strategie. Nejpoužívanější metodou v logickém programování je lineární metoda – rezoluční odvozovací pravidlo uplatňujeme vždy na poslední klauzuli přidanou k důkazu a některou další klauzuli, klauzuli, která je důsledkem uplatnění pravidla, pak použijeme v dalším kroku pro další odvození. Definice 8.3: Lineární výpočetní strom klauzule pro znalostní bázi je takový strom, kde: • všechny uzly jsou ohodnoceny klauzulemi, • kořen je ohodnocen cílovou klauzulí, • pro všechny uzly stromu platí: jestliže je uzel ohodnocen klauzulí C, pak každý jeho potomek je ohodnocen klauzulí vzniklou uplatněním rezolučního odvozovacího pravidla na klauzuli C a některou klauzuli znalostní báze. Příklad 8.6: Vytvořte výpočetní strom pro nepřímý důkaz důkaz klauzule ze znalostní báze 1. 2. 3. 4.
A, B → C D→B →A C→
82
D →
Při konstrukci nepřímého důkazu budeme vždy rezoluční odvozovací pravidlo používat na poslední klauzuli, kterou jsme přidali k posloupnosti důkazu (v prvním kroku to je klauzule popírající množiny) a některou další klauzuli, tedy budeme postupovat lineární metodou. V tomto příkladu existují dvě takové posloupnosti důkazu: 5. 6. 7. 8. 9.
→D →B A→C →C →
5. 6. 7. 8. 9.
PM R(2,5) R(1,6) R(3,7) R(4,8)
→D →B A→C A→ →
PM R(2,5) R(1,6) R(4,7) R(3,8)
Výpočetní strom konstruujeme tak, že kořen stromu ohodnotíme první klauzulí popírající množiny a dále podle každé vytvořené důkazní posloupnosti vytvoříme větev stromu. →D →B A→C @
@ @
→C
A→
→
→
Obrázek 8.1: Výpočetní strom nepřímého důkazu klauzule Výpočetní strom může být hodně rozvětvený a navíc i nekonečný (některá větev představuje nekonečný výpočet). Účelem je najít prázdnou klauzuli. Hledání můžeme provádět dvěma způsoby: • prohledávání do hloubky – prohledáme nejdřív první větev, pak druhou, . . . , • prohledávání do šířky – prohledáváme strom „po patrechÿ shora, tedy pracujeme se všemi větvemi stromu najednou. Výhodou druhé metody je spolehlivost, pokud někde ve stromě je prázdná klauzule, najdeme ji. Její nevýhodou je však pomalost a výpočetní složitost (musíme si udržovat informace o všech prováděných důkazech zároveň). Tuto nevýhodu řeší první metoda, její nevýhodou je však riziko možnosti nekonečného výpočtu (v případě, že větev nejvíc vlevo neobsahuje prázdnou klauzuli, například z důvodu zacyklení výpočtu). 83
Programovací jazyky pro logické programování obvykle používají lineární metodu s prohledáváním do hloubky. Nebezpečí zacyklení výpočtu lze pak předejít vhodným pořadím klauzulí ve znalostní bázi a pořadím atomů v jednotlivých klauzulích. Zacyklení většinou předejdeme, pokud dodržujeme tato pravidla: 1. Ve znalostní bázi nejdřív uvádíme fakty, pak pravidla. Protože překladač při prohledávání báze postupuje shora dolů, docílíme tím používání takových unifikací klauzulí pro rezoluci, při kterých nedojde ke zbytečnému opakování výpočtu a tím někdy i k rekurzivnímu vyhodnocování klauzulí. 2. Jestliže je v těle klauzule (v antecedentu) atom se stejným predikátem jako atom v hlavě klauzule, třeba i s jinými argumenty, pak takový atom umístíme až na konec těla klauzule. Opět tím zamezíme nadbytečnému rekurzivnímu volání klauzule.
8.3
Průběh výpočtu v Prologu
Prolog je deklarativní jazyk, tedy programátor určuje, co se má provést a ne jak se to má provést a kam ukládat mezivýsledky výpočtu. Data a program splývají, nerozlišují se. Řízení výpočtu je tedy na Prologu samotném, my mu pouze vhodným jazykem sdělíme, co má zjistit (odvodit, dokázat, vypsat). Přesto je užitečné mít alespoň základní přehled o tom, jak výpočet probíhá, a to proto, abychom se dokázali vyhnout zbytečné, třeba i nekonečné rekurzi, optimalizovat program, a také co nejlépe využít prostředky, které nám jazyk nabízí. Prolog při uplatňování rezoluce používá lineární metodu s prohledáváním do hloubky, která byla popsána v předchozí kapitole. Aby bylo možné používat rezoluční odvozovací pravidlo, musí být obvykle klauzule upraveny substitucí – unifikací. Prolog provádí nejobecnější unifikaci, aby se zbytečně neprodlužovala doba výpočtu. Informace o použitých unifikačních substitucích se ukládají. Protože všechny proměnné v Prologu jsou lokální pro danou klauzuli (dvě stejně pojmenované proměnné v různých klauzulích jsou ve skutečnosti různé proměnné) a globální proměnné neexistují, musí být v údaji o unifikaci explicitně odlišeny stejně pojmenované proměnné z různých klauzulí. Prolog toto zajišťuje připojením čísla klauzule k proměnné, a tím je odstraněno nebezpečí kolize. Pro unifikaci je použit algoritmus podobný algoritmu pro hledání nejobecnějšího unifikátoru, který je uveden v kapitole 6.5.2 na str. 63. Aniž si to většinou uvědomujeme, zadáváme dotaz v negovaném tvaru. Pokud jsou v dotazu použity proměnné, v původním (nenegovaném) tvaru jsou ve skutečnosti vázány existenčně, tedy ptáme se, zda existují nějaké hodnoty proměnných takové, že platí formule dotazu. V predikátové logice můžeme negovaný dotaz vyjádřit takto: ⇔
¬∃u1 ∃u2 . . . ∃ur (A1 &A2 & . . . &Ap ) ∀u1 ∀u2 . . . ∀ur (¬A1 ∨ ¬A2 ∨ . . . ∨ ¬Ap ) 84
⇔ ∀u1 ∀u2 . . . ∀ur (true → (¬A1 ∨ ¬A2 ∨ . . . ∨ ¬Ap )) Poslední uvedená formule se do klauzulární logiky přepisuje jako A1 , A2 , . . . , Ap →
(8.3)
Všechny proměnné ui jsou vázány univerzálně, proto lze na klauzuli uplatňovat rezoluční pravidlo. Samotný výpočet je rekurzivní proces, který se provádí tak dlouho, dokud je co počítat (u zacykleného výpočtu teoreticky i do nekonečna, prakticky se výpočet zastaví s chybovým hlášením o přetečení zásobníku). V každém kroku zpracováváme klauzuli, který nazýváme cílová klauzule, její atomy nazýváme cíle, a hledáme klauzuli takovou, aby bylo možné na ni a na cílovou klauzuli uplatnit pravidlo rezoluce. Když se nám to podaří, rezolventa (výsledek uplatnění pravidla) se stává novou cílovou klauzulí pro další krok výpočtu. Při výpočtu používáme zásobník , do kterého při každém použití unifikace a rezoluce ukládáme údaje o této operaci. Uložíme vždy číslo klauzule, na kterou bylo spolu s cílovou klauzulí uplatněno pravidlo rezoluce, a údaje o unifikační substituci použité pro přípravu na rezoluci, tedy údajem je uspořádaná dvojice [i, ϕ], kde i je číslo klauzule a ϕ je unifikace. Údaje se ze zásobníku vyjímají při každém ukončení výpočtu větve (ať úspěšném – yes nebo neúspěšném – no). Když byl tento údaj do zásobníku uložen, byla unifikace ϕ a rezoluce použita na klauzuli s číslem i. V případě úspěchu jsme již cíl, ke kterému se takto dalo dostat, zpracovali a potřebujeme najít další cíl, v případě neúspěchu tato cesta zklamala a potřebujeme najít další cestu ke splnění cíle, proto budeme pokračovat následující klauzulí – i + 1 s tím, že jako cílovou klauzuli budeme mít tu, která byla cílovou klauzulí před krokem určeným údajem [i, ϕ]. Tato klauzule se dá zjistit „zpětným provedenímÿ operací daných těmito údaji. Vyjmutí údajů ze zásobníku je vlastně navracení se k předchozímu cíli, tato operace se nazývá navracení (backtracking). Protože pracujeme s Hornovými klauzulemi a navíc výpočet začíná u dotazu, který má všechny atomy v antecedentu, je algoritmus postupu výpočtu poměrně jednoduchý: 1. Na začátku výpočtu se cílovou klauzulí stane (negovaný) dotaz. 2. Jestliže je cílovou klauzulí prázdná klauzule, končíme výpočet větve s úspěchem (yes). Jsou dvě možnosti: (a) V dotazu jsou proměnné: vypíšeme nalezené hodnoty těchto proměnných (poslední hodnoty ze zásobníku příslušející těmto proměnným), čekáme na stisk klávesy a pokud je to klávesa ; , provedeme navracení a pokračujeme bodem 3. (b) V dotazu nejsou proměnné: vypíšeme yes, ukončíme celý výpočet a smažeme obsah zásobníku. 85
3. Vezmeme nejlevější atom (cíl) cílové klauzule a hledáme v programu klauzuli, která • ještě pro tento cíl nebyla použita, • má ve své hlavě (tj. v konsekventu) tentýž predikát jako testovaný cíl • a je možné provést unifikaci přes atom v hlavě klauzule a testovaný cíl cílové klauzule. Jsou tři možnosti: (a) Takovou klauzuli najdeme: pokračujeme bodem 4. (b) Takovou klauzuli se nepodaří najít a zásobník není prázdný: provedeme navracení (vše, co bylo až do této pozice v programu provedeno, zrušíme a zkoušíme další cestu) a pokračujeme bodem 3. (c) Takovou klauzuli se nepodaří najít a zásobník je prázdný: nelze pokračovat jinak, než jak se dosud postupovalo (tj. zásobník je prázdný, ale cílová klauzule je neprázdná), končíme výpočet s neúspěchem (vypíšeme no). 4. Unifikujeme cílovou klauzuli a nalezenou klauzuli, uplatníme pravidlo rezoluce a rezolventu (výsledek rezoluce) použijeme jako novou cílovou klauzuli. Je zřejmé, že nejlevější cíl, který jsme zpracovávali v původní cílové klauzuli, se v nové cílové klauzuli neobjeví. Do zásobníku je uloženo číslo klauzule, která je unifikována s cílem, a údaje o použité substituci. Pokračujeme bodem 2. Příklad 8.7: Odvození odpovědi na dotaz „Jde Pepa do restaurace?ÿ z uvedeného programu provedeme nejdřív v klauzulární logice a pak v Prologu. V klauzulární logice: 1. 2. 3. 4. 5.
→ turista(pepa) → cestuje(pepa, dlouho) nudi se(X), spolecensky(X) → jde do(X, restaurace) turista(X), ma hlad(X) → jde do(X, restaurace) cestuje(X, dlouho) → ma hlad(X)
SA1 SA2 SA3 SA4 SA5 PM (výchozí cílová klauzule)
6. jde do(pepa, restaurace) →
7. nudi se(pepa), spolecensky(pepa) → jde do(pepa, restaurace) S(3){pepa/X} 8. nudi se(pepa), spolecensky(pepa) → R(6,7) nelze pokračovat, vyjmeme ze zásobníku [3, pepa/X], pokračujeme 4. klauzulí 9. turista(pepa), ma hlad(pepa) → jde do(pepa, restaurace) 10. turista(pepa), ma hlad(pepa) → 86
S(4){pepa/X} R(6,9)
11. 12. 13. 14.
ma hlad(pepa) → cestuje(pepa, dlouho) → ma hlad(pepa) cestuje(pepa, dlouho) → →
R(1,10) S(5){pepa/X} R(11,12) R(2,13)
V Prologu1 : 1. 2. 3. 4. 5.
turista(pepa). cestuje(pepa,dlouho). jde_do(X,restaurace) :- nudi_se(X),spolecensky(X). jde_do(X,restaurace) :- turista(X),ma_hlad(X). ma_hlad(X) :- cestuje(X,dlouho).
6. ?- jde_do(pepa,restaurace). Postup výpočtu: 1. Výchozí cílová klauzule je :- jde_do(pepa,restaurace). Hledáme v hlavách klauzulí predikát jde_do. 2. Nalezli jsme klauzuli číslo 3, hlava klauzule souhlasí s prvním (momentálně jediným) cílem cílové klauzule. Provedeme unifikaci, výsledkem unifikace jsou klauzule :- jde_do(pepa,restaurace). jde_do(pepa,restaurace) :- nudi_se(pepa),spolecensky(pepa). Do zásobníku uložíme [3,{pepa/X_3}]. Cílová klauzule je :- nudi_se(pepa),spolecensky(pepa). Hledáme v hlavách klauzulí predikát nudi_se. 3. Navracení, predikát nudi_se není v hlavě žádné unifikovatelné klauzule. Ze zásobníku vyjmeme [3,{pepa/X_3}], tyto údaje pomohou zjistit původní cílovou klauzuli, která se opět stává cílovou klauzulí. Prohledáváme program od klauzule číslo 4 (tj. 3+1). Cílová klauzule je :- jde_do(pepa,restaurace). 1
Ve skutečnosti bychom museli přidat ještě nějaké klauzule s predikátem nudi se a spolecensky v hlavě, protože jinak by při pokusu o vyhodnocení cíle jde do Prolog vypsal chybové hlášení Predicate Not Defined.
87
4. Nalezli jsme klauzuli číslo 4. Provedeme unifikaci, výsledkem unifikace jsou klauzule :- jde_do(pepa,restaurace). jde_do(pepa,restaurace) :- turista(pepa),ma_hlad(pepa). Do zásobníku uložíme [3,{pepa/X_4}]. Cílová klauzule je :- turista(pepa),ma_hlad(pepa). Hledáme v hlavách klauzulí predikát turista. 5. Nalezli jsme klauzuli číslo 1. Unifikace je prázdná množina (není třeba unifikovat, v obou klauzulích jsou pouze konstanty). Do zásobníku uložíme [1,∅]. Cílová klauzule je :- ma_hlad(pepa). Hledáme v hlavách klauzulí predikát ma_hlad 6. Nalezli jsme klauzuli číslo 5. Provedeme unifikaci, výsledkem unifikace jsou klauzule :- ma_hlad(pepa). ma_hlad(pepa) :- cestuje(pepa,dlouho). Do zásobníku uložíme [5,{pepa/X_5}]. Cílová klauzule je :- cestuje(pepa,dlouho). Hledáme v hlavách klauzulí predikát cestuje 7. Nalezli jsme klauzuli číslo 2. Unifikace je prázdná množina. Do zásobníku uložíme [2,∅]. Cílová klauzule je :- . Protože je to prázdná klauzule, končíme výpočet větve s výsledkem yes. V dotazu nejsou žádné proměnné, proto nemusíme pokračovat dál. Vypíšeme yes a vyprázdníme zásobník. Příklad 8.8: Podle stejné báze provedeme odvození odpovědi na dotaz „Kdo je hladový?ÿ (tj. tážeme se „Existuje někdo hladový?ÿ a chceme zároveň vědět, kdo to je). V klauzulární logice: 1. → turista(pepa) 2. → cestuje(pepa, dlouho) 3. nudi se(X), spolecensky(X) → jde do(X, restaurace) 88
SA1 SA2 SA3
4. turista(X), ma hlad(X) → jde do(X, restaurace) 5. cestuje(X, dlouho) → ma hlad(X)
PM (výchozí cílová klauzule)
6. ma hlad(X) → 7. 8. 9. 10.
SA4 SA5
S(5){X/X} (unifikace) R(6,7) S(8){pepa/X} (unifikace s 2) R(2,9)
cestuje(X, dlouho) → ma hlad(X) cestuje(X, dlouho) → cestuje(pepa, dlouho) → →
V Prologu2 : 1. 2. 3. 4. 5.
turista(pepa). cestuje(pepa,dlouho). jde_do(X,restaurace) :- nudi_se(X),spolecensky(X). jde_do(X,restaurace) :- turista(X),ma_hlad(X). ma_hlad(X) :- cestuje(X,dlouho).
6. ?- ma_hlad(X). Postup výpočtu: 1. Výchozí cílová klauzule je :- ma_hlad(X). Hledáme v hlavách klauzulí predikát ma_hlad. 2. Nalezli jsme klauzuli číslo 5. Výsledkem unifikace jsou klauzule :- ma_hlad(X). ma_hlad(X) :- cestuje(X,dlouho). (tj. klauzule se nemění) Do zásobníku uložíme [5,{X/X,X_5/X}]. Cílová klauzule je :- cestuje(X,dlouho). Hledáme v hlavách klauzulí predikát cestuje. 3. Nalezli jsme klauzuli číslo 2. Výsledkem unifikace jsou klauzule :- cestuje(pepa,dlouho). cestuje(pepa,dlouho). Do zásobníku uložíme [2,{pepa/X}]. Cílová klauzule je :- . 2
Aby Prolog mohl pracovat korektně, ve skutečnosti budeme potřebovat také klauzule, které mají v hlavě predikáty nudi se a spolecensky.
89
4. Je to prázdná klauzule, proto vypíšeme poslední hodnotu, která byla substituována za X (tj. to co je na zásobníku nejvýše): X = pepa a čekáme na stisk klávesy. 5. Byla stisknuta klávesa ; . 6. Provedeme navracení: vyjmeme ze zásobníku poslední uložené údaje – [2,{pepa/X}]. Cílová klauzule je :- cestuje(X,dlouho). Hledáme v hlavách klauzulí predikát cestuje, a to až od 3. klauzule. 7. Navracení, predikát cestuje není v hlavě žádné klauzule od klauzule č. 3. Ze zásobníku vyjmeme [5,{X/X,X_5/X}]. Cílová klauzule je :- ma_hlad(X). Hledáme v hlavách klauzulí predikát ma_hlad, a to až od 6. klauzule. 8. V bázi však už 6. klauzule není, navracení už nelze provést (zásobník je prázdný), proto končíme výpočet větve s neúspěchem (vypíšeme no) a ukončíme celý výpočet. Během výpočtu byl vygenerován tento výstup: X = pepa ; no
(v bodu 4 tohoto postupu) (v bodu 8 tohoto postupu)
90
Příloha A Příklady V této příloze jsou především příklady na procvičení převodu klauzulí do klauzulární logiky a odvozování v Klauzulárním axiomatickém systému. V některých příkladech je také úkolem převod báze a dotazu do programovacího jazyka Prolog. Řešení příkladů zde není uvedeno, najdeme je v příloze B. Příklad 1: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní zjistěte, zda platí „Kdo je okřídlený a má lehkou kostru, létá.ÿ přímým důkazem a zda platí „Existuje někdo, kdo nemá lehkou kostru.ÿ nepřímým důkazem. • • • • • • • •
Kdo je okřídlený a má lehkou kostru, umí létat. Ti, kdo umí létat a zrovna nelétají, odpočívají. Motýl, který odpočívá, je na květině (odpočívající motýl je na květině). Kdo je okřídlený a je na něčem, potřebuje to, na čem je. Motýl je okřídlený a má lehkou kostru, pštros je okřídlený, ale nemá lehkou kostru. Existuje někdo, kdo neumí létat. Kdo umí létat, je okřídlený (tj. má křídla). Zrovna nikdo neodpočívá.
Příklad 2: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a odvoďte podle ní odpověď na dotaz „Zlomila si Jana nohu?ÿ přímým i nepřímým důkazem. • • • •
Dobrá hospodyňka pro pírko přes plot skočí. Kdo skáče přes plot (pro cokoliv), zlomí si nohu nebo si udělá bouli. Jana je dobrá hospodyňka. Jana skočila přes plot pro pírko, ale neudělala si bouli. 91
Příklad 3: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Bylo nějaké dítě potrestáno zákazem večerníčka?ÿ nepřímým důkazem. Znalostní bázi přepište na program v Prologu a pak také do Prologu přepište následující dotazy. • • • • • • •
Mráz kreslí na okno. Jana a Pepík jsou děti, Patrik je dospělý. Jana kreslí na zeď, ale nebyla potrestána zákazem zákusku. Pepík kreslí na papír, Patrik kreslí na zeď. Kdo kreslí na zeď, je potrestán. Dospělý je potrestán vězením, dítě zákazem večerníčka nebo zákusku. Dítě, které je potrestáno zákazem večerníčka, pláče.
Dotazy pro vyjádření v Prologu: • • • • •
Kdo kam kreslí? Kdo pláče? Kreslí někdo na zeď? Které děti jsou potrestány? Jaké tresty mohou být uděleny? (nezajímá nás, kdo byl jak potrestán)
Příklad 4: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Pohybuje se někdo rychle?ÿ nepřímým důkazem. Znalostní bázi přepište na program v Prologu a pak také do Prologu přepište následující dotazy. • • • • • • • • •
Jerry je myš, Tom a Smoky jsou kočky a Baryk je pes. Jerry vidí Toma, Smoky vidí Baryka a Baryk vidí Smokyho. Kočky, myši a psi jsou zvířata. Žádný pes není kočka. Myši se bojí koček, kočky se bojí psů. Každý, kdo utíká, se pohybuje rychle. Každé zvíře, které vidí někoho, koho se bojí, utíká. Pro každého platí: když vidí toho, kdo se ho bojí, honí ho. Kdo někoho honí, pohybuje se rychle.
Dotazy pro vyjádření v Prologu: • Kdo vidí Toma? • Která zvířata se rychle pohybují? 92
• Utíká někdo? • Kdo se koho bojí? • Kdo koho honí? Příklad 5: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a odvoďte podle ní odpověď na dotaz „Je javor zelený?ÿ nepřímým důkazem. Znalostní bázi přepište do Prologu. • • • • • •
Javor je listnatý strom, borovice a modřín jsou jehličnaté stromy. Žádný listnatý strom není jehličnatý, žádný jehličnatý strom není listnatý. Listnaté stromy mají v létě listí, jehličnaté stromy mají v létě jehličí. Listnaté stromy nemají v zimě listí. Borovice má v zimě jehličí. Všechno, co má v létě listí nebo jehličí, je zelené.
Příklad 6: Vyjádřete v klauzulích klauzulární logiky znalostní bázi (žralok, delfín a kapr jsou konstanty) a podle ní odvoďte odpověď na dotaz „Potřebuje kapr vodu?ÿ nepřímým důkazem. Znalostní bázi také přepište do Prologu. • • • •
Všichni, kdo žijí ve vodě (slané nebo sladké), jsou vodní živočichové. Žralok a delfín žijí ve slané vodě, kapr žije ve sladké vodě. Každý vodní živočich potřebuje vodu. Někdo žije ve slané vodě.
Příklad 7: Podle znalostní báze v předchozím příkladu odvoďte odpověď na otázku „Existuje někdo, kdo žije ve slané vodě a potřebuje vodu?ÿ nepřímým důkazem. Příklad 8: Vyjádřete v klauzulích klauzulární logiky znalostní bázi (jména zvířat jsou konstanty) a podle ní odvoďte odpověď na dotaz „Utekl Ferda?ÿ nepřímým důkazem. Znalostní bázi přepište na program v Prologu. • Lišky a zajíci žijí v lese, králíci žijí na dvoře. • Bystrouška je liška, Ferda je králík a Ušák je zajíc. • Když se tvor žijící na dvoře dostane do lesa, potká nějakou lišku (jakoukoliv) a neuteče, je sežrán. • Ferda se dostal do lesa, potkal Bystroušku, ale nebyl sežrán. Příklad 9: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Je Pepa na moři?ÿ nepřímým důkazem. 93
• • • • •
Pepa a Honza jsou námořníci, Rudolf není námořník. Někteří námořníci umí plavat. Námořníci jsou na lodi, ale ne na řece. Loď může být na moři nebo na řece. Vztah „být na něčemÿ splňuje vlastnost tranzitivity, tedy „každý je také na tom, na čem je to, na čem jeÿ (například Kdo je na něčem, co je na moři, je také na moři).
Příklad 10: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Je zajíc býložravec?ÿ nepřímým důkazem. • • • • • • •
Liška je šelma. Šelmy jsou masožravci. Všichni masožravci jsou šelmy. Zajíc není šelma, a není ani všežravec. Kdo jí rostliny, je býložravec nebo všežravec. Kdo není masožravec, jí rostliny. (Každý je buď masožravec, nebo jí rostliny.) Existují nějaké šelmy.
Příklad 11: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Existuje někdo, kdo dýchá vzduch?ÿ nepřímým důkazem. Znalostní bázi přepište na program v Prologu. • • • • • •
Kdo žije ve vodě, a nemá žábra, má plíce. Kytovci, ryby i obojživelníci žijí ve vodě. Kytovci nemají žábra. Delfín a vorvaň jsou kytovci, štika je ryba a žába je obojživelník. Kdo má plíce, dýchá vzduch. Obojživelníci mají žábra i plíce, ryby mají žábra.
Příklad 12: Vyjádřete v klauzulích klauzulární logiky znalostní bázi a podle ní odvoďte odpověď na dotaz „Existuje pták, který dál doskáče?ÿ nepřímým důkazem. Znalostní bázi přepište na program v Prologu a pak také do Prologu přepište následující dotazy. • • • •
Skřivan a sova jsou ptáci, ale jen skřivan je ranní ptáče. Pepa je člověk a zároveň ranní ptáče. Lída je sportovec, vlastní trampolínu. Člověk Honza vlastní papouška a trampolínu, ale není sportovec. 94
• Každý sportovec je člověk. • Ranní ptáče dál doskáče. • Sportovec, který vlastní trampolínu, dál doskáče. Dotazy pro přepis do Prologu: • • • • •
Vyjmenuj všechny lidi. Kdo dál doskáče? Kdo je ranní ptáče? Jsou nějací sportovci? Který pták není ranní ptáče?
Příklad 13: Přepište následující věty na program v Prologu a formulujte uvedené dotazy. • • • • • • • •
Je -5 stupňů a sněží. Lůďa a Honza jsou cestáři, Ferda je sněhulák. Klapka má místo nosu mrkev. Honza právě vypráví pohádky. Kdo má mrkev místo nosu nebo uhlíky místo očí, je sněhulák. Mráz je, když je méně než 0 stupňů. Když je méně stupňů než 0, je mráz. Když je mráz a sněží, každý cestář odhrnuje sníh.
(vyprávění pohádek a odhrnování sněhu vyjádřete jedním predikátem určujícím, kdo jakou práci zrovna dělá) Dotazy: • • • • •
Jaké je počasí? Co zrovna dělají jednotliví cestáři? Vyjmenuj všechny sněhuláky. Dělá Lůďa něco? Co dělá Honza?
Příklad 14: Přepište následující věty na program v Prologu a formulujte uvedené dotazy. • Micka je kočka, Karlík a Hvězdička jsou papoušci, Houkalka je sova a Pepík je člověk. • Papoušci a sovy jsou ptáci, kočky a lidé jsou savci. • Žádný pták není savec. 95
• • • • • • •
Zvířaty jsou ptáci a dále savci kromě lidí. Ptáci mají peří a zobák. Savci kromě lidí mají čtyři nohy. Ptáci a lidé mají dvě nohy. Kočky mají rády ptáky. Pepík má rád všechna zvířata. Karlík má rád všechny savce kromě koček.
Dotazy: • • • •
Kdo Kdo Kdo Kdo
má má má má
dvě nohy? koho rád? rád toho, kdo má jeho rád? (tj. u koho je tato vlastnost obousměrná?) rád někoho dvounohého?
Příklad 15: Přepište následující věty na program v Prologu a formulujte uvedené dotazy. • • • • • • • • • • •
Mája a Vilík jsou včelky. Mája je pilná, zatímco Vilík je líný. Bzučilka je pilná včelka. Honza je včelař, do jeho úlu patří Mája a Vilík. Pepa je včelař, do jeho úlu patří Bzučilka. Neexistuje nikdo, kdo by byl zároveň pilný i líný. Včelky umí létat. Kdo nasbírá málo medu, je hladový. Pilné včelky nasbírají hodně medu, líné včelky nasbírají málo medu. Včelař, do jehož úlu patří nějaké hladové včelky, nasbírá málo medu. Včelař, který nenasbírá málo medu, nasbírá hodně medu.
Dotazy: • • • •
Kdo Kdo Kdo Kdo
nasbírá málo medu? nasbírá hodně medu? je hladový? vlastní úl, do něhož patří Mája?
Poznámka: V předposlední větě potřebujeme umístit tutéž anonymní proměnnou na dvě místa v jedné klauzuli (obdoba existenční konstanty v klauzulární logice). To se řeší přidáním znaku za podtržítko, tedy anonymní proměnná je proměnná začínající podtržítkem.
96
Příloha B Řešení příkladů V této příloze je řešení příkladů, jejichž zadání najdeme v příloze A. Při řešení nepřímým důkazem je obvykle použita lineární metoda, stejně jako v Prologu. U některých příkladů je také přepis do Prologu. V tomto přepisu některé klauzule předlohy v klauzulární logice nejsou přepsány, protože narozdíl postupu výpočtu v znalostní bázi klauzulární logiky Prolog pracuje s uzavřeným světem – nemusíme v programu dávat na vědomí, že určitý objekt nějakou vlastnost nemá, stačí, když není uvedeno, že tuto vlastnost má. Rovněž je zde ukázáno řešení některých problémů, které přináší trochu jiný způsob výpočtu Prologu, zejména striktní tvar Hornových klauzulí a tím i řešení negace v některých případech, kdy Prolog odmítá převzít tvar klauzule podle klauzulární logiky (negace v hlavě klauzule) nebo podává jiné než očekávané výsledky (například nekonečný výpočet). Řešení 1: Predikáty: okridleny(< kdo >) lehka kostra(< kdo >) umi(< kdo >, < co >) leta(< kdo >)
odpociva(< kdo >) je(< kdo >, < kde >) potrebuje(< kdo >, < co >)
Znalostní báze a přímé odvození prvního tvrzení: 1. 2. 3. 4. 5. 6.
odpociva(motyl) → je(motyl, kvetina) → okridleny(motyl) → lehka kostra(motyl) → okridleny(pstros) lehka kostra(pstros) → okridleny(X), lehka kostra(X) → umi(X, letat) 97
SA1 SA2 SA3 SA4 SA5 SA6
7. 8. 9. 10. 11.
umi(X, letat) → leta(X), odpociva(X) okridleny(X), je(X, Y ) → potrebuje(X, Y ) umi(@c, letat) → umi(X, letat) → okridleny(X) odpociva(X) →
SA7 SA8 SA9 SA10 SA11
12. okridleny(X), lehka kostra(X) → leta(X), odpociva(X) 13. okridleny(X), lehka kostra(X) → leta(X)
R(6,7) R(11,12)
Nepřímé odvození druhého tvrzení: PM S(12){pstros/X} R(5,13)
12. → lehka kostra(X) 13. → lehka kostra(pstros) 14. → Řešení 2: Predikáty: hospodynka(< kdo >, < jaka >) skace(< kdo >, < pro co >, < kam >) zraneni(< kdo >, < jake >) Znalostní báze a přímé odvození: 1. 2. 3. 4. 5.
→ hospodynka(jana, dobry) → skace(jana, pirko, pres plot) zraneni(jana, boule) → hospodynka(X, dobry) → skace(X, pirko, pres plot) skace(X, Y, pres plot) → zraneni(X, zlom noha), zraneni(X, boule)
SA1 SA2 SA3 SA4 SA5
6. hospodynka(jana, dobry) → skace(jana, pirko, pres plot) S(4){jana/X} 7. → skace(jana, pirko, pres plot) R(1,6) 8. skace(jana, pirko, pres plot) → zraneni(jana, zlom noha), zraneni(jana, boule) S(5){jana/X, pirko/Y } 9. → zraneni(jana, zlom noha), zraneni(jana, boule) R(7,8) 10. → zraneni(jana, zlom noha) R(3,9) Nepřímé odvození (navazujeme na znalostní bázi): 6. zraneni(jana, zlom noha) → PM (popírající množina) 7. skace(jana, pirko, pres plot) → zraneni(jana, zlom noha), zraneni(jana, boule) S(5){jana/X, pirko/Y } 98
8. 9. 10. 11. 12.
skace(jana, pirko, pres plot) → zraneni(jana, boule) hospodynka(jana, dobry) → skace(jana, pirko, pres plot) hospodynka(jana, dobry) → zraneni(jana, boule) → zraneni(jana, boule) →
R(6,7) S(4){jana/X} R(8,9) R(1,10) R(3,11)
Řešení 3: Predikáty: kresli(< kdo >, < kam >) dite(< kdo >) dospely(< kdo >)
trest(< kdo >, < jaky >) place(< kdo >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11.
→ kresli(mraz, okno) → dite(jana) → dite(pepik) → dospely(patrik) → kresli(jana, zed) → kresli(pepik, papir) → kresli(patrik, zed) kresli(X, zed) → potrestan(X) dospely(X), potrestan(X) → trest(X, vezeni) dite(X), potrestan(X) → trest(X, zakaz vecernicka) dite(X), trest(X, zakaz vecernicka) → place(X)
12. dite(X), trest(X, zakaz vecernicka) → 13. 14. 15. 16. 17. 18. 19. 20.
dite(jana), trest(jana, zakaz vecernicka) → trest(jana, zakaz vecernicka) → dite(jana), potrestan(jana) → trest(jana, zakaz vecernicka) dite(jana), potrestan(jana) → potrestan(jana) →R(2,16) kresli(jana, zed) → potrestan(jana) kresli(jana, zed) → →
99
SA1 SA2 SA3 SA4 SA5 SA6 SA7 SA8 SA9 SA10 SA11 PM S(12){jana/X} R(2,13) S(10){jana/X} R(14,15) S(8){jana/X} R(17,18) R(5,19)
Pokud nebudeme důsledně používat lineární metodu, bude pro tento příklad řešení kratší: 12. dite(X), trest(X, zakaz vecernicka) → 13. 14. 15. 16. 17.
PM R(10,12) R(8,13) S(14){jana/X} R(2,15) R(5,16)
dite(X), potrestan(X) → dite(X), kresli(X, zed) → dite(jana), kresli(jana, zed) → kresli(jana, zed) → →
Program v Prologu: kresli(mraz,okno). dite(jana). dite(pepik). dospely(patrik). kresli(jana,zed). kresli(pepik,papir). kresli(patrik,zed). potrestan(X) :- kresli(X,zed). trest(X,vezeni) :- dospely(X),potrestan(X). trest(X,zakaz_vecernicka) :- dite(X),potrestan(X). place(X) :- dite(X),trest(X,zakaz_vecernicka). Dotazy: ?????-
kresli(X,Y). place(X). kresli(_,zed). dite(X),potrestan(X). trest(_,Trest).
Řešení 4: Predikáty: mys(< kdo >) kocka(< kdo >) pes(< kdo >)
honi(< kdo >, < koho >) vidi(< kdo >, < koho >) zvire(< kdo >)
boji se(< kdo >, < koho >) pohybuje se(< kdo >, < jak >) utika(< kdo >)
Znalostní báze a nepřímé odvození: 1. → mys(jerry) 2. → kocka(tom)
SA1 SA2 100
3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. 17.
→ kocka(smoky) → pes(baryk) → vidi(jerry, tom) → vidi(smoky, baryk) → vidi(baryk, smoky) kocka(X) → zvire(X) mys(X) → zvire(X) pes(X) → zvire(X) pes(X), kocka(X) → mys(X), kocka(Y ) → boji se(X, Y ) kocka(X), pes(Y ) → boji se(X, Y ) utika(X) → pohybuje se(X, rychle) boji se(X, Y ), vidi(X, Y ), zvire(X) → utika(X) boji se(Y, X), vidi(X, Y ) → honi(X, Y ) honi(X, @c) → pohybuje se(X, rychle)
SA3 SA4 SA5 SA6 SA7 SA8 SA9 SA10 SA11 SA12 SA13 SA14 SA15 SA16 SA17 PM
18. pohybuje se(X, rychle) → 19. 20. 21. 22. 23. 24. 25. 26. 27.
utika(X) → R(14,18) boji se(X, Y ), vidi(X, Y ), zvire(X) → R(15,19) vidi(X, Y ), zvire(X), mys(X), kocka(Y ) → R(12,20) vidi(jerry, tom), zvire(jerry), mys(jerry), kocka(tom) → S(21){jerry/X, tom/Y } zvire(jerry), mys(jerry), kocka(tom) → R(5,22) mys(jerry) → zvire(jerry) S(4){jerry/X} mys(jerry), kocka(tom) → R(23,24) kocka(tom) → R(1,25) → R(2,26)
Program v Prologu: mys(jerry). kocka(tom). kocka(smoky). pes(baryk). vidi(jerry,tom). vidi(smoky,baryk). vidi(baryk,smoky). zvire(X) :- kocka(X). zvire(X) :- mys(X). zvire(X) :- pes(X).
(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) 101
boji_se(Kdo,Koho) :- mys(Kdo),kocka(Koho). boji_se(Kdo,Koho) :- kocka(Kdo),pes(Koho). pohybuje_se(X,rychle) :- utika(X). utika(X) :- boji_se(X,Y),vidi(X,Y),zvire(X). honi(X,Y) :- boji_se(Y,X),vidi(X,Y). pohybuje_se(X,rychle) :- honi(X,_).
(12) (13) (14) (15) (16) (17)
Klauzuli číslo 11 nepřepisujeme, protože Prolog pracuje v uzavřeném světě. Dotazy: ?????-
vidi(X,tom). zvire(X),pohybuje_se(X,rychle). utika(_). boji_se(Kdo,Koho). honi(Kdo,Koho).
Řešení 5: Predikáty: strom(< strom >, < jaky >) barva(< co >, < barva >)
ma listi(< co >, < kdy >) ma jehlici(< co >, < kdy >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10.
→ strom(javor, listnaty) → strom(borovice, jehlicnaty) → strom(modrin, jehlicnaty) strom(X, listnaty), strom(X, jehlicnaty) → strom(X, listnaty) → ma listi(X, leto) strom(X, jehlicnaty) → ma jehlici(X, leto) strom(X, listnaty), ma listi(X, zima) → → ma jehlici(borovice, zima) ma listi(X, leto) → barva(X, zelena) ma jehlici(X, leto) → barva(X, zelena)
11. barva(javor, zelena) → 12. 13. 14. 15. 16.
SA1 SA2 SA3 SA4 SA5 SA6 SA7 SA8 SA9 SA10 PM
ma listi(javor, leto) → barva(javor, zelena) ma listi(javor, leto) → strom(javor, listnaty) → ma listi(javor, leto) strom(javor, listnaty) → → 102
S(9){javor/X} R(11,12) S(5){javor/X} R(13,14) R(1,15)
Přepis znalostní báze na program v Prologu: strom(javor,listnaty). strom(borovice,jehlicnaty). strom(modrin,jehlicnaty). ma_listi(X,leto) :- strom(X,listnaty). ma_jehlici(X,leto) :- strom(X,jehlicnaty). ma_jehlici(borovice,zima). barva(X,zelena) :- ma_listi(X,leto). barva(X,zelena) :- ma_jehlici(X,leto).
(1) (2) (3) (5) (6) (8) (9) (10)
Klauzule číslo 4 a 7 nemusíme přepisovat, protože Prolog pracuje v uzavřeném světě. Řešení 6: Predikáty: zije ve vode(< kdo >, < jaka >) vodni zivocich(< kdo >) potrebuje(< kdo >, < co >) Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7.
→ zije ve vode(zralok, slany) → zije ve vode(delf in, slany) → zije ve vode(kapr, sladky) zije ve vode(X, slany) → vodni zivocich(X) zije ve vode(X, sladky) → vodni zivocich(X) vodni zivocich(X) → potrebuje(X, voda) → zije ve vode(@c, slany)
SA1 SA2 SA3 SA4 SA5 SA6 SA7
8. potrebuje(kapr, voda) → 9. 10. 11. 12. 13.
PM S(6){kapr/X} R(8,9) S(5){kapr/X} R(10,11) R(3,12)
vodni zivocich(kapr) → potrebuje(kapr, voda) vodni zivocich(kapr) → zije ve vode(kapr, sladky) → vodni zivocich(kapr) zije ve vode(kapr, sladky) → →
Přepis znalostní báze na program v Prologu: (1) (2)
zije_ve_vode(zralok,slany). zije_ve_vode(delfin,slany). 103
zije_ve_vode(kapr,sladky). vodni_zivocich(X) :- zije_ve_vode(X,slany). vodni_zivocich(X) :- zije_ve_vode(X,sladky). potrebuje(X,voda) :- vodni_zivocich(X).
(3) (4) (5) (6)
Sedmou klauzuli již nemusíme přepisovat do Prologu, protože vyplývá z první a druhé klauzule. Řešení 7: Popírající množinu vytvoříme přepisem negace závěru z predikátové logiky: ¬∃x(zije ve vode(x, slany) &potrebuje(x, voda)) ⇔ ⇔ ∀x(¬zije ve vode(x, slany) ∨ ¬potrebuje(x, voda)) Nepřímé odvození: 8. 9. 10. 11. 12. 13. 14. 15.
zije ve vode(X, slany), potrebuje(X, voda) → zije ve vode(zralok, slany), potrebuje(zralok, voda) → potrebuje(zralok, voda) → vodni zivocich(zralok) → potrebuje(zralok, voda) vodni zivocich(zralok) → zije ve vode(zralok, slany) → vodni zivocich(zralok) zije ve vode(zralok, slany) → →
PM S(8){zralok/X} R(1,9) S(6){zralok/X} R(10,11) S(4){zralok/X} R(12,13) R(1,14)
Pokud nebudeme používat důsledně lineární metodu: 8. 9. 10. 11. 12. 13.
zije ve vode(X, slany), potrebuje(X, voda) → vodni zivocich(X), zije ve vode(X, slany) → zije ve vode(X, slany), zije ve vode(X, slany) → zije ve vode(X, slany) → zije ve vode(@c, slany) → →
PM R(6,8) (unifikace) R(1,9) KK(10) S(11){@c/X; 1} R(7,12)
Krok 12 důkazu si můžeme dovolit, protože množina univerza diskurzu je zjevně neprázdná, obsahuje prvky zralok, delf in, kapr, voda, slany, sladky. Řešení 8: Predikáty: zije kde(< kdo >, < kde >) je v lese(< kdo >) potka(< kdo >, < koho >)
sezran(< kdo >) utika(< kdo >) liska(< kdo >)
104
zajic(< kdo >) kralik(< kdo >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10.
→ liska(bystrouska) → kralik(f erda) → zajic(usak) → je v lese(f erda) → potka(f erda, bystrouska) sezran(f erda) → liska(X) → zije kde(X, les) zajic(X) → zije kde(X, les) kralik(X) → zije kde(X, dvur) zije kde(X, dvur), je v lese(X), potka(X, Y ), liska(Y ) → sezran(X), utika(X)
11. utika(f erda) →
SA1 SA2 SA3 SA4 SA5 SA6 SA7 SA8 SA9 SA10 PM
12. zije kde(f erda, dvur), je v lese(f erda), potka(f erda, Y ), liska(Y ) → sezran(f erda), utika(f erda) S(10){f erda/X} 13. zije kde(f erda, dvur), je v lese(f erda), potka(f erda, Y ), liska(Y ) → sezran(f erda) R(11,12) S(9){f erda/X} 14. kralik(f erda) → zije kde(f erda, dvur) 15. kralik(f erda), je v lese(f erda), potka(f erda, Y ), liska(Y ) → sezran(f erda) R(13,14) R(2,15) 16. je v lese(f erda), potka(f erda, Y ), liska(Y ) → sezran(f erda) 17. potka(f erda, Y ), liska(Y ) → sezran(f erda) R(4,16) 18. potka(f erda, bystrouska), liska(bystrouska) → sezran(f erda) S(17){bystrouska/Y } 19. liska(bystrouska) → sezran(f erda) R(5,18) 20. → sezran(f erda) R(1,19) 21. → R(6,20) Přepis znalostní báze na program v Prologu: (1) (2) (3) (4) (5) (6) (7)
liska(bystrouska). kralik(ferda). zajic(usak). je_v_lese(ferda). potka(ferda,bystrouska). sezran(X) :- X=ferda,!,fail. zije_kde(X,les) :- liska(X). 105
zije_kde(X,les) :- zajic(X). zije_kde(X,dvur) :- kralik(X). utika(X) :zije_kde(X,dvur),je_v_lese(X), potka(X,Y),liska(Y), not(sezran(X)).
(8) (9)
(10)
Při přepisu 6. klauzule byly použity dva vestavěné predikáty Prologu fail a !. Predikát fail má tu dobrou vlastnost, že je vždy vyhodnocen jako f alse, predikát ! se nazývá predikát řezu a slouží k „odříznutíÿ dalších možných generovaných řešení (je vyhodnocen jako true, tedy uspěje, ale znemožní navracení). Všechny tyto vestavěné predikáty jsou probírány ve volitelném kurzu Praktikum z logického programování. Prologovská klauzule sezran(X) :- X=ferda,!,fail. znamená: „Jestliže je dotyčný Ferda, pak není pravda, že je sežrán, a žádné další možnosti není dovoleno zkoušet.ÿ Poznámka: dikátu not:
Predikát fail v kombinaci s predikátem řezu je použit při definování pre-
not(X) :- call(X),!,fail. not(X). To znamená: Nejdřív je zavolán cíl X pomocí vestavěného predikátu call/1 (ten jenom zavolá – „spustíÿ – svůj argument). Dále se pokračuje podle toho, jakou pravdivostní hodnotu vrátí vyhodnocení call(X): true : díky predikátu fail první klauzule vrátí hodnotu f alse a díky predikátu ! vyhodnocování predikátu not(X) nepokračuje, tedy not(X) je vyhodnoceno jako f alse, f alse : v první klauzuli vyhodnocování nedojde až k predikátu řezu ! a tedy při navracení pokračujeme k druhé klauzuli, kterou lze s cílem unifikovat vždy a protože je to fakt bez předpokladů, cíl je vyhodnocen jako true. Řešení 9: Predikáty: namornik(< kdo >) umi(< kdo >, < co >) je kde(< kdo − co >, < kde >) Znalostní báze a nepřímé odvození: 1. 2. 3. 4.
→ namornik(pepa) → namornik(honza) namornik(rudolf ) → namornik(@c) → umi(@c, plavat)
SA1 SA2 SA3 SA4 106
5. 6. 7. 8.
namornik(X) → je kde(X, lod) namornik(X), je kde(X, reka) → → je kde(lod, more), je kde(lod, reka) je kde(X, Y ), je kde(Y, Z) → je kde(X, Z)
PM
9. je kde(pepa, more) → 10. 11. 12. 13. 14. 15. 16. 17. 18. 19. 20. 21. 22. 23. 24.
SA5 SA6 SA7 SA8
je kde(pepa, Y ), je kde(Y, more) → je kde(pepa, more) je kde(pepa, Y ), je kde(Y, more) → namornik(pepa) → je kde(pepa, lod) je kde(pepa, lod), je kde(lod, more) → namornik(pepa), je kde(lod, more) → je kde(lod, more) → → je kde(lod, reka) je kde(X, lod), je kde(lod, reka) → je kde(X, reka) je kde(X, lod) → je kde(X, reka) namornik(X) → je kde(X, reka) namornik(pepa) → je kde(pepa, reka) → je kde(pepa, reka) namornik(pepa), je kde(pepa, reka) → namornik(pepa) → →
S(8){pepa/X, more/Z} R(9,10) S(5){pepa/X} S(11){lod/Y } R(12,13) R(1,14) R(7,15) S(8){lod/Y, reka/Z} R(16,17) R(5,18) S(19){pepa/X} R(1,20) S(6){pepa/X} R(21,22) R(1,23)
Řešení 10: Predikáty: bylozravec(< kdo >) vsezravec(< kdo >) masozravec(< kdo >)
selma(< kdo >) ji(< kdo >, < co >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7.
→ selma(liska) selma(zajic) → vsezravec(zajic) → selma(X) → masozravec(X) masozravec(X) → selma(X) ji(X, rostliny) → bylozravec(X), vsezravec(X) → masozravec(X), ji(X, rostliny)
107
SA1 SA2 SA3 SA4 SA5 SA6 SA7
8. → selma(@c)
SA8
9. bylozravec(zajic) →
PM
10. 11. 12. 13. 14. 15. 16.
ji(zajic, rostliny) → bylozravec(zajic), vsezravec(zajic) ji(zajic, rostliny) → vsezravec(zajic) → masozravec(zajic), ji(zajic, rostliny) → masozravec(zajic) selma(zajic) → masozravec(zajic) selma(zajic) → →
S(6){zajic/X} R(9,10) S(7){zajic/X} R(11,12) S(4){zajic/X} R(13,14) R(2,15)
Řešení 11: Predikáty: zije(< kdo >, < kde >) ma(< kdo >, < co >) dycha(< kdo >, < co >)
kytovec(< kdo >) ryba(< kdo >) obojzivelnik(< kdo >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13.
→ kytovec(delf in) → kytovec(vorvan) → ryba(stika) → obojzivelnik(zaba) kytovec(X) → zije(X, voda) ryba(X) → zije(X, voda) obojzivelnik(X) → zije(X, voda) kytovec(X), ma(X, zabra) → zije(X, voda) → ma(X, zabra), ma(X, plice) ma(X, plice) → dycha(X, vzduch) obojzivelnik(X) → ma(X, zabra) obojzivelnik(X) → ma(X, plice) ryba(X) → ma(X, zabra)
14. dycha(X, vzduch) → 15. 16. 17. 18.
SA1 SA2 SA3 SA4 SA5 SA6 SA7 SA8 SA9 SA10 SA11 SA12 SA13 PM
ma(X, plice) → zije(X, voda) → ma(X, zabra) kytovec(X) → ma(X, zabra) kytovec(delf in) → ma(delf in, zabra) 108
R(10,14) R(9,15) R(5,16) S(17){delf in/X}
19. 20. 21. 22.
R(1,18) S(8){delf in/X} R(19,20) R(1,21)
→ ma(delf in, zabra) kytovec(delf in), ma(delf in, zabra) → kytovec(delf in) → →
Přepis znalostní báze na program v Prologu: kytovec(delfin). kytovec(vorvan). ryba(stika). obojzivelnik(zaba). zije(X,voda) :- kytovec(X). zije(X,voda) :- ryba(X). zije(X,voda) :- obojzivelnik(X). ma(X,plice) :zije(X,voda), not(ma(X,zabra)). dycha(X,vzduch) :- ma(X,plice). ma(X,zabra) :- obojzivelnik(X). ma(X,plice) :- obojzivelnik(X). ma(X,zabra) :- ryba(X).
(1) (2) (3) (4) (5) (6) (7) (9) (10) (11) (12) (13)
Klauzuli číslo 8 nemusíme přepisovat, protože Prolog pracuje v uzavřeném světě. Řešení 12: Predikáty: ranni ptace(< kdo >) doskace(< kdo >, < kam >) ptak(< kdo >)
clovek(< kdo >) vlastni(< kdo >, < co >) sportovec(< kdo >)
Znalostní báze a nepřímé odvození: 1. 2. 3. 4. 5. 6. 7. 8. 9.
→ ptak(skrivan) → ranni ptace(skrivan) → ptak(sova) ranni ptace(sova) → → clovek(pepa) → ranni ptace(pepa) → sportovec(lida) → vlastni(lida, trampolina) → clovek(honza)
SA1 SA2 SA3 SA4 SA5 SA6 SA7 SA8 SA9 109
10. 11. 12. 13. 14. 15.
→ vlastni(honza, papousek) → vlastni(honza, trampolina) sportovec(honza) → sportovec(X) → clovek(X) ranni ptace(X) → doskace(X, dal) sportovec(X), vlastni(X, trampolina) → doskace(X, dal)
SA10 SA11 SA12 SA13 SA14 SA15
16. ptak(X), doskace(X, dal) → 17. 18. 19. 20. 21.
PM S(16){skrivan/X} R(1,17) S(14){skrivan/X} R(18,19) R(2,20)
ptak(skrivan), doskace(skrivan, dal) → doskace(skrivan, dal) → ranni ptace(skrivan) → doskace(skrivan, dal) ranni ptace(skrivan) → →
Přepis na program v Prologu: ptak(skrivan). ranni_ptace(skrivan). ptak(sova). clovek(pepa). ranni_ptace(pepa). vlastni(lida,trampolina). sportovec(lida). clovek(honza). vlastni(honza,papousek). vlastni(honza,trampolina). clovek(X) :- sportovec(X). doskace(X,dal) :- ranni_ptace(X). doskace(X,dal) :sportovec(X), vlastni(X,trampolina).
(1) (2) (3) (5) (6) (7) (8) (9) (10) (11) (13) (14) (15)
Klauzule číslo 4 a 12 nepřepisujeme, protože Prolog pracuje s uzavřeným světem. Dotazy: ?????-
clovek(X). doskace(X,dal). ranni_ptace(X). sportovec(_). ptak(X),not(ranni_ptace(X)).
110
Řešení 13: Predikáty: teplota(< stupnu >) pocasi(< jake >) pracuje(< kdo >, < prace >)
cestar(< kdo >) snehulak(< kdo >) misto nosu(< kdo >, < maco >)
Program v Prologu: teplota(-5). pocasi(snezi). cestar(luda). cestar(honza). snehulak(ferda). misto_nosu(klapka,mrkev). prace(honza,vypravi_pohadky). snehulak(X) :- misto_nosu(X,mrkev). snehulak(X) :- misto_oci(X,uhliky). pocasi(mraz) :- teplota(X),X<0. prace(X,odhrnuje_snih) :- pocasi(mraz),pocasi(snezi),cestar(X). Dotazy: ?????-
pocasi(X). cestar(X),prace(X,Y). snehulak(X). prace(luda,_). prace(honza,Prace).
Řešení 14: Predikáty: kocka(< kdo >) papousek(< kdo >) sova(< kdo >)
clovek(< kdo >) ptak(< kdo >) savec(< kdo >)
zvire(< kdo >) ma(< kdo >, < co >) pocet nohou(< kdo >, < kolik >)
Program v Prologu: kocka(micka). papousek(karlik). papousek(hvezdicka). sova(houkalka). clovek(pepik). ptak(X) :- papousek(X). ptak(X) :- sova(X). savec(X) :- kocka(X). 111
savec(X) :- clovek(X). zvire(X) :- ptak(X). zvire(X) :- savec(X),not(clovek(X)). ma(X,peri) :- ptak(X). ma(X,zobak) :- ptak(X). pocet_nohou(X,4) :- savec(X),not(clovek(X)). pocet_nohou(X,2) :- ptak(X). pocet_nohou(X,2) :- clovek(X). ma_rad(Y,X) :- ptak(X),kocka(Y). ma_rad(pepik,X) :- zvire(X). ma_rad(karlik,X) :- savec(X),not(kocka(X)). Ostatní věty není nutné přepisovat do Prologu, protože ten pracuje s uzavřeným světem. Dotazy: ????-
pocet_nohou(X,2). ma_rad(Kdo,Koho). ma_rad(X,Y),ma_rad(Y,X). ma_rad(X,Y),pocet_nohou(Y,2).
Řešení 15: Predikáty: vcelka(< kdo >) vcelar(< kdo >) pilny(< kdo >)
liny(< kdo >) hladovy(< kdo >) umi(< kdo >, < co >)
patri do ulu(< kdo >, < vlastnik >) nasbira(< kdo >, < co >, < kolik >)
Program v Prologu: vcelka(maja). pilny(maja). vcelka(vilik). liny(vilik). vcelka(bzucilka). pilny(bzucilka). vcelar(honza). vcelar(pepa). patri_do_ulu(maja,honza). patri_do_ulu(vilik,honza). patri_do_ulu(bzucilka,pepa). umi(X,letat) :- vcelka(X). hladovy(X) :- nasbira(X,med,malo). nasbira(X,med,hodne) :- pilny(X),vcelka(X). 112
nasbira(X,med,malo) :- liny(X),vcelka(X). nasbira(X,med,malo) :vcelar(X), patri_do_ulu(_y,X), vcelka(_y),hladovy(_y). nasbira(X,med,hodne) :vcelar(X), not(nasbira(X,med,malo)). Dotazy: ????-
nasbira(X,med,malo). nasbira(X,med,hodne). hladovy(X). patri_do_ulu(maja,X).
113
Rejstřík α-pravidlo, 43, 46 β-pravidlo, 43, 46 δ-pravidlo, 46 γ-pravidlo, 46 algoritmus výpočtu v Prologu, 85 algoritmus zjištění unifikátoru, 64 atom bázový, 49 atom splnitelný, 53 axiomy, 8, 9, 12, 27, 38, 43, 45, 70 axiomy speciální, 66, 70 backtracking, 85 bezespornost Hilbertovského s. VL, 35 bezespornost SPD PL, 26 bezespornost SPD VL, 23 báze znalostní, 66, 70 Colmerauer, A., 75 cíl, 85 denotace, 52 disjunkce atomů v klauzuli, 56 dotaz, 76, 84 dualizace, 41 důkaz, 5, 13, 15, 28, 38, 43, 46, 72, 73 důkaz alternativní, 36 důkaz hypotéza nepřímá, 17 důkaz hypotéza přímá, 16 důkaz nepřímý, 15, 73 důkaz přímý, 13, 72 důkaz větvený s hypotézami nepřímý, 18 důkaz větvený s hypotézami přímý, 17 důkaz z dokazatelných formulí, 36 důkazové metody sémantické analýzy, 4 důkazy, 7
důsledek dvojice klauzulí, 62 fakt v klauzulární logice, 49 fakt v Prologu, 76 fakt v znalostní bázi, 67 formule duální, 42 formule splnitelná, 3 funktor existenční, 48 funktor Skolemův, 48 generování do generování do Gentzenovský Gentzenovský
hloubky, 82 šířky, 82 systém PL, 45 systém VL, 43
Hilbertovský axiomatický systém PL, 38 Hilbertovský axiomatický systém VL, 27 hlava pravidla, 76 hypotéza, 16 jazyk deklarativní, 84 klauzule, 47, 49 klauzule cílová, 76, 85, 86 klauzule Hornovy, 47, 76, 85 klauzule Hornovy zobecněné, 47 klauzule logicky platná, 53 klauzule nepravdivá ve struktuře, 53 klauzule nesplnitelná, 53 klauzule platná ve struktuře, 53 klauzule pravdivá ve struktuře, 53 klauzule prázdná, 55, 81, 88 Klauzulární axiomatický systém, 70 klauzulární logika, 47 konjunkce atomů v klauzuli, 56 konstanta existenční, 48 konstanta Skolemova, 48 114
kontradikce, 3 korektnost Gentzenovského s. PL, 46 korektnost Gentzenovského s. VL, 45 korektnost Hilbertovského s. PL, 39 korektnost Hilbertovského s. VL, 33 korektnost Klauzulárního ax. systému, 74 korektnost SPD PL, 25 korektnost SPD VL, 20 korektnost sémantická, 9 lemma o neutrální formuli, 21, 31 logika klauzulární, 47 metoda lineární, 82, 84 minimálnost Hilbertovského s. VL, 35 množina formulí splnitelná, 3 množina klauzulí nesplnitelná, 81 množina neshod, 64 množina popírající, 59 množina sporná, 11, 70 model formule, 3 model znalostní báze, 69 modus ponens, 27, 38, 71 modus tolens, 71 navracení, 85 negace atomů, 57 negace klauzule, 58 negace v Prologu, 79 ohodnocení proměnné, 52 ohodnocení termu, 52 pravdivost klauzulí, 53 pravidla dedukční, 12, 23 pravidla odvozovací, 8, 27, 38, 43, 46, 70 pravidlo dedukční E∃, 23 pravidlo dedukční E∀, 23 pravidlo dedukční ED, 12 pravidlo dedukční EE, 12 pravidlo dedukční EI, 12 pravidlo dedukční EK, 12 pravidlo dedukční MP, 12 pravidlo dedukční Z∃, 23
pravidlo dedukční Z∀, 23 pravidlo dedukční ZD, 12 pravidlo dedukční ZE, 12 pravidlo dedukční ZI, 12 pravidlo dedukční ZK, 12 pravidlo odvozovací, 5 pravidlo odvozovací existenční substituce, 71 pravidlo odvozovací G, 38 pravidlo odvozovací MP, 27, 38 pravidlo odvozovací rezoluční, 62, 70, 81, 82 pravidlo odvozovací substituce, 70 pravidlo pomocné EN, 16, 30 pravidlo pomocné K, 16, 30 pravidlo pomocné KD, 16 pravidlo pomocné kontrakce, 71 pravidlo pomocné logické zákony, 71 pravidlo pomocné PO, 30, 37 pravidlo pomocné přeuspořádání atomů, 71 pravidlo pomocné rezoluce, 19 pravidlo pomocné SM, 15, 31 pravidlo pomocné T, 16 pravidlo pomocné TI, 14, 30, 36 pravidlo pomocné Z∀, 39 pravidlo pomocné ZN, 16, 31 pravidlo v Prologu, 76 pravidlo v znalostní bázi, 67 predikát not, 79 predikát rovnosti, 59, 71, 80 predikát řezu, 106 program v Prologu, 76 programování logické, 75 prohledávání do hloubky, 83, 84 prohledávání do šířky, 83 Prolog, 75 proměnná anonymní, 78, 96 rezoluce, 4, 6, 62, 81, 85, 86 rezoluce v logickém programování, 81 rezoluční řez, 62, 70 rezolventa, 81, 85, 86 Robinsonův rezoluční princip, 81 strom sémantický, 4 115
strom výpočetní lineární, 82 struktura, 52 struktura aplikovatelná, 52, 69 substituce, 13, 60, 70, 71 substituce existenční, 61, 71 syntaxe jazyka klauzulární logiky, 48 syntaxe Prologu, 78 systém formální, 8 systém formální axiomatický, 9, 27, 41, 70 systém formální bezesporný, 11 systém formální minimální, 11 systém formální předpokladový, 9, 12, 41 systém formální sporný, 11 Systém přirozené dedukce PL, 23 Systém přirozené dedukce VL, 12 sémantika jazyka klauzulární logiky, 52
zákony logické, 71 zásobník, 85, 86 úplnost Gentzenovského s. PL, 46 úplnost Gentzenovského s. VL, 45 úplnost Hilbertovského s. PL, 39 úplnost Hilbertovského s. VL, 33 úplnost SPD PL, 26 úplnost SPD VL, 23 úplnost sémantická, 9 úsudek deduktivní, 4
tablo duální, 44 tablo sémantické, 4, 5, 10, 44 tabulka sémantická, 4 tautologie, 3 term bázový, 49, 52 tvrzení existenční, 50 tvrzení univerzální, 49 tělo pravidla, 76 unifikace, 63, 84–86 unifikátor, 63 unifikátor nejobecnější, 64, 71, 84 unifikátor obecnější, 64 univerzum diskurzu, 52 uzávěr rezoluční, 81 valuace aplikovatelná, 52 valuace proměnné, 52 valuace termu, 52 věta o dedukci, 13, 28 věta o implikaci, 28 věta o substituci, 13 věta Postova, 33 zacyklení výpočtu, 84 zobrazení denotační, 52 zákon logický, 53 116
