Inference ve výrokové a predikátové logice
Aleš Horák
E-mail: hales@fi.muni.cz
http://nlp.fi.muni.cz/uui/
Obsah:
▶ Inference ve výrokové logice
▶ Inference v predikátové logice
▶ Shrnutí
Úvod do umělé inteligence 7/12 1 / 33
Inference ve výrokové logice
Logický agent – inference
připomínka – komponenty logického agenta:
inferenční stroj (inference engine)
báze znalostí (knowledge base)
algoritmy nezávislé na doméně
znalosti o doméně
inference – vyvozování důsledků z báze znalostí
KB ⊢i α . . . věta α může být vyvozena z KB pomocí (procedury) i
(i odvodí α z KB)
Bezespornost: i je bezesporná ⇔ ∀KB ⊢i α ⇒ KB |= α
Úplnost: i je úplná ⇔ ∀KB |= α ⇒ KB ⊢i α
Pokud je KB pravdivá v reálném světě ⇒ ∀ věta α vyvozená z KB
pomocí bezesporné inference je také pravdivá ve skutečném světě
Úvod do umělé inteligence 7/12 2 / 33
Inference ve výrokové logice
Historie logického vyvozování
450 př.n.l. stoikové výroková logika, inference (pravděpodobně)
322 př.n.l. Aristoteles inferenční pravidla, kvantifikátory
1565 Cardano teorie pravděpodobnosti (výroková logika + nejistota)
1847 Boole výroková logika (znovu)
1879 Frege predikátová logika 1. řádu
1922 Wittgenstein důkaz pomocí pravdivostních tabulek
1930 Gödel ∃ úplný algoritmus pro PL1
1930 Herbrand úplný algoritmus pro PL1 (redukce na výroky)
1931 Gödel ¬∃ úplný algoritmus pro aritmetiku
1960 Davis/Putnam “praktický” algoritmus pro výrokovou logiku
1965 Robinson “praktický” algoritmus pro PL1 – rezoluce
Úvod do umělé inteligence 7/12 3 / 33
Inference ve výrokové logice Inference kontrolou modelů
Inference ve Wumpusově jeskyni
situace:
– v [1, 1] nedetekováno nic
– krok doprava, v [2, 1] Vánek
uvažujeme možné modely pro ‘?’
(budou nás zajímat jen Jámy)
A
V
?
?
?
3 pole s Booleovskými možnostmi {T, F} ⇒ 23 = 8 možných
modelů
Úvod do umělé inteligence 7/12 4 / 33
Inference ve výrokové logice Inference kontrolou modelů
Modely ve Wumpusově jeskyni
uvažujeme všech 8 možných modelů:
1 2 3
1
2
Breeze
PIT
1 2 3
1
2
Breeze
PIT
1 2 3
1
2
Breeze
PIT PIT
PIT
1 2 3
1
2
Breeze
PIT
PIT
1 2 3
1
2
Breeze
PIT
1 2 3
1
2
Breeze
PIT
PIT
1 2 3
1
2
Breeze
PIT PIT
1 2 3
1
2
Breeze
KB
1
KB = pravidla Wumpusovy jeskyně + pozorování
α1 = “[1, 2] je bezpečné pole” KB |= α1
α2 = “[2, 2] je bezpečné pole” KB ̸|= α2
kontrola modelů → jednoduchý způsob logické inference
Úvod do umělé inteligence 7/12 5 / 33
Inference ve výrokové logice Inference kontrolou modelů
Pravdivostní tabulka pro inferenci
V1,1 V2,1 J1,1 J1,2 J2,1 J2,2 J3,1 KB α1
false false false false false false false false true
false false false false false false true false true
...
...
...
...
...
...
...
...
...
false true false false false false false false true
false true false false false false true true true
false true false false false true false true true
false true false false false true true true true
false true false false true false false false true
...
...
...
...
...
...
...
...
...
true true true true true true true false false
KB |= α1
KB = pravidla Wumpusovy jeskyně + pozorování
α1 = “[1, 2] je bezpečné pole”
Úvod do umělé inteligence 7/12 6 / 33
Inference ve výrokové logice Inference kontrolou modelů
Inference kontrolou modelů
Kontrola všech modelů do hloubky je bezesporná a úplná (pro konečný
počet výrokových symbolů)
function TT-Entails?(KB, α) # vrací True, pokud KB |= α
symbols ← list_of_symbols(KB ∪ α)
return TT-Check-All(KB, α, symbols, {})
function TT-Check-All(KB, α, symbols, model) # shoduje se α s KB na modelu?
if Empty?(symbols) then
if PL-True?(KB,model) then return PL-True?(α,model)
else return True # když je KB nepravdivá, vždy vrací True
else
P ← symbols.first
rest ← symbols.rest
return (...................TT-Check-All(KB,α,rest,model ∪ {P=True})
and
...................TT-Check-All(KB,α,rest,model ∪ {P=False}))
vrací true, pokud je Alpha pravdivá v Modelu
O(2n) pro n symbolů, NP-úplný problém
Úvod do umělé inteligence 7/12 7 / 33
Inference ve výrokové logice Inference kontrolou modelů
Inference kontrolou modelů
▶ kontrola modelů (model checking)
• procházení pravdivostní tabulky (vždycky exponenciální v n)
• vylepšené prohledávání s navracením (improved backtracking), např. DPLL
• heuristické prohledávání prostoru modelů (bezesporné, ale neúplné)
▶ aplikace inferenčních pravidel
• legitimní (bezesporné) generování nových výroků ze starých
• důkaz = sekvence aplikací inferenčních pravidel např. pravidla pro logickou
ekvivalenci
je možné použít inferenční pravidla jako operátory ve standardních
prohledávacích algoritmech
• typicky vyžaduje překlad vět do normální formy
Úvod do umělé inteligence 7/12 8 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Dopředné a zpětné řetězení
pokud KB = konjunkce Hornových klauzulí
⇒ můžeme použít dopředné a zpětné řetězení
Hornova klauzule =
výrokový symbol; nebo
(konjunkce symbolů) ⇒ symbol
např.: KB = C ∧ (B ⇒ A) ∧ (C ∧ D ⇒ B)
pravidlo Modus Ponens – pro KB z Hornových klauzulí je úplné
α1, . . . , αn, α1 ∧ · · · ∧ αn ⇒ β
β
algoritmy dopředného nebo zpětného řetězení jsou přirozené a mají
lineární časovou složitost vzhledem k velikosti báze znalostí
Úvod do umělé inteligence 7/12 9 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Dopředné řetězení
Idea: aplikuj pravidlo, jehož premisy jsou splněné v KB
přidej jeho důsledek do KB
pokračuj do doby, než je nalezena odpověď
KB:
P ⇒ Q
L ∧ M ⇒ P
B ∧ L ⇒ M
A ∧ P ⇒ L
A ∧ B ⇒ L
A
B
AND-OR graf KB:
Q
P
M
L
BA
Úvod do umělé inteligence 7/12 10 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Dopředné řetězení – příklad
P ⇒ Q
L ∧ M ⇒ P
B ∧ L ⇒ M
A ∧ P ⇒ L
A ∧ B ⇒ L
A
B
A B
0
L
0
M
0
P
0
0
Q
Úvod do umělé inteligence 7/12 11 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Algoritmus dopředného řetězení
function PL-FC-Entails?(KB, q) # vrací True nebo False
# KB je množina klauzulí, q je symbol/dotaz
count ← {c: num_premise_symbols(c) for ∀c ∈ list_of_clauses(KB ∪ q)}
inferred ← {s: False for ∀s ∈ list_of_symbols(KB ∪ q)}
queue ← facts_queue(KB)
while queue ̸= ∅ do
p ← queue.pop
if p = q then return True
if inferred [p] = False then
inferred [p] ← True
foreach clause c in KB where p is in c.premise do
count[c] −= 1
if count[c] = 0 then queue.add(c.conclusion)
return False
počet symbolů v premisi každé klauzule
fronta, na začátku obsahuje fakta z KB
Úvod do umělé inteligence 7/12 12 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Zpětné řetězení
Idea: pracuje zpětně od dotazu q
zkontroluj, jestli není q už známo
dokaž zpětným řetězením všechny premisy nějakého pravidla,
které má q jako důsledek
kontrola cyklů – pro každý podcíl se nejprve podívej, jestli už nebyl řešen
(tj. pamatuje si true i false výsledek)
Úvod do umělé inteligence 7/12 13 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Zpětné řetězení – příklad
P ⇒ Q
L ∧ M ⇒ P
B ∧ L ⇒ M
A ∧ P ⇒ L
A ∧ B ⇒ L
A
B
A
Q
P
L
B
M
Úvod do umělé inteligence 7/12 14 / 33
Inference ve výrokové logice Dopředné a zpětné řetězení
Porovnání dopředného a zpětného řetězení
▶ dopředné řetězení je řízeno daty
• automatické, nevědomé zpracování
• např. rozpoznávání objektů, rutinní rozhodování
• může udělat hodně nadbytečné práce bez vztahu k dotazu/cíli
▶ zpětné řetězení je řízeno dotazem
• vhodné pro hledání odpovědí na konkrétní dotaz
• např. “Kde jsou moje klíče?”, “Jak se mám přihlásit na PGS?”
• složitost zpětného řetězení může být mnohem menší než lineární vzhledem
k velikosti KB
Úvod do umělé inteligence 7/12 15 / 33
Inference ve výrokové logice DPLL
Davis-Putnam-Logemann-Loveland (DPLL)
dopředné a zpětné řetězení – pouze pro Hornovy klauzule
DPLL – vylepšené prohledávání s navracením, improved backtracking
základní algoritmus typu SAT solver
neomezuje KB, pracuje s formulemi v CNF
připomínka CNF
▶ klauzule – disjunkce literálů
▶ literál – symbol nebo negovaný symbol
(¬D ∨ ¬B ∨ C)
∧ (B ∨ ¬A ∨ ¬C)
∧ (¬C ∨ ¬B ∨ E)
∧ (E ∨ ¬D ∨ B)
∧ (B ∨ E ∨ ¬C)
literály ¬D, ¬B a C
pět klauzulí spojených konjunkcí ∧
Úvod do umělé inteligence 7/12 16 / 33
Inference ve výrokové logice DPLL
DPLL
DPLL vylepšení:
1. dřívější ukončení – DPLL detekuje pravdivost věty už z částečného modelu
klauzule (disjunkce literálů) je pravdivá
např. ¬D ∨ ¬B ∨ C
⇔ alespoň jeden literál je pravdivý
D = False, B = False nebo C = True
2. heuristika čistých symbolů, pure symbol heuristic
čistý symbol je ve všech klauzulích buď vždy pozitivní nebo vždy negovaný
v KB = {(A ∨ ¬B), (¬B ∨ ¬C), (C ∨ A)} jsou A a B čisté symboly, C není
když čistý symbol nastavíme na True hodnotu literálu (tedy negovaný
symbol=False) ⇒neporušíme splnitelnost KB
3. heuristika jednotkových klauzulí, unit clause heuristic
jednotková klauzule – obsahuje právě jeden literál (nebo ostatní dříve
určeny jako False)
pro splnění klauzule musí být daný literál pozitivní
Úvod do umělé inteligence 7/12 17 / 33
Inference ve výrokové logice DPLL
DPLL
function DPLL-Satisfiable?(s) # je výroková formule s splnitelná?
clauses ← cnf_set_of_clauses(s) # množina klauzulí z CNF(s)
symbols ← list_of_symbols(s) # seznam symbolů v s
return DPLL( clauses , symbols, {})
function DPLL( clauses , symbols, model) # jsou klauzule clauses pravdivé v modelu?
if clauses = ∅ then return True # prázdná množina klauzulí je pravdivá
if ∀ clause ∈ clauses: clause is True in model then return True
if ∃ clause ∈ clauses: clause is False in model then return False
P, value ← Find-Pure-Symbol(symbols, clauses, model)
if P ̸= None then return ........DPLL(clauses, symbols − P, model ∪ {P=value})
P, value ← Find-Unit-Clause(clauses, model)
if P ̸= None then return ........DPLL(clauses, symbols − P, model ∪ {P=value})
P ← symbols.first; rest ← symbols.rest
return ........DPLL( clauses , rest , model ∪ {P=True}) or
........DPLL( clauses , rest , model ∪ {P=False})
Úvod do umělé inteligence 7/12 18 / 33
Inference ve výrokové logice DPLL
DPLL– další možná vylepšení
▶ analýza komponent – identifikace nepropojených klauzulí a jejich
separátní zpracování
▶ uspořádání symbolů a hodnot – jako u splňování podmínek, např.
nejčastěji použitý symbol
▶ inteligentní navracení – zapamatování konfliktů, návrat k nejbližšímu
▶ náhodné restarty – po určité době začít výpočet od začátku
▶ chytré indexování
s těmito vylepšeními zvládnou moderní SAT algoritmy problémy v rozsahu
desítek milionů symbolů
Úvod do umělé inteligence 7/12 19 / 33
Inference ve výrokové logice Rezoluce
Rezoluce
obecný inferenční algoritmus – rezoluce
▶ dopředné a zpětné řetězení – úplné pro Hornovy klauzule, ale neúplné
pro obecnou KB
▶ rezoluce – úplná (pro důkaz sporem) pro výrokovou i predikátovou
logiku
▶ logické programování – SLD rezoluce
Úvod do umělé inteligence 7/12 20 / 33
Inference ve výrokové logice Rezoluce
Rezoluce
rezoluční vyvozování je pouze částečně rozhodnutelné:
▶ může najít důkaz α, když KB |= α
▶ nemůže vždy dokázat, že KB ̸|= α
viz problém zastavení – důkazová procedura nemusí skončit
nejde použít pro generování, pouze pro vyvracení
rezoluce je důkaz sporem:
pro důkaz KB |= α ukážeme, že KB ∧ ¬α je nesplnitelné
rezoluce používá KB, ¬α v konjunktivní normální formě (CNF), např.:
(P ∨ Q) ⇒ (Q ⇔ R) ≡ (¬P ∨ ¬Q ∨ R)
∧ (¬P ∨ Q ∨ ¬R)
∧ (¬Q ∨ R)
Úvod do umělé inteligence 7/12 21 / 33
Inference ve výrokové logice Rezoluce
Rezoluční pravidlo
algoritmus je založen na opakované aplikaci rezolučního pravidla – ze
dvou klauzulí odvoď novou klauzuli
C1 C2
C
▶ klauzule: C1 = P1 ∨ P2 ∨ . . . ∨ Pn
a C2 = ¬P1 ∨ Q1 ∨ Q2 ∨ . . . ∨ Qm
▶ výsledek (rezolventa):
C = P2 ∨ P3 ∨ . . . ∨ Pn ∨ Q1 ∨ Q2 ∨ . . . ∨ Qm
▶ vyruší se opačné literály P1 a ¬P1
pokud nic nezbude, výsledkem je prázdná
klauzule (odpovídá False)
postup rezolučního důkazu tvrzení F:
– začneme s ¬F
– rezolvujeme s klauzulí z KB (která obsahuje F)
– opakujeme až do odvození prázdné klauzule ⊓⊔
– když se to podaří → došli jsme ke sporu (pro ¬F) → musí platit F
Úvod do umělé inteligence 7/12 22 / 33
Inference ve výrokové logice Rezoluce
Rezoluce
function PL-Resolution(KB, α) # vrací True nebo False podle toho, zda KB|=α nebo KB̸|=α
clauses ← cnf_set_of_clauses(KB ∧ ¬α)
new_clauses ← ∅
while True do
foreach pair of clauses Ci , Cj ∈ clauses do
resolvent ← PL-Resolve(Ci , Cj )
if resolvent = then return True
new_clauses ← new_clauses ∪ {resolvent}
if new_clauses ⊆clauses then return False
clauses ← clauses ∪ new_clauses
rezoluce pokračuje v odvozování dokud nenastane situace, kdy:
▶ nejdou vytvořit žádné nové klauzule, pak KB ̸|= α
▶ dvě klauzule se rezolvují do prázdné klauzule , pak KB |= α
Úvod do umělé inteligence 7/12 23 / 33
Inference ve výrokové logice Rezoluce
Rezoluce – příklad z Wumpusovy jeskyně
báze znalostí KB:
▶ pravidlo V1,1 ⇔ (J1,2 ∨ J2,1)
(¬J2,1 ∨ V1,1) ∧ (¬V1,1 ∨ J1,2 ∨ J2,1) ∧ (¬J1,2 ∨ V1,1)
▶ vnímání ¬V1,1
▶ dotaz (co se má dokázat) ¬J1,2?
¬J2,1 ∨ V1,1 ¬V1,1 ∨ J1,2 ∨ J2,1 ¬J1,2 ∨ V1,1 ¬V1,1 J1,2
¬V1,1 ∨ J1,2 ∨ V1,1 J1,2 ∨ J2,1 ∨ ¬J2,1 ¬V1,1 ∨ J2,1 ∨ V1,1 J1,2 ∨ J2,1 ∨ ¬J1,2 ¬J2,1 ¬J1,2
Úvod do umělé inteligence 7/12 24 / 33
Inference ve výrokové logice Rezoluce
Rezoluce – příklad s výběrem klauzulí
▶ pravidla
• mráz ∧ srážky ⇒ sněží
¬mráz ∨ ¬srážky ∨ sněží
• Leden ⇒ mráz
¬Leden ∨ mráz
• mraky ⇒ srážky
¬mraky ∨ srážky
▶ fakta – Leden, mraky
▶ dotaz (co se má dokázat)
• sněží?
¬sněží
Úvod do umělé inteligence 7/12 25 / 33
Inference ve výrokové logice Rezoluce
Důkaz tvrzení “sněží”
S – sněží, s – srážky, m – mráz, L – Leden, M – mraky ¬m ∨ ¬s ∨ S
¬L ∨ m
¬M ∨ s
L, M¬S ¬m ∨ ¬s ∨ S
¬m ∨ ¬s ¬L ∨ m
¬L ∨ ¬s ¬M ∨ s
¬L ∨ ¬M L
¬M M
⊓⊔
Úvod do umělé inteligence 7/12 26 / 33
Inference v predikátové logice Kontrola modelů
Kontrola modelů
teoreticky můžeme určit všechny modely výčtem ze slovníku KB:
pro počet objektů n = 1, . . . , (∞)
pro každý k-ární predikát Pk ze slovníku
pro každou možnou k-ární relaci na n objektech
pro každý konstantní symbol C ze slovníku
pro každou volbu referenta pro C z n objektů . . .
prakticky je kontrola modelů nepoužitelná
inference je možná pouze podle inferenčních pravidel (dopředné/zpětné
řetězení, rezoluce, . . . )
Úvod do umělé inteligence 7/12 27 / 33
Inference v predikátové logice Unifikace
Unifikace – kvantifikátory
aplikace inferenčních pravidel – jak řešit kvantifikátory?
∃ kvantifikátor – řeší Skolemizace (převod PL1 do CNF)
∀ kvantifikátor – obecně proměnnou můžeme nahradit za term bez
proměnných (ground term)
např. v KB ∀x King(x) ∧ Greedy(x) ⇒ Evil(x)
King(John)
Greedy(John)
Brother(Richard, John)
první větu můžeme nahradit
King(John) ∧ Greedy(John) ⇒ Evil(John)
King(Richard) ∧ Greedy(Richard) ⇒ Evil(Richard)
Úvod do umělé inteligence 7/12 28 / 33
Inference v predikátové logice Unifikace
Unifikace – unifikace
∀x King(x) ∧ Greedy(x) ⇒ Evil(x)
King(John)
Greedy(John)
Brother(Richard, John)náhrada všech objektů za ∀x – velice neefektivní
lépe – vybírat hodnoty (substituce), které splňují literály premisy:
▶ ∀x King(x) splňuje pouze substituce σ = {x/John}
▶ σ vyhovuje i ∀x Greedy(x)
▶ a tedy platí i závěr Evil(x)σ = Evil(John)
nemusíme uvažovat King(Richard) ∧ Greedy(Richard) ⇒ Evil(Richard),
protože neplatí King(Richard)
Úvod do umělé inteligence 7/12 29 / 33
Inference v predikátové logice Unifikace
Unifikace – unifikace
potřebujeme “hledač” substitucí – algoritmus unifikace
unify(α, β) = σ taková, že ασ = βσ
např. unify(Knows(John, x), Knows(John, Jane)) = {x/Jane}
unify(Knows(John, x), Knows(y, Bill)) = {x/Bill, y/John}
unify(Knows(John, x), Knows(y, Mother(y))) = {y/John, x/Mother(John)}
unify(Knows(John, x), Knows(Bill, Elizabeth)) = failure
unify(Knows(John, x), Knows(x, Elizabeth)) = failure
unify v poslední větě lze vyřešit přejmenováním proměnných
unify(Knows(John, x), Knows(x2, Jane)) = {x/Jane, x2/John}
platných unifikací existuje víc, unify vrací nejobecnější unifikátor
Úvod do umělé inteligence 7/12 30 / 33
Inference v predikátové logice Zobecněné Modus Ponens
Zobecněné Modus Ponens
základní inferenční pravidlo – zobecněné Modus Ponens (Generalized
Modus Ponens, GMP)
p1
′, p2
′, . . . , pn
′, (p1 ∧ p2 ∧ . . . ∧ pn ⇒ q)
qσ
kde σ = i unify(pi
′, pi ) pro atomické formule pi , pi
′ a q s přejmenováním
kolizních proměnných
např.
King(John), Greedy(John), (King(x) ∧ Greedy(x) ⇒ Evil(x))
Evil(x){x/John}
Úvod do umělé inteligence 7/12 31 / 33
Inference v predikátové logice Zobecněné Modus Ponens
Zobecněné Modus Ponens
▶ používá unifikaci
▶ tato úprava MP se označuje jako lifting (pozvedává MP z jednoduché
výrokové logiky bez proměnných na logiku predikátovou)
▶ hlavní výhoda proti výčtu všech termů – jen ty substituce, které jsou pro
pravidlo nutné
▶ GMP je využito v upravených verzích inferenčních algoritmů –
dopředné/zpětné řetězení, rezoluce
hlavní úpravy – použití unifikace, při True vrací i možné substituce
Animal(F(x)) ∨ Loves(G(x), x) ¬Loves(u, v) ∨ ¬Kills(u, v)
Animal(F(x)) ∨ ¬Kills(G(x), x)
σ = {u/G(x), v/x}
▶ dopředné/zpětné řetězení je pro PL1 neúplné, rezoluce je úplná, i když
jen částečně rozhodnutelná (nemusí skončit pro nepravdivé tvrzení)
Úvod do umělé inteligence 7/12 32 / 33
Shrnutí
Shrnutí
logický agent aplikuje inferenci na bázi znalostí pro vyvození nových znalostí a tvorbu
rozhodnutí
základní koncepty logiky:
syntaxe: formální struktura vět inference: vyvození věty z jiných vět
sémantika: pravdivost vět podle modelů bezespornost: inference produkuje jen vyplývající věty
vyplývání: nutná pravdivost věty v závislosti
na jiné větě
úplnost: inference vyprodukuje ∀ vyplývající věty
výroková logika nemá dostatečnou expresivitu
predikátová logika prvního řádu:
– syntaxe: konstanty, funkce, predikáty, rovnost, kvantifikátory
– větší expresivita – dostatečná pro Wumpusovu jeskyni
– “poslední” logika, pro kterou existuje bezesporná a úplná inference (Gödelovy věty o
neúplnosti)
jiné možné logiky:
jazyk ontologie pravdivostní hodnoty
výroková logika fakty true/false/⊥
predikátová logika 1. řádu fakty, objekty, relace true/false/⊥
temporální logika fakty, objekty, relace, čas true/false/⊥
teorie pravděpodobnosti fakty míra pravděpodobnosti ∈ [0, 1]
fuzzy logika míra pravdivosti ∈ [0, 1] intervaly hodnot
Úvod do umělé inteligence 7/12 33 / 33