.

0 (hodnocen0 x )

(18) Půjčeno:18x 

BK

Vyd. 1.

Brno : Computer Press, 2003

ix, 269 s. : il.

ISBN 80-251-0023-5 (brož.)

Obsahuje ilustrace, tabulky, předmluvu, dodatek, rejstřík, údaje o autorce a její fotografii

Bibliografie: s. 263-266

Inteligence umělá - logika formální - učebnice vysokošk.

Logika formální - inteligence umělá - učebnice vysokošk.

000033576

PŘEDMLUVA ix // 1 FORMÁLNÍ REPREZENTACE ZNALOSTÍ 1 // 1.1 ZNALOSTI A JEJICH REPREZENTACE 1 // 1.1.1 Data, informace, znalosti 1 // 1.1.2 Světy a jejich modely 1 // 1.1.3 Znalosti procedurální a deklarativní 2 // 1.1.4 Pojmy a jejich jazyková reprezentace 2 // 1.1.5 Modelování usuzování pomocí formálního jazyka 4 // 1.1.6 Formálni logika jako prostředek reprezentace znalostí 5 // 1.1.7 Formalizace - cesta ? automatizaci 5 // 1.2 FORMÁLNÍ JAZYK 6 // 1.2.1 Syntax formálního jazyka 6 // 1.2.2 Denotační sémantika formálního jazyka 6 // 1.2.3 Jazyk a metajazyk 7 // REPREZENTACE ZNALOSTI VÝROKOVOU LOGIKOU // 2.1. JAZYK L VÝROKOVÉ LOGIKY A JEHO EXPRESIVITA // 2.1.1 Výrok a jeho pravdivost // 2.1.2 Gramatika jazyka L výrokové logiky // 2.1.3 Konstrukce výrokové formule // 2.1.4 Stromová reprezentace a míry složitosti formule // 2.1.5 Spočenost množiny výrokových formulí // 2.2 SÉMANTIKA JAZYKA L VÝROKOVÉ LOGIKY // 2.2.1 Interpretace jazyka L výrokové logiky // 2.2.2 Valuace výrokových proměnných a interpretace formulí // 2.2.3 Interpretace formuli Booleovými funkcemi // 2.3 SPLŇOVÁNÍ A MODELY FORMULÍ // 2.3.1 Tabulková metoda sémantické analýzy výrokové formule // 2.3.2 Splnitelné formule, tautologie a kontradikce // 2.3.3 Modely formulí // 2.3.4 Dualita formulí // 2.3.5 Substituce // 2.4 NORMÁLNÍ FORMY VÝROKOVÝCH FORMULÍ // 2.4.1 Ekvivalence formuli // 2.4.2 Funkčně úplné množiny výrokových spojek // 2.4.3 Disjunktivní normální formy výrokových formuli // 2.4.4 Konjunktivní normální formy výrokových formulí // 2.5 ROZHODOVÁNÍ SPLNITEĽNOSTI VÝROKOVÝCH FORMULÍ // 2.5.1 Rozhodovací algoritmy // 2.5.2 Rozhodování sémantickými stromy // 2.5.3 Quineův rozhodovací algoritmus // 2.5.4 Nepřímé důkazy logické platnosti implikaci //

2.5.5 Rozhodovaní táhlovou a rezoluční metodou 37 // 2.6 LOGICKÉ DŮSLEDKY VÝROKOVÝCH FORMULÍ 38 // 2.6.1 Logický důsledek daných předpokladů 39 // 2.6.2 Teorie a její axiómy z hlediska sémantiky 39 // 3 FORMÁLNÍ DŮKAZY VE VÝROKOVÉ LOGICE 45 // 3.1 VLASTNOSTI FORMÁLNÍCH DŮKAZŮ 45 // 3.1.1 Jazyk, speciální axiómy a odvozovaci pravidla 45 // 3.1.2 Sémantická korektnost a úplnost důkazové metody 46 // 3.1.3 Přímé a nepřímé důkazy logických důsledků 46 // 3.2 REZOLUČNÍ FORMÁLNÍ DŮKAZY VE VÝROKOVÉ LOGICE 46 // 3.2.1 Jazyk LC rezolučního formálního systému 46 // 3.2.2 Rezoluční odvozovaci pravidlo 47 // 3.2.3 Rezoluční strom a rezoluční důkaz 49 // 3.2.4 Sémantická korektnost a úplnost rezolučního důkazu 51 // 3.2.5 Nepřímé formální důkazy rezolučním popřením 53 // 3.2.6 Přímé generování vět teorie 54 // 3.3 REZOLUCE A NEKONEČNÉ MNOŽINY KLAUZULÍ 56 // 3.4 TABLOVÉ FORMÁLNÍ DŮKAZY VE VÝROKOVÉ LOGICE 57 // 3.4.1 Jazyk táhlových důkazů ve výrokové logice 58 // 3.4.2 Sémantická korektnost a úplnost nepřímých táhlových důkazů 62 // 3.4.3 Logické důsledky a sémantické tablo ve výrokové logice 67 // 4 AXIOMATICKÉ SYSTÉMY VÝROKOVÉ LOGIKY 69 // 4.1 OBECNÉ VLASTNOSTI ... SYSTÉMŮ 69 // 4.1.1 Od sémantiky ? formálnímu generováni vět 69 // 4.1.2 Prostředky odvozování a dokazování 69 // 4.1.3 Jazyk axiomatického systému 71 // 4.1.4 Axiómy a odvozovaci pravidla 71 // 4.1.5 Požadavek sémantické korektnosti a úplnosti systému 74 // 4.1.6 Formální důkazy platnosti metajazykových schémat 75 // 4.2 GENTZENOVSKÝ AXIOMATICKÝ SYSTÉM G 75 // 4.2.1 Sémantická tabla duálních formulí 75 // 4.2.2 Jazyk, axiómy a odvozovaci pravidla systému G 77 // 4.2.3 Formální dedukce v systému G 79 // 4.2.4 Sémantická korektnost a úplnost systému G 83 //

4.3 KLAUZULÁRNÍ AXIOMATICKÝ SYSTÉM C 85 // 4.3.1 Axiómatický systém C ve vztahu k systému G 85 // 4.3.2 Jazyk, axiómy a odvozovaci pravidla systému C 85 // 4.3.3 Sémantická korektnost a úplnost systému C 87 // 4.4 HILBERTOVSKÝ AXIOMATICKÝ SYSTÉM H 87 // 4.4.1 Jazyk, axiómy a odvozovaci pravidla hilbertovského systému H 87 // 4.4.2 Důkazy vět v hilbertovském systému H 89 // 4.4.3 Sémantická korektnost a úplnost systému H 97 // 4.5 BEZESPORNOST V AXIOMATICKÝCH SYSTÉMECH VÝROKOVÉ LOGIKY 98 // 5 REPREZENTACE ZNALOSTÍ PREDIKÁTOVOU LOGIKOU 101 // 5.1 JAZYK LI PREDIKÁTOVÉ LOGIKY A JEHO EXPRESIVITA 101 // 5.1.1 Syntax jazyka LI predikátové logiky 104 // 5.1.2 Termy a jejich konstrukce 106 // / 5.1.3 Formule jazyka LI a její konstrukce 106 // 5.1.4 Formační strom a složitost predikátové formule 108 // 5.1.5 Proměnné a kvantifikátory 112 // 5.2 SÉMANTIKA JAZYKA LI 115 // 5.2.1 Interpretace jazyka LI 115 // 5.2.2 Struktura a pravidla interpretace jazyka LI 116 // 5.2.3 Použití funkci a predikátu rovnosti 123 // 5.2.4 Formule s kvantifikátory a jejich interpretace 124 // 5.3 KLAUZULÁRNÍ FORMA FORMULE JAZYKA LI 127 // 5.3.1 Některé platné vztahy formulí s kvantifikátory 127 // 5.3.2 Převod formule do prenexni normální formy 128 // 5.3.3 Klauzulámí forma formule, skolemizace 131 // 6 SPLNITELOST A LOGICKÝ DŮSLEDEK 137 // 6.1 SPLNITELNOST A PLATNOST PREDIKÁTOVÝCH FORMULÍ 137 // 6.1.1 Tabulková metoda sémantické analýzy formulí s kvantifikátory 142 // 6.2 MODELY A LOGICKÉ DŮSLEDKY 144 // 7 FORMÁLNÍ DII KAZY V PREDIKÁTOVÉ LOGICE 147 // 7.1 REZOLUČNÍ FORMÁLNÍ DŮKAZY PREDIKÁTOVÝCH FORMULÍ 147 // 7.1.1 Unifikace 147 // 7.1.2 Množina neshod 148 // 7.1.3 Unifikační algoritmus 150 // 7.1.4 Příklady predikátových rezolučních důkazů 152 //

// 7.2 TABLOVÉ FORMÁLNÍ DŮKAZY V PREDIKÁTOVÉ LOGICE 153 // 7.2.1 Jazyk táhlových důkazů v predikátové logice 153 // 7.2.2 Sémantické tablo formulí s vázanými proměnnými 154 // 7.2.3 Formální definice sémantického tabla 155 // 7.2.4 Sémantická korektnost a úplnost predikátového táhlového důkazu 158 // 7.2.5 Příklady predikátových táhlových důkazů 161 // 7.2.6 Sémantické tablo a logický důsledek 164 // 7.2.7 Vytvářeni teorií 167 // 7.2.8 Nekonečné generováni sémantického tabla 168 // 8 ROZHODNUTELNOST V PREDIKÁTOVÉ LOGICE 171 // 8.1 ČÁSTEČNÁ ROZHODNUTELNOST 171 // 8.2 HERBRANDOVA ROZHODOVACÍ PROCEDURA 171 // 8.2.1 Herbrandova struktura a model 172 // 8.2.2 Herbrandova věta 176 // 8.2.3 Analýza pomocí sémantického stromu 178 // 8.2.4 Nekonečné modely v predikátové logice 179 // 8.2.5 Herbrandova procedura a logický důsledek 180 // 9 AXIOMATICKÉ SYSTÉMY PREDIKÁTOVÉ LOGIKY 185 // 9.1 GENTZENOVSKÝ AXIOMATICKÝ SYSTÉM G1 185 // 9.1.1 Jazyk, axiómy a odvozovaci pravidla systému G1 185 // 9.1.2 Gentzenovské důkazy v systému G1 186 // 9.1.3 Sémantická korektnost a úplnost systému G1 191 // 9.2 HILBERTOVSKÝ AXIÓMATICKÝ SYSTÉM H1 193 // 9.2.1 Jazyk, axiómy a odvozovaci pravidla systému H1 .193 // 9.2.2 Další pomocná odvozovaci pravidla 195 // 9.2.3 Důkaz zpětným postupem (backward chaining) 198 // 9.2.4 Sémantická korektnost a úplnost systému H1 200 // 9.3 BEZESPORNOST V AXIOMATICKÝCH SYSTÉMECH PREDIKÁTOVÉ LOGIKY 201 // 10 REPREZENTACE ZNALOSTÍ KLAUZULÁRNÍ LOGIKOU 203 // 10.1 PREDIKÁTOVÁ A KLAUZULÁRNÍ LOGIKA 203 // 10.2 SYNTAX JAZYKA LÍC KLAUZULÁRNÍ LOGIKY 204 // 10.2.1 Gramatika jazyka LÍC klauzulámí logiky 204 // 10.2.2 Univerzální klauzule 206 // 10.2.3 Substituce termů za proměnné 207 // 10.2.4 Existenční kvantifikace v klauzulární logice 209 //

10.3 VÝZNAM PRVKŮ JAZYKA LÍC KLAUZULÁRNÍ LOGIKY 210 // 10.3.1 Struktura přiřazená jazyku LÍC klauzulámí logiky 210 // 10.3.2 Ohodnocení proměnných a vyhodnocení termů 211 // 10.3.3 Interpretace atomů 213 // 10.3.4 Interpretace klauzuli 215 // 10.4 EXPRESIVITA SPECIÁLNÍCH TYPŮ KLAUZULÍ 215 // 10.4.1 Klauzule bez antecedentu nebo konsekventu 215 // 10.4.2 Reprezentace negativních tvrzení 217 // 10.4.3 Konjunkce a disjunkce atomů v klauzuli 220 // 10.5 ZNALOSTNÍ BÁZE KLAUZULÁRNÍ LOGIKY A JEJÍ MODELY 222 // 10.5.1 Reprezentace znalostí znalostní bází 222 // 10.5.2 Fakta a prvky interpretujících relací 223 // 10.5.3 Předpoklad "uzavřeného světa" 223 // 10.5.4 Fakta a pravidla ve znalostní bázi 224 // 10.6 INTERPRETACE ZNALOSTNÍ BÁZE 225 // 10.6.1 Zamýšlená interpretace a aplikovatelné struktury 225 // 10.6.2 Příklady interpretace báze znalostí 226 // 10.7 MODELY A LOGICKÉ DŮSLEDKY BÁZE ZNALOSTÍ 228 // 10.7.1 Splnitelnost klauzule v dané struktuře 228 // 10.7.2 Model znalostní báze, logický důsledek 229 // 10.7.3 Logická platnost klauzule 233 // 10.7.4 Logické zákony s predikátem rovnosti 234 // 10.8 AXIOMATICKÝ SYSTÉM Cl KLAUZULÁRNÍ LOGIKY 236 // 10.8.1 Axiómy v klauzulárnim axiómatickém systému Cl 236 // 10.8.2 Odvozovaci pravidla v klauzulámí logice 237 // 10.8.3 Použiti dalších logických zákonů a odvozovacich pravidel 239 // 10.8.4 Odvozováni ze znalostní báze 240 // 10.8.5 Rezoluce v klauzulámí logice 241 // 10.9 PŘÍMÉ A NEPŘÍMÉ KLAUZULÁRNÍ ODVOZOVÁNÍ 244 // 10.9.1 Přímé a nepřímé odvozováni z bázových klauzuli 244 // 10.9.2 Popřeni klauzule s proměnnými a existenčními konstantami 247 // 10.9.3 Řešeni logických hádanek přímým postupem 250 // A DODATEK 259 // A.1 USPOŘÁDÁNÍ 259 // A.2 STROM 260 // LITERATURA 263 // REJSTŘÍK 267