Prostředky umělé inteligence
Predikátová logika
© 2004, doc. RNDr. Ing. Tomáš Březina, CSc.
Jazyk predikátové logiky			
Formule predikátové logikyvznikají z atomických formúl		pomocí logických spojek	
a kvantifikátorů. Za základní se obvykle berou logické	spojky konjunkce a		, disjunkce
v, implikace —» a negace —i.			
Každá atomická formule je formule.			
• Jsou—li ee, ß formule, pak výrazy			
\a/\ß\, ícev/?], fee—»/?], —,a,			
jsou rovněž formule.			
• Je—li a formule a X proměnná, výrazy			
MXa, 3Xa			
jsou rovněž formule.			
• Jiné formule neexistují.			
Formální systém matematické logiky
Je představován
•  Jazykem predikátové logiky
•  Axiomy
•  Odvozovacími pravidly
Term  /  a formule a  jazyka predikátové logiky lze považovat za slova (řetězce) v abecedě tvořené symboly uvažovaného jazyka a značkami a,v,—»,—i,V,3,(,).
Precedence operátorů
^,V,3,/\v,-»
Jazyk predikátové logiky		
Syntaxe predikátové logiky je soubor pravidel pro popis	objektů termy. Termy se	
skládají z proměnných, funkcí a konstant. Nejjednodušší vztahy mezi termy,		kterým
lze přiřadit pravdivostníhodnotu (true/false) vyjadřuj	atomické formule	pomoci
predikátů.		
Predikát		
• odpovídá relaci,		
• podle počtu termů může být unární, binární, ternární.		
Atomickou formuli tvoří predikát s volbou termů v argumentech.		
Pozn.:		
Výčet všech konstant, funkcí a predikátů se specifikuje jazyk konkrétní predikátové		
logiky.		
Jazyk predikátové logiky
•  Konstanty obvykle reprezentují konkrétní objekty.
•  Volba predikátůje dána vztahy, které chceme používat.
•  Funkce se používají pro přiřazení objektů jiným objektům.
Pozn.:
•  Umožňují formulovat (speciální) axiomy.
•  Obvykle se definuje nějaký pevně zvolený systém speciálních axiomů, který vymezuje uvažované prostředí
Formální systém matematické logiky
•  Je—li term / tvaru fítJ.,,...,O, pak podtermyjsou termy t t ...jn. Totéž platí pro všechny podtermy těchto termů.
•  Formule ß je podformulí, je-li ß podřetězcem formule ee, který je současně formulí.
•  Daný výskyt proměnné X ve formuli a je vázaný, jestliže je součástí nějaké podformule tvaru \/Xß nebo 3Xß. Proměnná je vázaná ve formuli a, má-li v ní vázaný výskyt. Není-li daný výskyt proměnné X vázaný, je volný. Proměnná je volná ve formuli a, má-li tam volný výskyt.
•  Formule je otevřená, neobsahuje-li žádnou vázanou proměnnou.
•  Formule je uzavřená, neobsahuje-li žádnou volnou proměnnou.
1
Formální systém matematické logiky
Formule s čistými proměnnými ye formule, v níž není žádná proměnná současně volná i vázaná.
Všechny proměnné, které nejsou explicitně kvantifikovány ve formuli jsou volné proměnné, tj. lze za ně dosadit libovolný term. Formule vzniklá dosazením se nazývá //ifte/ic/původní formule.
Normální tvary formulí
Ke každé formuli (p predikátové logiky lze nalézt ekvivalentní formuli (p (mají stejné pravdivostní hodnoty ve stejných situacích) v konjunktivně-disjunktivním tvaru (KDF). Základním představitelem KDF vez kvantifikátorů je klauzule.
Klauzule
•  je konečná disjunkce literálů (atomických formulí nebo jejich negací),
•  všechny proměnné klauzule jsou považovány za volné.
Formální systém matematické logiky
• Přímý důkaz = používá odvozovací pravidla a axiomy k získání odvozované formule, t Nepřímý důkaz = důkaz, že speciální axiomy jsou ve sporu s negací dokazované formule.
Rezoluční metoda
Pozn.:
•  Pro libovolnou množinu formulí (teorii M) lze nalézt odpovídající reprezentaci ve formě množiny klauzulí.
•  Pro důkaz, že v nějaké teorii M obsahující axiomy ve tvaru základních klauzulí platí klauzule a. vce.v...\/ani stačí ukázat, že teorie M'=M>u —iIcc. vce, v...vcera I je sporná. V klauzulárním tvaru teorie je M', M'=MKJÍ—Ia.,—Ia2,...,an\/
■ kde —i —i\ß\\ je pro libovolnou formuli ß je nahrazeno formulí ß.
Formální systém matematické logiky
Zvláštním případem klauzule je prázdná klauzule [ ] s pravdivostní hodnotou false.
Konjunktivně disjunktivní forma je konjunkcí klauzulí. Může obsahovat kvantifikátory.
Prenexní normální forma obsahuje kvantifikátory pouze na začátku formule. Formule, která z ní vznikne odtržením kvantifikátorů je bekvantifikátorové jádro.
Ke každé formuli existuje její bezkvantifikátorové jádro v konjunktivní normální formě.
Klauzule lze považovat za univerzální vyjadřovací prostředek predikátové logiky formulí s univerzálními kvantifikátory. Existenční kvantifikátory se eliminují tzv. Skolemizací, získá se Skolemův variant původní funkce.
Rezoluční metoda
Rezoluční metoda je metodou hledání sporu v konečné množině klauzulí (nepřímá metoda).
T\->oc právě tehdy,když Tu —,[a)\ jesporná.
Rezoluce je úplná dokazovací metoda (tj. je schopna nalézt spor v každé sporné množině klauzulí), proto lze rezoluci považovat za univerzální metodu důkazu vhodnou pro hledání důkazu).
Mechanismus rezoluční metody
Spočívá v odvozování rezolvent pomocí rezolučního pravidla vždy ze dvou rodičovských klauzulí a jejich přidávání do teorie v klauzulárním tvaru M'.
• Přitom je každá rezolventa je logickým důsledkem rodičovských klauzulí, a tedy i celé výchozí množiny klauzulí. Hledáme-li zamítnutí, máme v každém kroku k dispozici konečnou množinu klauzulí, která je sjednocením výchozí množiny a všech jejích dosud vytvořených rezolvent. Z této množiny lze obecně vytvořit ne jednu, ale konečně mnoho dalších rezolvent.
■ Důkaz sporu je dokončen, podaří-li se odvodit prázdnou klauzuli, která je sama nesplnitelná a má pravdivostní hodnotu false. Vtom případě mluvíme o zamítnutí výchozí množiny klauzulí. Délka důkazu podstatně závisí na tom, které z možných rezolvent budeme postupně vybírat. Hovoříme o volbě strategie.
Pozn.:
Pro stručnost je někdy výhodné klauzule zapisovat jako množiny literálů.
Robinsonova věta
Libovolná množina klauzulí je sporná právě tehdy, je-li  z ní odvoditelná prázdná klauzule po konečném počtu použití obecného rezolučního pravidla.
•  Pro libovolný (tedy nejen rezoluční) algoritmus, který zjišťuje, zda zvolená formule je důsledkem vstupní množiny klauzulí, neexistuje žádné časové omezení pro délku jeho práce.
•  Pokud je nějaká formule dokazatelná, pak algoritmus skončí, ale obecně nelze předem určit kdy.
Pozn.:
Jde o důsledek slavné Gódelovy věty o neúplnosti.
Rezoluční metoda / Pravidlo základní rezoluce
•  Výchozí   množina   klauzulí   obsahuje   jen   základní   klauzule   (tj.   klauzule   bez proměnných).
•  Může být utvořena např. z libovolných uzavřených instancí obecných klauzulí.
Pravidlo:
Jsou - li cp a y/ dvě základní klauzule a je - li a atomická formule bez proměnných, pak z dvojice klauzulí av<p a -iav(c lze odvodit rezolventu <p\/if/ formulí av<p a -navi//. Literály a a -na, které umožnily vzájemně rezolvovat obě uvažované formule, se nazývají doplňkovými literály.
Pozn.:
•  Vychází z pravidla „modus ponens", tj. rezolventa libovolné (konečné) množiny klauzulí M je splněna v každém modelu teorie M.
•  Pokud z výchozí množiny M  odvodíme rezolucí prázdnou klauzuli, pak teorie M nemůže mít žádný model (je sporná).
•  Je-li teorie M sporná, pak v ní lze pomocí základní rezoluce odvodit prázdnou klauzuli.
Unifikace
Pro zobecněnou rezoluci  má zásadní význam nejobecnější unifikace pro zvolenou
konečnou množinu výrazů \e\      tj. substituce 5 za volné proměnné studovaných
I.   l\iel výrazů taková, že:
i) pro všechny výrazy £., E   platí, že EJs\=E ís\,
ii) pro libovolnou substituci u, splňující rovněž podmínku i) platí, že existuje substituce v taková, že pro každý výraz E ,^\eA     platí \E (s) \(v)=E .(«), čili u=s.v .
Zobecněná rezoluce
Používá pravidlo obecné rezoluce.
Uvažujme dvě klauzule (p a i// takové, že nemají společné proměnné. Nechť existují neprázdné klauzule (p., i//, a (p2, 1//, takové, zeje splněno:
•  <P^<P2 fe<P aVivV2 Je V'
•  existuje nejobecnější unifikace 5 literálů z q>l a negací z literálů 1//. Takové rodičovské klauzule (p a i// lze rezolvovat, výsledkem je klauzule (pJsy/y/ [s\, kterou nazýváme výsledná klauzule.
Pozn.:
Tytéž dvě klauzule mohou být obecně rezolvovány více rozdílnými způsoby.
	Zobecněná rezoluce / Příklad Teorie M je představována dvěma formulemi Ai, A2. Má být v teorii M dokazatelná. Teorie M a formule C v klauzulárním tvaru		zjištěno, je - li formule C
	Al:	"Někteří pacienti maií radi iakéhokoliv doktora."	
		3X(P(X)r,yr(D(r)^R(xj)))	
		-nDir^vRia^)	
	A2:	"Zádnv pacient nemá rad mastičkáře."	
		VX(P(X)^VT(M(T) ->^R(X,T)))	
		^(X2)v^VÍ(72)v^R(X2,72)	
	C:	"Žádný doktor není mastičkář."	
	^C:	■     ....■■■■  ■    -     :...■  ■■■	
		D(a2) M(a2)	
			
Zobecněná rezoluce / Příklad
Aplikace rezoluční metody
1.	Ai:	P{<$	
2.	A,:	-UTJvRfa^)	
3.	A2:	-P(X2)v^M(T2)v^R(X2,T2)	
4.	^C:	D(a2)	
5.	^C:	M(a2)	
6.	4.,2.	R(ara2)	a2/7l
7.	6.,3.	-P(ai)v^á(a2)	VX2 a2ir2
8.	7.,5.	-P^)	
9.	8..1.	U	
Rezoluční zamítnutí
Strategie zamítnutí může být
•  úplná: pokud je prázdná klauzule z výchozí množiny odvoditelná, vede na sestrojení prázdné klauzule;
•  neúplná: nemusí vést na sestrojení prázdné klauzule, i když tato je odvoditelná.
Derivační graf
•  rezolventa je spojena hranami s oběma svými rodiči,
•  listy grafu jsou výchozí klauzule,
•  kořen grafu je prázdná klauzule.
Rezoluční zamítnutí je podgraf derivačního grafu, jehož
•  listy jsou výchozí klauzule,
•  kořen je prázdná klauzule.
Řád rezolventy
•  je 0 pro vstupní rezolventu
•  je i, je-li aspoň jeden z rodičů řádu i - 1
	Rezoluční zamítnutí/ Příklad Teorie M a formule C v klauzulámím tvaru		
	A,:	"Každý, kdo umí dokazovat věty, se nedá napálit."	
		VJf(Z)(JO->-JV(JO)	
		-DfX^v-NfXJ	
	A2:	"Roztržití lidé se dají napálit."	
		VX(R(X)->N(X))	
		-R(X2)vN(X2)	
	A3:	"Někteří roztržití lidé isou inteligentní."	
		3x(R(xyi(xy>	
		«(«;) /(«;)	
	C:	"Jsou inteligentní lidé, kteří neumí dokazovat věty."	
	^C:	^3X(I(Xy,^D(X)))	
		-I(X3)vD(X3)	
			
Rezoluční zamítnutí / Příklad
Aplikace rezoluční metody
1.	Ai:	-ßCArpv-jvcjTj)	
2.	A2:	^R(X2)viV(X2)	
3.		R(<\)	
4.	A3:	K<\)	
5.	^C:	-I(X3)vD(X3)	
6.	5.,4.	DfaJ	"l/X3
7.	6.,1.	^(Oj)	a1/X1
8.	7.,2.	-^(<\)	a1ÍX1
9.	8.,3.	u	
Rezoluční zamítnutí / strategie
Strategie prohledávání do šířky
postupně se generují všechny rezolventy i-tého řádu. Rezolventy /+l-tého řádu jsou generovány až tehdy, až jsou vygenerovány všechny rezolventy /-tého řadu.
Strategie podporné množiny
V každé   výchozí   množině   klauzulí  je   možné   určit   podmnožinu,   která   je   sama
bezesporná. Rezolventy dvojic z této podmnožiny nemohou vést ke sporu.
Strategie podpůrné množiny generuje rezolventy jen z takových rodičovských párů, kdy
jeden z rodičů je odvozen od negace dokazovaného tvrzení. Je tak buď přímo klauzulí,
která vznikla  při negaci dokazovaného tvrzení, nebo má takovou klauzuli za svého
předchůdce.
Pozn.:
•  Postupuje se do šířky.
•  Důkaz může být delší, při prohledávání do šířky.
•  Počet rezolvent všech řádů roste pomaleji u prohledávání do šířky.
Rezoluční zamítnutí / strategie
Jednotko vá strategie
generuje  rezolventy z párů, ve kterých je alespoň jeden  z rodičů klauzule tvořená jediným literálem.
Pozn.:
•  Není úplná strategie.
•  strategii lze chápat jako modifikaci podpůrné množiny, ve které se prohledávání do šířky zjemňuje jednotkovou preferencí.
Rezoluční zamítnutí/ strategie
Vstupní strategie
generuje rezolventy z párů, ve kterých je alespoň jeden  z rodičů  přímo  z výchozí množiny klauzulí.
Pozn.:
•  Není úplná strategie.
•  Jednoduchá a ve většině případů velmi efektivní.
•  Existují různá rozšíření do úplné strategie.
Rezoluční zamítnutí / strategie
Filtrační strategie
Dvě klauzule a, ß mohou být rodiči rezolventy, je—li
•  a nebo ß ze vstupní množiny nebo
•  a ani ß nejsou ze vstupní množiny, ale v derivačním grafu je buď a předchůdcem ß, nebo ß je předchůdcem a.
Pozn.:
•  Jde o rozšíření vstupní strategie do úplné strategie.
Rezoluční zamítnutí / strategie
Pozn.:
•  Některé z uvedených strategií je možné kombinovat.
•  Časté spojení strategie podpůrné množiny se vstupní nebo filtrační strategií (každá z nich svým způsobem omezuje množinu rezolvent, ale neurčuje pořadí pro jejich generovánO-
•  Většina strategií má řadu dalších zjemnění, které nějakým způsobem určují pořadí generovaných rezolvent. Nejjednodušším příkladem je jednotková preference (dává přednost rezolventám z jednotkových klauzulí). Další strategie využívají různých typů uspořádání literélů a klauzulí.
Omezování množiny rezolvent / Horn
Hornovy klauzule
jsou klauzule, které obsahují nejvýše jeden pozitivní literal.
Hornova logika
•  formule transform ovatel n é na konjunkce Hornových klauzulí,
•  vlatní podmnožina predikátové logiky,
•  lze ji velmi efektivně zpracovávat,
•  používá ji "logické programování" (PROLOG).
Rezoluční zamítnutí/ strategie
Lineární strategie
generuje rezolventy z párů, ve kterých je jeden z rodičů poslední generovaná klauzule.
Pozn.:
•  strategií existuje několik
•  nejde o úplné strategie
použití v interaktivních systémech dokazování vět
Omezování množiny rezolvent
Každá strategie prohledávání generuje i rezolventy, které z různých důvodů nemohou přispět k důkazu sporu. Některé jsou z nich snadno identifikovatelné. Tím, že se vynechají, se dále zmenší prohledávaný prostor.
Např.:
• Tautologie (obsahují doplňkový pár literálů) nemají žádný podíl na nesplnitelnosti množiny, lze je vypustit.
•  Eliminace na základě logických hodnot literálů (až po substituci konstant) klauzulí, které obsahují literály s pravdivostní hodnotou true, zkracovat klauzule o literály, jejichž pravdivostní hodnota je false.
•  Eliminace se může provést, je li jedna klauzule důsledkem jiné. říkáme, že klauzule y. zahrnuje klauzuli y , jestliže pro nějakou substituci 5 platí yJs)czy (klauzule chápeme jako množiny literálů).
Umělá inteligence a logika
•  Matematická logika je prostředek reprezentace znalostí.
•  Zásadní princip budování logiky pro strojové dokazování je její monotónnost
ír \-^ <p\-> ír* h^ <p\ a ír* 3 f\
Je—li (p dokazatelná v teorii T, pak je dokazatelná i v každé teorii T*zíT .
Pozn.:
•  Monotónnost vyjadřuje předpoklad, že čím více bude výchozích axiómů, tím více nových tvrzení lze dokázat.
*■ V běžném usuzování může být monotónnost na překážku.
5
Příklad
Teorie T =^^,^1 a formule C
I „Každý pták umí létat."
VX(P(X)^£(X))
-PÍXJvUXJ
'Tučňák ie pták."
vx(r(x)^p(x))
^r(x,)vP(x,)
'Quido je tučňák."
C:
T(Quido) I" Quido umí létat.
—iL(Quidój)
Tj. platí 7 ^C.
Aplikace rezoluční metody
1.	Ai:	^(X^vLťXj)	
2.	A2:	^r(x2)vP(x2)	
3.	A,:	T(Quido)	
4.	^C:	—L(Quido)	
5.	l.,4.	—P(Quido)	Quido IX
6.	5.,2.	—iT(Quido)	Quido 1X
7.	6.,3.	U	
Příklad
Tj. platí T*\—>—iC, ale současně, protože T""ziT , platí i T*l—>C . Tím jsme zjistili, že teorie T" obsahuje spor (její axiómy umožňují odvodit jak formuli, tak její negaci).
Příklad
Teorie T* = U,ArA3,Ail a formule -,C Aplikace rezoluční metody
A,:	"Každv pták umí létat."
	VX(P(X)^L(X))
	^(X^vLťXj)
A2:	"Tučňák ie pták."
	vx(r(x)^p(x))
	^r(x2)vP(x2)
A3:	"Ouido ie tučňák."
	T(Quido)
A,:	"Tučňáci nelátají. "
	VX(T(X)^^L(X))
	-,T(X3)v^L(X3)
C:	"Ouido neumí létat."
	—i(—L(Quido))
i.	Ai:	^(X^vLťXj)	
2.	A2:	-,T(X2)vP(X2)	
3.	A,:	T(Quido)	
4.	A,:	-,T(X3)v^L(X3)	
5.	^C:	L(Quido)	
6.	5.,4.	—T(Quidó)	Quido IX
8.	6.3.	U	
Neformální logiky
•  Univerzální tvrzení v běžném životě mají řadu nevyslovených (implicitních) předpokladů. Jeden ze zdrojů nemonotónního usuzování jsou výjimky. Tím jsou inspirovány další formální systémy, mj. nemonotónnílogika.
•  Jiným problémem je příliš „hrubá" rozlišovací schopnost pravdivostních hodnot true/false. Často se náš úsudek opírá o pravděpodobnostní hodnocení s daleko širší škálou hodnot (pravděpodobnostní logika). Se širší škálou hodnost pracuje také neostrá (fuzzy) logika.
•  Predikátová logika je vhodným prostředím uvažování pro určitý druh problémů. Pro jiné problémy se hledají a formalizují jiné modely. Spor o tom, zda je možné vybudovat inteligentní entitu pouze s použitím vhodného symbolického systému (logicistický přístup), či zda je nutné použití subsymbolických prvků jako jsou neuronové sítě (konekcionistickýpřístup).