IV130 Přínosy a rizika
inteligentních systémů
12. dubna 2024
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émantikadefinující význam sentencí, zejména pak jejích pravdivost vzhledem k
možnémusvě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 RussellNorw
ig: AIA 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ů
❖Formule 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 zapisovatve 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žinyklauzulí, 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 pravdyz
[0,1]
známý intervalhodnot
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 RussellNorw
ig: AIA 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éhoprostoru pomocí
techniky demodulace a paramodulace
• Rezoluce na Hornových klauzulích se dá využít jako programovací jazyk (Prolog a
další)
• Systémylogického programovánízaložené na zpětném řetězení využívají
důmyslnýchkompilač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)