IV130	Přínosy	a	rizika	
inteligentních	systémů
31. března 2023
Logičtí aktéři, vyvozování
Logičtí	(znalostní)	aktéři
• Aktéři	si	vytvářejí	reprezentaci	světa
• Z	reprezentace	světa	vyvozují	nové	informace
• Tyto	informace	dále	využívají	ke	svým	akcím
• Logičtí	(znalostní)	aktéři	dávají	dohromady	obecné	znalosti	s	
konkrétními	znalostmi	z	pozorování	světa	(smyslových	vstupů)
• Odvozování může	odhalovat	skryté	vlastnosti	světa	(prostředí)
• Reprezentace	znalostí jako	množina	vět	(sentencí)	v	jazyce	
reprezentace	znalostí	
• Sentence	bez	odvození	se	nazývá	axiómem
• Operace	TELL	přidává	tvrzení	do	znalostní	báze	
• Operace	ASK	ze	znalostní	báze	vybírá	odpověď,	která	vyplývá	z	
obsahu znalostí	báze	spolu	s	tím,	co	do	ní	přidaly	operace	TELL
• Znalostní	bázi si	udržuje	aktér,	na	počátku	může	obsahovat	nějaké	
obecné	znalosti
Logika	znalostního	aktéra
• Vhodná	syntax pro	vyjadřování	sentencí
• Sémantika definující	význam	sentencí,	zejména	pak	jejích	pravdivost	vzhledem	k	
možnému	světu	(stavu	světa,	modelu)
• Pokud	je	sentence	pravdivá	v	modelu,	pak	říkáme,	že	model	splňuje	tuto	sentenci	
(nebo	je	to	model	té	sentence)
• Ze	sentence α plyne	sentence	β,	pokud	každý model	splňující	α splňuje	také	β
• Vyplývání	lze	využít	k	odvozování	důsledků;	Vyvozování	je	formální	cesta,	jak	tyto	
důsledky	hledat
• Korektní	vyvozování	odvozuje	pouze	takové	sentence,	které	vyplývají	z	výchozích
• Obsahuje-li	znalostní	báze	pravdivé	sentence	o	reálném	světě,	dává	korektní	
vyvozování	pouze	sentence,	které	jsou	rovněž	pravdivé:	
Obrázky a schémata z RussellNorwig:
AI A Modern Approach, 4th
ed., 2021
Výroková	logika
• Z	hlediska	logických	operací	jsou	vyhodnocení	sentencí	v	tomto	jazyce	dány	
pravdivostními	tabulkami:
• Odvozování	generováním	důsledků	enumerace	pravdivostní	tabulky,	tzv.	ověřování	
modelů	(model	checking)
• Odvozovací	pravidla,	zejména	pak	rezoluční	metoda
Dokazování	ve	výrokové	logice
• Dokazování	teorémů	vyvozování	přímo	na	úrovni	sentencí
• Logické	ekvivalence	sentencí
• Odvozovací	pravidla:
• Modus	ponens					α	⇒ β,		α |=	β
• Eliminace	konjunkce:		α ∧ β |= α
• Pravidla	na	bázi	logických	ekvivalencí
Odvozování	ve	výrokové	logice
• Věta	(sentence)	je	splnitelná,	pokud	je	pravdivá	v	nějakém	
modelu.							Příklad:	A	∨ B,	C
• Věta	(sentence)	je	nesplnitelná,	pokud	není	pravdivá	v	žádném	
modelu.							Příklad:	A	∧ ¬A
• Logický	důsledek	lze	převést	na	testování	splnitelnosti,	protože	
KB	╞ α	právě	tehdy,	když	je	(KB	∧ ¬α)	nesplnitelná.	(Důkaz	se	
vede	pomocí	zamítnutí	nebo	sporem:	Ověřování,	zda	α	je	
logickým	důsledkem	KB	lze	tedy	převést	na	problém	testování	
splnitelnosti	(KB	∧ ¬α).)
• Výrokové	formule	v	konjunktivní	normální	formě	(CNF):
Ø literál je	výroková	proměnná	nebo	její	negace
Ø Klauzule je	disjunkce	literálů
vFormule	v	CNF	je	konjunkce	klauzulí
• Každou	formuli	lze	převést	do	CNF.
Rezoluční	odvozování	ve	výrokové	logice
• Rezoluční algoritmus dokazuje nesplnitelnost formule (KB ∧ ¬α) převedené
do CNF opakovanou aplikací rezolučního pravidla,
• To ze dvou klauzulí obsahujících komplementární literály (P a ¬P)
• vytvoří novou klauzuli:
• ℓi a mj jsou	komplementární	literály.
• Příklad:
• Algoritmus	končí	pokud
• nelze	přidat	žádnou	další	klauzuli,	a	pak	¬	KB╞ α),	nebo
• vznikla	prázdná	klauzule,	a	pak	KB╞ α	
• Jde	o úplný	a	korektní	algoritmus
• Úplné je i používání jedné z klauzulí z oporné množiny T ⊆ S takové, že S−T je
bezesporná (např. pochází z bezesporných axiómů).
Rezoluční	odvozování	ve	výrokové	logice
Hornovy	klauzule
• Klauzule odpovídající implikacím P1∧ .	.	.	∧ Pn→	Q ,	kde	žádný	z	P1,	. .	., Pn ,	Q
není negativní
• V množinovém zápise mají klauzule tvar { Q, ¬P1 , . . . , ¬Pn } ,
• Hornova klauzule s právě jedním pozitivním literálem se nazývá
programová klauzule. Namísto {	Q,	¬P1 ,	.	.	.	,	¬Pn }	bývá	v	kontextu	logického	
programování	zvykem	ji	zapisovat	ve	tvaru:		Q	←	P1 ,…,Pn
• Taková	klauzule	se	nazývá	pravidlem pro	n	>	0;	nebo	faktem pro	n	=	0	(její	zápis	je	
pak	Q	zvýrazněně	Q	←)
• Hornova	klauzule	bez	pozitivních	literálů,	tj.	{	¬P1 ,	.	.	.	,	¬Pn}	či	←	P1 ,…,Pn,	se	
nazývá	cílem (cílovou	klauzulí).
• Cíle	a	fakta	spolu	interagují	při	vytváření	důkazů	nesplnitelnosti	množin	Hornových	
klauzulí:	bez	obou	z	nich	je	lib.	množina	Hornových	klauzulí	splnitelná.
• Pro	Hornovy	klauzule	jsou	úplnými	metodami	jednotková	rezoluce (aspoň	jedna	z	
použitých	klauzuilí	musí	být	jednoprvková)	i	lineární	rezoluce (alespoň	jedna	z	
klauzulí	je	ze	vstupní	množiny	klauzulí,	tj.	KB	bez	dalších	odvozování).
Hornovy	klauzule
• Gramatika pro Hornovy klauzule:
Hornovy	klauzule	- dopředné řetězení
• Dopředné řetězení:
• Z dostupných faktů odvozujeme pomocí Hornových klauzulí všechny možné
závěry dokud vznikají nové fakty resp. dokud nedokážeme platnost dotazu.
• U každé klauzule si pamatujeme počet předpokladů, který se zmenší, když
je předpoklad dokázán.
• Klauzule s nula (zbývajícími) předpoklady slouží k dokázání hlavy klauzule.
• Postup řízený daty v KB.
• Jde o korektní a úplný algoritmus pro Hornovy klauzule
• Lineární časová složitost v rozměru báze znalostí KB
• Zpětné řetězení:
• Pro daný dotaz hledáme rozdělení pomocí Hornovy klauzule na poddotazy,
které se řeší stejným způsobem.
• Postup řízený dotazem
Logiky	za	výrokovou	logikou
• Zachycení vlastností objektů, relací, funkcí a vlastností
• Ontologické zakotvení jazyka logiky – co se předpokládá o stavebních
kamenech vyjadřování a vyvozování
Jazyky Ontologické	zakotvení	(co	
ve	světě	existuje)
Epistemiologické	zakotvení	(co	aktér	
věří	o	faktech)
Výroková	logika fakta true/false/unknown
Logika	prvního	řádu fakta,	objekty,	relace true/false/unknown
Temporální	logika fakta,	objekty,	relace,	časy true/false/unknown
Pravděpodobnostní	logika fakta stupeň	víry	z	intervalu	[0,1]	
Fuzzy	logika Fakta	se	stupněm	pravdy	z	
[0,1]	
známý	interval	hodnot
Predikátová	logika	1.řádu
• Rozšířený jazyk:
• Kvantifikátory
• Funkční syboly
• Predikáty
• Operace TELL dává do
znalostní báze:
Ø Axiómy (fakta)
Ø Definice (tvrzení ve
traru ekvivalencí)
Ø Teorémy (lze odvodit z
jiných, ale může
zrychlovat vyvozování)
• Operace ASK:
Ø Dotazy na obsah
databáze
Ø Odvozování dalších
vlastností pro objekty
dotazu
Ø Instanciace objektů, pro
něž platí nějaká
vlastnost
Predikátová	logika	1.řádu
• konstanty (jména objektů):
Ø Richard, John, Koruna
Ø Funkční symbol: LeváNoha
• Termy (jiný způsob
pojmenování objektu):
Ø Levánoha(John)
• Predikátové symboly:
Ø Bratr, NaHlavě, Osoba, Král,
Koruna
• Atomická tvrzení (popis relace
mezi objekty):
Ø Bratr(Richard,John)
• Složená tvrzení:
Ø Král(Richard) ∨ Král(John)
Ø ¬Král(Richard) ⇒ Král(John)
• Tvrzení o výběru objektů
(kvantifikátory):
Ø ∀x Král(x) ⇒ Osoba(x)
Ø ∃x Koruna(x) ∧
NaHlavě(x,John)
Ø ∀x,y Bratr(x,y) ⇒ Bratr(y,x)
Ø ∃x,y Bratr(x,Richard) ∧
Bratr(y,Richard)
Ø ∃x,y Bratr(x,Richard) ∧
Bratr(y,Richard) ∧ ¬(x=y)
Obrázky a schémata z RussellNorwig:
AI A Modern Approach, 4th
ed., 2021
Predikátová	logika	1.řádu
Ø Skolemizace pro práci s kvantifikátory (zachovává splnitelnost)
Ø Unifikace pro hledání instancí umožňujících rezoluční krok (instancí
vedoucích k vygenerování kontradikce)
Ø Herbrandovy intepretace definující „symbolické“ interpretace bez ohledu na
konkreétní problémovou doménu
Ø Specifikace vyjádřené logikou prvního řádu lze „uzemnit“ resp.
„propozicionalizovat“ vygenerováním všech možných základních instancí
formulí zahrnujících proměnné (resp. kvantifikátory) – znamená to ovšem
obrovskou extenzi prohledávaného stavového prostoru: substitucí je typicky
nekonečně mnoho
Ø Výroková i predikátová logika mají zásadní slabiny ve zvládání nejasně
vymezených propozic
Predikátová	logika	1.řádu
Ø Skolemizace pro práci s kvantifikátory (zachovává splnitelnost)
Predikátová	logika	1.řádu
Ø Unifikace pro práci s funkcemi a proměnnými
Predikátová	logika	1.řádu
Ø Unifikace pro práci s funkcemi a proměnnými
Predikátová	logika	1.řádu
Predikátová	logika	1.řádu
Efektivní	hledání	rezolučních	důkazů
• Jednotková rezoluce:
Ø Snahou je získat prázdnou klauzuli, proto je dobré, pokud se nově
odvozené klauzule zkracují
Ø Preferujeme rezoluční krok, kde je jedna z klauzulí jednotková (obsahuje
jediný literál)
Ø Obecně omezení pouze na jednotkové rezoluce není úplné, ale pro
Hornovy klauzule ano (tam je to dopředné řetězení)
• Množina podpory:
Ø Vybrané klauzule, z nichž alespoň jedna se vždy účastní rezoluce (výsledek
rezoluce se přidává do množiny podpory, která neobsahuje spor)
Ø Počáteční množina podpory typicky obsahuje negovaný dotaz
• Vstupní rezoluce:
Ø Každého rezolučního kroku se účastní alespoň jedna klauzule ze vstupu
počáteční KB nebo dotaz
Ø Nejde o úplnou metodu
• Subsumce:
Ø Eliminujeme klauzule, které jsou zahrnuty jinými klauzulemi
Ø Je-li v bázi znalostí P(x), je zbytečné přidávat P(A) ani P(A) ∨ Q(B)
Rozšíření	základní	podoby	rezolučních	důkazů
• Zpracování	rovnosti	vyžaduje	redukci	prohledávaného	stavového	prostoru	pomocí	
techniky	demodulace a	paramodulace
• Rezoluce	na	Hornových	klauzulích	se	dá	využít	jako	programovací	jazyk	(Prolog	a	
další)
• Systémy	logického	programování	založené	na	zpětném	řetězení	využívají	
důmyslných	kompilačních	technik	a	velmi	efektivní	odvozování;	handicapem	je	
citlivost	zpětného	řetězení	na	nekonečné	cykly	a	redundantní	odvozování
• Dopředné	řetězení	se	využívá	v	deduktivních	databázích	a	produkčních	systémech,	
je	to	metoda,	která	je	úplná	pro	jazyk	Datalog,	který	tímto	způsoberm	pracuje	v	
polynomiálním	čase	
• Automatizované	dokazování	je	již	prakticky	použitelným	nástrojem,	který	umožnil	
jak	rekonstrukci	starších	výsledků	(Gödelova	věta	o	neúplnosti,	1986),	tak	výsledků	
nových	(Např.	Keplerova	domněnka	o	minimálním	objemu	poskládaných	koulí,	
2005,	resp.	2017