Logika prvn´ıho ˇr´adu a transparentn´ı intenzion´aln´ı logika (TIL) Aleˇs Hor´ak E-mail:
[email protected] http://nlp.fi.muni.cz/uui/
Obsah: Predik´atov´a logika prvn´ıho ˇr´adu Logick´a anal´yza pˇrirozen´eho jazyka Transparentn´ı intenzion´aln´ı logika ´ Uvod do umˇ el´ e inteligence 9/12
1 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Predik´ atov´ a logika 1. ˇr´ adu
V´yhody a nev´yhody v´yrokov´e logiky
, ,
v´yrokov´a logika je deklarativn´ı: syntaxe pˇr´ımo koresponduje s fakty
,
v´yrokov´a logika je kompoziˇcn´ı: v´yznam P1 ∧ P2 je odvozen z v´yznamu P1 a P2
v´yrokov´a logika umoˇzn ˇuje zpracov´avat ˇc´asteˇcn´e/disjunktivn´ı/negovan´e informace (coˇz je v´ıc, neˇz um´ı vˇetˇsina datov´ych struktur a datab´az´ı)
,
ve v´yrokov´e logice je v´yznam kontextovˇe nez´avisl´y (narozd´ıl od pˇrirozen´eho jazyka, kde v´yznam z´avis´ı na kontextu)
/
v´yrokov´a logika m´a velice omezenou expresivitu (narozd´ıl od pˇrirozen´eho jazyka) napˇr. nem´ame jak ˇr´ıct “J´amy zp˚ usobuj´ı V´anek ve vedlejˇs´ıch m´ıstnostech” jinak, neˇz vyjmenovat odpov´ıdaj´ıc´ı v´yrok pro kaˇzd´e pole ´ Uvod do umˇ el´ e inteligence 9/12
2 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Predik´ atov´ a logika 1. ˇr´ adu
Predik´atov´a logika prvn´ıho ˇr´adu
First-order predicate logic, FOPL/PL1 v´yrokov´a logika → svˇet obsahuje fakty × PL1 pˇredpokl´ad´a, ˇze svˇet obsahuje: • objekty – lidi, domy, teorie, barvy, roky, . . . • relace – ˇ cerven´y, kulat´y, prvoˇc´ıseln´y, bratˇri, vˇetˇs´ı neˇz, uvnitˇr, . . . • funkce – otec nˇ ekoho, nejlepˇs´ı pˇr´ıtel, plus jedna, zaˇc´atek ˇceho, . . .
´ Uvod do umˇ el´ e inteligence 9/12
3 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Syntaxe predik´ atov´ e logiky
Syntaxe predik´atov´e logiky z´akladn´ı prvky – konstanty funktory predik´at˚ u funkce promˇenn´e spojky rovnost kvantifik´atory
KingJohn, 2, RichardTheLionheart, . . . Brother, >, . . . Sqrt, LeftLegOf, . . . x, y , a, b, . . . ∧ ∨ ¬ ⇒ ⇔ = ∀∃
atomick´e formule – predik´aty sloˇzen´e termy
Brother(KingJohn, RichardTheLionheart)
> Length LeftLegOf(Richard) , Length LeftLegOf(KingJohn)
sloˇzen´e formule – tvoˇr´ı se z atomick´ych formul´ı pomoc´ı spojek ¬S, napˇr.
S1 ∧ S2 ,
S1 ∨ S2 ,
S1 ⇒ S2 ,
S1 ⇔ S2
Sibling(KingJohn, Richard) ⇒ Sibling(Richard, KingJohn) >(1, 2) ∨ ≤(1, 2) >(1, 2) ∧ ¬>(1, 2) ´ Uvod do umˇ el´ e inteligence 9/12
4 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Pravdivost v predik´ atov´ e logice
Pravdivost v predik´atov´e logice
pravdivost formule (s´emantika) se urˇcuje vzhledem k modelu a interpretaci model obsahuje ≥ 1 objekt˚ u a relace mezi nimi interpretace definuje vztah mezi syntax´ı a modelem – urˇcuje referenty pro: konstantn´ı symboly → objekty predik´atov´e symboly → relace funkˇcn´ı symboly → funkce atomick´a formule predik´ at(term1 , . . . , termn ) je pravdiv´a ⇔ ⇔ objekty odkazovan´e pomoc´ı term1 , . . . , termn jsou v relaci pojmenovan´e funktorem predik´ at.
´ Uvod do umˇ el´ e inteligence 9/12
5 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Pravdivost v predik´ atov´ e logice
Pˇr´ıklad modelu a interpretace ve FOPL koruna
na hlavˇe
bratr
osoba
osoba kr´al
bratr
R
$
J lev´a noha
lev´a noha
5 objekt˚ u, 2 bin´arn´ı relace, 3 un´arn´ı relace (osoba, kr´al, koruna) a 1 un´arn´ı funkce (lev´a noha). ´ Uvod do umˇ el´ e inteligence 9/12
6 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Kvantifikace
Univerz´aln´ı kvantifikace ∀hpromˇenn´e i hformulei ∀x Na(x, FI MU) ⇒ inteligentn´ı(x)
“Kaˇzd´y na FI MU je inteligentn´ı:” ∀x P je pravdiv´e v modelu m moˇzn´y objekt z modelu m
⇔
P je pravdiv´a pro x = kaˇzd´y
zhruba odpov´ıd´a konjunkci instanciac´ı P Na(Petr, FI MU) ⇒ inteligentn´ı(Petr) ∧ Na(Honza, FI MU) ⇒ inteligentn´ı(Honza) ∧ Na(FI MU, FI MU) ⇒ inteligentn´ı(FI MU) ∧ ...
´ Uvod do umˇ el´ e inteligence 9/12
7 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Kvantifikace
Existenˇcn´ı kvantifikace ∃hpromˇenn´e i hformulei “Nˇekdo na MFF UK je inteligentn´ı:” ∃x Na(x, MFF UK) ∧ inteligentn´ı(x) ∃x P je pravdiv´e v modelu m objekt z modelu m
⇔
P je pravdiv´a pro x = nˇejak´y
zhruba odpov´ıd´a disjunkci instanciac´ı P Na(Petr, MFF UK) ∧ inteligentn´ı(Petr) ∨ Na(Honza, MFF UK) ∧ inteligentn´ı(Honza) ∨ Na(MFF UK, MFF UK) ∧ inteligentn´ı(MFF UK) ∨ ...
´ Uvod do umˇ el´ e inteligence 9/12
8 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Kvantifikace
Vlastnosti kvantifikac´ı pozor pˇri pouˇzit´ı kvantifik´ator˚ u na z´amˇenu ∧ a ⇒: “kaˇzd´y P je Q.” “nˇekdo P je Q.”
dobˇre ∀x P ⇒ Q ∃x (P ∧ Q)
´ Uvod do umˇ el´ e inteligence 9/12
ˇspatnˇe ∀x P ∧ Q ∃x (P ⇒ Q)
9 / 34
znamenalo by “kaˇzd´y je P i Q.” “nˇekdo nen´ı P nebo je Q.”
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Kvantifikace
Vlastnosti kvantifikac´ı pozor pˇri pouˇzit´ı kvantifik´ator˚ u na z´amˇenu ∧ a ⇒: “kaˇzd´y P je Q.” “nˇekdo P je Q.”
∀x∀y ∃x∃y ∃x∀y
dobˇre ∀x P ⇒ Q ∃x (P ∧ Q)
je stejn´e jako je stejn´e jako nen´ı stejn´e jako
ˇspatnˇe ∀x P ∧ Q ∃x (P ⇒ Q)
znamenalo by “kaˇzd´y je P i Q.” “nˇekdo nen´ı P nebo je Q.”
∀y ∀x ∃y ∃x ∀y ∃x
∃x∀y m´a r´ad(x, y ) – “Existuje osoba, kter´a m´a r´ada vˇsechny lidi na svˇetˇe.” ∀y ∃x m´a r´ad(x, y ) – “Kaˇzd´eho na svˇetˇe m´a alespoˇ n jedna osoba r´ada.” (potenci´alnˇe kaˇzd´eho jin´a)
´ Uvod do umˇ el´ e inteligence 9/12
9 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Kvantifikace
Vlastnosti kvantifikac´ı pozor pˇri pouˇzit´ı kvantifik´ator˚ u na z´amˇenu ∧ a ⇒: “kaˇzd´y P je Q.” “nˇekdo P je Q.”
∀x∀y ∃x∃y ∃x∀y
dobˇre ∀x P ⇒ Q ∃x (P ∧ Q)
je stejn´e jako je stejn´e jako nen´ı stejn´e jako
ˇspatnˇe ∀x P ∧ Q ∃x (P ⇒ Q)
znamenalo by “kaˇzd´y je P i Q.” “nˇekdo nen´ı P nebo je Q.”
∀y ∀x ∃y ∃x ∀y ∃x
∃x∀y m´a r´ad(x, y ) – “Existuje osoba, kter´a m´a r´ada vˇsechny lidi na svˇetˇe.” ∀y ∃x m´a r´ad(x, y ) – “Kaˇzd´eho na svˇetˇe m´a alespoˇ n jedna osoba r´ada.” (potenci´alnˇe kaˇzd´eho jin´a)
dualita kvantifik´ator˚ u oba mohou b´yt vyj´adˇreny pomoc´ı druh´eho ∀x m´a r´ad(x, zmrzlina) ∃x m´a r´ad(x, mrkev)
≡ ≡
´ Uvod do umˇ el´ e inteligence 9/12
¬∃x ¬m´a r´ad(x, zmrzlina) ¬∀x ¬m´a r´ad(x, mrkev) 9 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB:
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech pro kaˇzd´y konstantn´ı symbol C ze slovn´ıku
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech pro kaˇzd´y konstantn´ı symbol C ze slovn´ıku pro kaˇzdou volbu referenta pro C z n objekt˚ u ...
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech pro kaˇzd´y konstantn´ı symbol C ze slovn´ıku pro kaˇzdou volbu referenta pro C z n objekt˚ u ... prakticky je kontrola model˚ u nepouˇziteln´a
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech pro kaˇzd´y konstantn´ı symbol C ze slovn´ıku pro kaˇzdou volbu referenta pro C z n objekt˚ u ... prakticky je kontrola model˚ u nepouˇziteln´a inference je moˇzn´a pouze podle inferenˇcn´ıch pravidel (dopˇredn´e/zpˇetn´e ˇretˇezen´ı, rezoluce, . . . )
´ Uvod do umˇ el´ e inteligence 9/12
10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Inference ve FOPL
Inference ve FOPL teoreticky m˚ uˇzeme urˇcit vˇsechny modely v´yˇctem ze slovn´ıku KB: u n = 1, . . . , (∞) pro poˇcet objekt˚ pro kaˇzd´y k-´arn´ı predik´at Pk ze slovn´ıku pro kaˇzdou moˇznou k-´arn´ı relaci na n objektech pro kaˇzd´y konstantn´ı symbol C ze slovn´ıku pro kaˇzdou volbu referenta pro C z n objekt˚ u ... prakticky je kontrola model˚ u nepouˇziteln´a inference je moˇzn´a pouze podle inferenˇcn´ıch pravidel (dopˇredn´e/zpˇetn´e ˇretˇezen´ı, rezoluce, . . . ) z´akladn´ı inferenˇcn´ı pravidlo – zobecnˇen´e Modus Ponens (Generalized Modus Ponens, GMP) – pouˇz´ıv´a nav´ıc unifikaci p1 ′ , p2 ′ , ..., pn ′ , (p1 ∧p2 ∧...∧pn ⇒q) Subst(θ,q)
kde ∀i Subst(θ, pi ′ ) = Subst(θ, pi ) pro atomick´e formule pi , pi ′ a q ´ Uvod do umˇ el´ e inteligence 9/12
– vznik´a z MP pomoc´ı liftingu – vyuˇz´ıv´a upraven´e verze inferenˇcn´ıch algoritm˚ u– dopˇredn´e/zpˇetn´e ˇretˇezen´ı, rezoluce 10 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı ve FOPL pˇredpokl´adejme, ˇze agent ve Wumpusovˇe jeskyni c´ıt´ı Z´apach a V´anek, ale nevid´ı Tˇrpyt, nenarazil do zdi a nezabil Wumpuse v ˇcase t = 5: tell(KB, percept([z´ apach, v´ anek, nic, nic, nic], 5)). ?− ask(KB,action(A,5)). % ∃A action(A,5) ?
tj. dotaz “Vypl´yv´a nˇejak´a akce z KB v ˇcase t = 5?”
´ Uvod do umˇ el´ e inteligence 9/12
11 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı ve FOPL pˇredpokl´adejme, ˇze agent ve Wumpusovˇe jeskyni c´ıt´ı Z´apach a V´anek, ale nevid´ı Tˇrpyt, nenarazil do zdi a nezabil Wumpuse v ˇcase t = 5: tell(KB, percept([z´ apach, v´ anek, nic, nic, nic], 5)). ?− ask(KB,action(A,5)). % ∃A action(A,5) ?
tj. dotaz “Vypl´yv´a nˇejak´a akce z KB v ˇcase t = 5?” ← substituce (hodnot promˇenn´ym) odpovˇed’: true, {a/V´ystˇrel}
´ Uvod do umˇ el´ e inteligence 9/12
11 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı ve FOPL pˇredpokl´adejme, ˇze agent ve Wumpusovˇe jeskyni c´ıt´ı Z´apach a V´anek, ale nevid´ı Tˇrpyt, nenarazil do zdi a nezabil Wumpuse v ˇcase t = 5: tell(KB, percept([z´ apach, v´ anek, nic, nic, nic], 5)). ?− ask(KB,action(A,5)). % ∃A action(A,5) ?
tj. dotaz “Vypl´yv´a nˇejak´a akce z KB v ˇcase t = 5?” ← substituce (hodnot promˇenn´ym) odpovˇed’: true, {a/V´ystˇrel} pro vˇetu S a substituci σ → Sσ oznaˇcuje v´ysledek aplikace σ na S: S
= chytˇrejˇs´ı(x, y )
σ = {x/Petr, y /Honza} Sσ = chytˇrejˇs´ı(Petr, Honza) Ask(KB, S) vrac´ı nˇekter´a/vˇsechna σ takov´e, ˇze KB |= Sσ ´ Uvod do umˇ el´ e inteligence 9/12
11 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı pro Wumpusovu jeskyni
Vn´ım´an´ı: ∀v , tr , n, w , t Percept([Z´apach, v , tr , n, w ], t) ⇒ Je z´apach(t) ∀z, v , n, w , t Percept([z, v , Tˇrpyt, n, w ], t) ⇒ M´ame zlato(t) Reflex: ∀t M´ame zlato(t) ⇒ Action(Zvednut´ı, t) Reflex s vnitˇrn´ım stavem: nemˇeli jsme uˇz zlato? ∀t M´ame zlato(t) ∧ ¬Drˇz´ım(Zlato, t) ⇒ Action(Zvednut´ı, t) Drˇz´ım(Zlato, t) nen´ı pozorovateln´e ⇒ je d˚ uleˇzit´e drˇzet si informace o vnitˇrn´ıch stavech
´ Uvod do umˇ el´ e inteligence 9/12
12 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı pro Wumpusovu jeskyni pokraˇc. Vyvozov´an´ı skryt´ych skuteˇcnost´ı: vlastnosti pozice: ∀x, t Na poli(Agent, x, t) ∧ Je z´apach(t) ⇒ Zap´ach´a(x) ∀x, t Na poli(Agent, x, t) ∧ Je v´anek(t) ⇒ S v´ankem(x) “V poli vedle J´amy je V´anek:” • diagnostick´ e pravidlo – odvod´ı pˇr´ıˇciny z n´asledku
∀y S v´ankem(y ) ⇒ ∃x J´ama(x) ∧ Vedle(x, y ) • pˇr´ıˇ cinn´e pravidlo – odvod´ı v´ysledek z premisy
∀x, y J´ama(x) ∧ Vedle(x, y ) ⇒ S v´ankem(y ) • ani jedno z nich nen´ı u ´pln´e
napˇr. pˇr´ıˇcinn´e pravidlo neˇr´ık´a, jestli v poli daleko od J´amy nem˚ uˇze b´yt V´anek • definice vztahu V´ anku a J´amy: ∀y S v´ankem(y ) ⇔ [∃x J´ama(x) ∧ Vedle(x, y )] ´ Uvod do umˇ el´ e inteligence 9/12
13 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
B´ aze znalost´ı ve FOPL
B´aze znalost´ı pro Wumpusovu jeskyni – rozhodov´an´ı poˇc´ateˇcn´ı podm´ınka v KB: Na poli(Agent, [1, 1], S0 ) dotaz Ask(KB, ∃s Drˇz´ım(Zlato, s)) tj., “V jak´e situaci budu drˇzet Zlato?” situace jsou propojeny pomoc´ı funkce Result: Result(a, s) . . . situace, kter´a je v´ysledkem ˇcinnosti a v s odpovˇed’ (napˇr. v situaci, kdy hned na vedlejˇs´ım poli je Zlato) {s/Result(Zvednut´ı, Result(Krok dopˇredu, S0 ))} tj., jdi dopˇredu a zvedni Zlato ´ Uvod do umˇ el´ e inteligence 9/12
14 / 34
Predik´ atov´ a logika prvn´ıho ˇr´ adu
Shrnut´ı
Shrnut´ı logick´ y agent aplikuje inferenci na b´ azi znalost´ı pro vyvozen´ı nov´ ych znalost´ı a tvorbu rozhodnut´ı z´ akladn´ı koncepty logiky: syntaxe: form´ aln´ı struktura vˇ et inference: vyvozen´ı vˇ ety z jin´ ych vˇ et s´ emantika: pravdivost vˇ et podle model˚ u bezespornost: inference produkuje jen vypl´ yvaj´ıc´ı vˇ ety vypl´ yv´ an´ı: nutn´ a pravdivost vˇ ety v z´ avisu ´plnost: inference vyprodukuje ∀ vypl´ yvaj´ıc´ı vˇ ety losti na jin´ e vˇ etˇ e v´ yrokov´ a logika nem´ a dostateˇ cnou expresivitu predik´ atov´ a logika prvn´ıho ˇr´ adu: – syntaxe: konstanty, funkce, predik´ aty, rovnost, kvantifik´ atory – vˇ etˇs´ı expresivita – dostateˇ cn´ a pro Wumpusovu jeskyni – “posledn´ı” logika, pro kterou existuje bezesporn´ aau ´pln´ a inference (G¨ odelovy vˇ ety o ne´ uplnosti) jin´ e moˇzn´ e logiky: jazyk v´ yrokov´ a logika predik´ atov´ a logika 1. ˇr´ adu tempor´ aln´ı logika teorie pravdˇ epodobnosti fuzzy logika
ontologie fakty fakty, objekty, relace fakty, objekty, relace, ˇ cas fakty m´ıra pravdivosti ∈ [0, 1]
´ Uvod do umˇ el´ e inteligence 9/12
15 / 34
pravdivostn´ı hodnoty true/false/⊥ true/false/⊥ true/false/⊥ m´ıra pravdˇ epodobnosti ∈ [0, 1] intervaly hodnot
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Obsah 1
2
3
Predik´atov´a logika prvn´ıho ˇr´adu Predik´atov´a logika 1. ˇr´adu Syntaxe predik´atov´e logiky Pravdivost v predik´atov´e logice Kvantifikace Inference ve FOPL B´aze znalost´ı ve FOPL Shrnut´ı Logick´a anal´yza pˇrirozen´eho jazyka Vztah pojmu a v´yrazu Omezenost predik´atov´e logiky 1. ˇr´adu Extenze a intenze Transparentn´ı intenzion´aln´ı logika Typy v TILu Konstrukce Pˇr´ıklady pˇr´ınosu TILu ´ Uvod do umˇ el´ e inteligence 9/12
16 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Logick´a anal´yza pˇrirozen´eho jazyka logick´a anal´yza PJ – anal´yza v´yznamu v´yraz˚ u (vˇet) PJ pˇrirozen´y jazyk (ˇceˇstina, angliˇctina, . . . ) = n´astroj pojmov´eho uchopen´ı reality pojem – krit´eria/procedury umoˇzn ˇuj´ıc´ı identifikovat r˚ uzn´e konkr´etn´ı a abstraktn´ı objekty (napˇr. “planeta” – tˇr´ıda nebesk´ych tˇeles s urˇcit´ymi charakteristikami – ob´ıh´a po obˇeˇzn´e dr´aze kolem st´alice, nen´ı zdrojem svˇetla, . . . )
´ Uvod do umˇ el´ e inteligence 9/12
17 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Logick´a anal´yza pˇrirozen´eho jazyka logick´a anal´yza PJ – anal´yza v´yznamu v´yraz˚ u (vˇet) PJ pˇrirozen´y jazyk (ˇceˇstina, angliˇctina, . . . ) = n´astroj pojmov´eho uchopen´ı reality pojem – krit´eria/procedury umoˇzn ˇuj´ıc´ı identifikovat r˚ uzn´e konkr´etn´ı a abstraktn´ı objekty (napˇr. “planeta” – tˇr´ıda nebesk´ych tˇeles s urˇcit´ymi charakteristikami – ob´ıh´a po obˇeˇzn´e dr´aze kolem st´alice, nen´ı zdrojem svˇetla, . . . )
– pojem 6= v´yraz – napˇr. v´yrazy v r˚ uzn´ych jazyc´ıch ˇcasto reprezentuj´ı stejn´y pojem (pojem(“prvoˇc´ıslo”) ≡ pojem(“prime number”))
´ Uvod do umˇ el´ e inteligence 9/12
17 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Logick´a anal´yza pˇrirozen´eho jazyka logick´a anal´yza PJ – anal´yza v´yznamu v´yraz˚ u (vˇet) PJ pˇrirozen´y jazyk (ˇceˇstina, angliˇctina, . . . ) = n´astroj pojmov´eho uchopen´ı reality pojem – krit´eria/procedury umoˇzn ˇuj´ıc´ı identifikovat r˚ uzn´e konkr´etn´ı a abstraktn´ı objekty (napˇr. “planeta” – tˇr´ıda nebesk´ych tˇeles s urˇcit´ymi charakteristikami – ob´ıh´a po obˇeˇzn´e dr´aze kolem st´alice, nen´ı zdrojem svˇetla, . . . )
– pojem 6= v´yraz – napˇr. v´yrazy v r˚ uzn´ych jazyc´ıch ˇcasto reprezentuj´ı stejn´y pojem (pojem(“prvoˇc´ıslo”) ≡ pojem(“prime number”)) – pojem 6= pˇredstava – pˇredstava je subjektivn´ı, pojem je objektivn´ı
´ Uvod do umˇ el´ e inteligence 9/12
17 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Logick´a anal´yza pˇrirozen´eho jazyka logick´a anal´yza PJ – anal´yza v´yznamu v´yraz˚ u (vˇet) PJ pˇrirozen´y jazyk (ˇceˇstina, angliˇctina, . . . ) = n´astroj pojmov´eho uchopen´ı reality pojem – krit´eria/procedury umoˇzn ˇuj´ıc´ı identifikovat r˚ uzn´e konkr´etn´ı a abstraktn´ı objekty (napˇr. “planeta” – tˇr´ıda nebesk´ych tˇeles s urˇcit´ymi charakteristikami – ob´ıh´a po obˇeˇzn´e dr´aze kolem st´alice, nen´ı zdrojem svˇetla, . . . )
– pojem 6= v´yraz – napˇr. v´yrazy v r˚ uzn´ych jazyc´ıch ˇcasto reprezentuj´ı stejn´y pojem (pojem(“prvoˇc´ıslo”) ≡ pojem(“prime number”)) – pojem 6= pˇredstava – pˇredstava je subjektivn´ı, pojem je objektivn´ı – pojmy mohou identifikovat r˚ uzn´e objekty: • • • • • •
ˇ jedno individuum – individu´aln´ı pojmy (napˇr. Petr, Pegas, prezident CR) tˇr´ıdu objekt˚ u – vlastnost (napˇr. ˇcerven´y, ˇselma, hora) n-ˇclennou relaci – vztah (napˇr. otec (nˇekoho), kˇrivdit (nˇekdo nˇekomu)) pravdivostn´ı hodnotu – propozice (napˇr. v Brnˇe prˇs´ı) funkcion´aln´ı pˇriˇrazen´ı – empirick´e funkce (napˇr. rychlost) ˇc´ıslo – (fyzik´aln´ı) veliˇciny (napˇr. rychlost svˇetla) ´ Uvod do umˇ el´ e inteligence 9/12
17 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Vztah pojmu a v´ yrazu
Vztah pojmu a v´yrazu ve zjednoduˇsen´e podobˇe: pojem odpov´ıd´a logick´e konstrukci
´ Uvod do umˇ el´ e inteligence 9/12
18 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Vztah pojmu a v´ yrazu
Vztah pojmu a v´yrazu ve zjednoduˇsen´e podobˇe: pojem odpov´ıd´a logick´e konstrukci
ko ns
je
t ru
tu
uj e
en
/id e
nt
rez rep
ifik
uj e
konstrukce/pojem
objekt
oznaˇ cuje
´ Uvod do umˇ el´ e inteligence 9/12
18 / 34
v´yraz
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Vztah pojmu a v´ yrazu
Vztah pojmu a v´yrazu ve zjednoduˇsen´e podobˇe: pojem odpov´ıd´a logick´e konstrukci konstrukce/pojem
uj
je ku
oznaˇ cuje
v´ yraz
re
ifi
ko n
st
e
ru
uj
pr e
e/ id en t
objekt
λw λt[Author ofwt Hamlet]
nt
e/
ze
id
e pr
en
re
tifi
ku
je
sloˇzen´ y z pojm˚ u ‘Author of’ a ‘Hamlet’
funkce (tabulka), kter´ a podle svˇ eta a ˇ casu uk´ aˇze na individum. V naˇsem svˇ etˇ e na Williama Shakespeara
nt
uj
e
ko ns
t ru
uj
ze
AH
´ Uvod do umˇ el´ e inteligence 9/12
oznaˇ cuje
18 / 34
“autor Hamleta”
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Omezenost predik´atov´e logiky 1. ˇr´adu dva omezuj´ıc´ı rysy: – nedostateˇcn´a expresivita – extenzionalismus
´ Uvod do umˇ el´ e inteligence 9/12
19 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Omezenost predik´atov´e logiky 1. ˇr´adu dva omezuj´ıc´ı rysy: – nedostateˇcn´a expresivita – extenzionalismus Expresivita: vyjadˇrovac´ı s´ıla jazyka “Je-li barva stropu pokoje ˇc. 3 uklidˇnuj´ıc´ı, je pokoj ˇc. 3 vhodn´y pro pacienta X a nen´ı vhodn´y pro pacienta Y .”
´ Uvod do umˇ el´ e inteligence 9/12
19 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Omezenost predik´atov´e logiky 1. ˇr´adu dva omezuj´ıc´ı rysy: – nedostateˇcn´a expresivita – extenzionalismus Expresivita: vyjadˇrovac´ı s´ıla jazyka “Je-li barva stropu pokoje ˇc. 3 uklidˇnuj´ıc´ı, je pokoj ˇc. 3 vhodn´y pro pacienta X a nen´ı vhodn´y pro pacienta Y .” anal´yza ve v´yrokov´e logice: P ⇒ (Q ∧ ¬R) P “Barva stropu pokoje ˇc. 3 je uklidˇ nuj´ıc´ı.” Q R
“Pokoj ˇc. 3 je vhodn´y pro pacienta X .” “Pokoj ˇc. 3 je vhodn´y pro pacienta Y .”
´ Uvod do umˇ el´ e inteligence 9/12
19 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Omezenost predik´atov´e logiky 1. ˇr´adu dva omezuj´ıc´ı rysy: – nedostateˇcn´a expresivita – extenzionalismus Expresivita: vyjadˇrovac´ı s´ıla jazyka “Je-li barva stropu pokoje ˇc. 3 uklidˇnuj´ıc´ı, je pokoj ˇc. 3 vhodn´y pro pacienta X a nen´ı vhodn´y pro pacienta Y .” anal´yza ve v´yrokov´e logice: P ⇒ (Q ∧ ¬R) P “Barva stropu pokoje ˇc. 3 je uklidˇ nuj´ıc´ı.” Q R
“Pokoj ˇc. 3 je vhodn´y pro pacienta X .” “Pokoj ˇc. 3 je vhodn´y pro pacienta Y .”
anal´yza v PL1: U(B) ⇒ (V (P, X ) ∧ ¬V (P, Y ))
U B V P X,Y
´ Uvod do umˇ el´ e inteligence 9/12
tˇr´ıda uklidˇ nuj´ıc´ıch objekt˚ u individuum ‘barva stropu pokoje ˇc. 3’ relace mezi individuy ‘b´yt vhodn´y pro’ individuum ‘pokoj ˇc. 3’ individua ‘pacient X ’ a ‘pacient Y ’ 19 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Nedostateˇcn´a expresivita PL1
ˇ Cerven´ a barva je kr´asnˇejˇs´ı neˇz hnˇed´a barva.
´ Uvod do umˇ el´ e inteligence 9/12
20 / 34
Kostka je ˇcerven´a.
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Nedostateˇcn´a expresivita PL1
ˇ Cerven´ a barva je kr´asnˇejˇs´ı neˇz hnˇed´a barva. anal´yza v PL1:
Kostka je ˇcerven´a.
ˇ1 , H) ˇ2 (Ko) Kr (C C individuum ‘ˇcerven´a barva’ vlastnost individu´ı ‘b´yt ˇcerven´y’ (tˇr´ıda ˇcerven´ych objekt˚ u) ˇ ˇ nelze vyj´adˇrit C1 ≡ C2 ˇ1 C ˇ2 C
´ Uvod do umˇ el´ e inteligence 9/12
20 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1
Varˇsava
´ Uvod do umˇ el´ e inteligence 9/12
hlavn´ı mˇesto Polska
21 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1
Varˇsava Varˇsava
hlavn´ı mˇesto Polska – jm´eno individua, jasnˇe identifikovateln´e a odliˇsiteln´e
´ Uvod do umˇ el´ e inteligence 9/12
21 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1
Varˇsava Varˇsava hlavn´ı mˇesto Polska
hlavn´ı mˇesto Polska – jm´eno individua, jasnˇe identifikovateln´e a odliˇsiteln´e – individuov´a role, moment´alnˇe identifikuje Varˇsavu, ale dˇr´ıve to byl i Krakov
´ Uvod do umˇ el´ e inteligence 9/12
21 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1
Varˇsava Varˇsava hlavn´ı mˇesto Polska
hlavn´ı mˇesto Polska – jm´eno individua, jasnˇe identifikovateln´e a odliˇsiteln´e – individuov´a role, moment´alnˇe identifikuje Varˇsavu, ale dˇr´ıve to byl i Krakov
‘hlavn´ı mˇesto Polska’ – z´avis´ı na svˇetˇe a ˇcase – pochopen´ı v´yznamu, ale nen´ı v´azan´e na znalost obsahu – tj. v´yznam na svˇetˇe a ˇcase nez´avis´ı
´ Uvod do umˇ el´ e inteligence 9/12
21 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
´ Uvod do umˇ el´ e inteligence 9/12
budova X je vˇetˇs´ı neˇz budova Y
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y matematick´ e
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a
´ Uvod do umˇ el´ e inteligence 9/12
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a vˇetˇs´ı neˇz – vztah dvou individu´ı, kter´y se m˚ uˇze mˇenit v ˇcase (otec a syn)
matematick´ e empirick´ e
´ Uvod do umˇ el´ e inteligence 9/12
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a vˇetˇs´ı neˇz – vztah dvou individu´ı, kter´y se m˚ uˇze mˇenit v ˇcase (otec a syn)
matematick´ e empirick´ e
ano
´ Uvod do umˇ el´ e inteligence 9/12
V Brnˇe prˇs´ı
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a vˇetˇs´ı neˇz – vztah dvou individu´ı, kter´y se m˚ uˇze mˇenit v ˇcase (otec a syn)
matematick´ e empirick´ e
ano ano
V Brnˇe prˇs´ı
– pravdivostn´ı hodnota true
´ Uvod do umˇ el´ e inteligence 9/12
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a vˇetˇs´ı neˇz – vztah dvou individu´ı, kter´y se m˚ uˇze mˇenit v ˇcase (otec a syn)
matematick´ e empirick´ e
ano
V Brnˇe prˇs´ı
– pravdivostn´ı hodnota true ano V Brnˇe prˇs´ı – propozice – oznaˇcuje pravdivostn´ı hodnotu, kter´a se mˇen´ı (alespoˇ n) v ˇcase
´ Uvod do umˇ el´ e inteligence 9/12
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Omezenost predik´ atov´ e logiky 1. ˇr´ adu
Extenzionalismus PL1 pokraˇc. ˇc´ıslo X je vˇetˇs´ı neˇz ˇc´ıslo Y
budova X je vˇetˇs´ı neˇz budova Y
vˇetˇs´ı neˇz – relace dvojic ˇc´ısel, pevnˇe dan´a vˇetˇs´ı neˇz – vztah dvou individu´ı, kter´y se m˚ uˇze mˇenit v ˇcase (otec a syn)
matematick´ e empirick´ e
ano
V Brnˇe prˇs´ı
– pravdivostn´ı hodnota true ano V Brnˇe prˇs´ı – propozice – oznaˇcuje pravdivostn´ı hodnotu, kter´a se mˇen´ı (alespoˇ n) v ˇcase i kdyˇz hodnota nˇekdy z´avis´ı na svˇetˇe a ˇcase, samotn´y v´yznam na nich nez´avis´ı ´ Uvod do umˇ el´ e inteligence 9/12
22 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Extenze a intenze
Extenze a intenze
Definujeme: intenze – objekty typu funkc´ı, jejichˇz hodnoty z´avis´ı na svˇetˇe a ˇcase extenze – ostatn´ı objekty (na svˇetˇe a ˇcase nez´avisl´e)
´ Uvod do umˇ el´ e inteligence 9/12
23 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Extenze a intenze
Extenze a intenze
Definujeme: intenze – objekty typu funkc´ı, jejichˇz hodnoty z´avis´ı na svˇetˇe a ˇcase extenze – ostatn´ı objekty (na svˇetˇe a ˇcase nez´avisl´e) ˇcast´e extenze a intenze: extenze individua tˇr´ıdy relace pravdivostn´ı hodnoty funkce ˇc´ısla
´ Uvod do umˇ el´ e inteligence 9/12
intenze individuov´e role vlastnosti vztahy propozice empirick´e funkce veliˇciny
23 / 34
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Extenze a intenze
Rozˇs´ıˇren´y vztah v´yrazu a v´yznamu u intenz´ı
id
konstrukce
uj
oznaˇ cuje
oz n
urˇ cuje
v´ yraz
extenze
´ Uvod do umˇ el´ e inteligence 9/12
aˇc uj
e
ukazuje na
24 / 34
reprezentuje
st
e
ru
uj
ko n
konstruuje
nt
e/
ze
objekt
intenze
e pr
en
re
tifi
ku
je
konstrukce/pojem
v´yraz
Logick´ a anal´ yza pˇrirozen´ eho jazyka
Extenze a intenze
Rozˇs´ıˇren´y vztah v´yrazu a v´yznamu u intenz´ı
konstruuje
j ˇcu na e ukazuje na
konstruuje
urˇ cuje
v´ yraz
AH
William Shakespear
´ Uvod do umˇ el´ e inteligence 9/12
oz n
λw λt[Author ofwt Hamlet]
aˇc uj e
ukazuje na
24 / 34
reprezentuje
oz
urˇ cuje
extenze
konstrukce reprezentuje
intenze
“autor Hamleta”
Transparentn´ı intenzion´ aln´ı logika
Obsah 1
2
3
Predik´atov´a logika prvn´ıho ˇr´adu Predik´atov´a logika 1. ˇr´adu Syntaxe predik´atov´e logiky Pravdivost v predik´atov´e logice Kvantifikace Inference ve FOPL B´aze znalost´ı ve FOPL Shrnut´ı Logick´a anal´yza pˇrirozen´eho jazyka Vztah pojmu a v´yrazu Omezenost predik´atov´e logiky 1. ˇr´adu Extenze a intenze Transparentn´ı intenzion´aln´ı logika Typy v TILu Konstrukce Pˇr´ıklady pˇr´ınosu TILu ´ Uvod do umˇ el´ e inteligence 9/12
25 / 34
Transparentn´ı intenzion´ aln´ı logika
Transparentn´ı intenzion´aln´ı logika Transparent Intensional Logic, TIL logick´y syst´em speci´alnˇe navrˇzen´y pro zachycen´ı v´yznamu v´yraz˚ u PJ autor Pavel Tich´y: The Foundations of Frege’s Logic, de Gruyter, Berlin, New York, 1988. obdobn´a teorie – Montagueho intenzion´aln´ı logika – Tich´y ukazuje jej´ı nedostatky Tich´y vych´az´ı z myˇslenek – Gottlob Frege (1848 – 1925, logik) a Alonzo Church (1903 – 1995, teorie typ˚ u) vlastnosti: • rozvˇ etven´a typov´a hierarchie (s typy vyˇsˇs´ıch ˇr´ad˚ u) • tempor´ aln´ı • intenzion´ aln´ı (intenze × extenze)
transparentost: 1. nositel v´yznamu (konstrukce) nen´ı prvek form´aln´ıho apar´atu, tento apar´at pouze studuje konstrukce 2. zachycen´ı intenzionality je pˇresnˇe pops´ano z matematick´eho hlediska ´ Uvod do umˇ el´ e inteligence 9/12
26 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Typy v TILu
typ objektu: – z´akladn´ı typy – typov´a b´aze = {o, ι, τ, ω} – funcion´aln´ı typy – funkce nad typovou b´az´ı napˇr.
ι,
((ιτ )ω),
(oι),
(((oι)τ )ω),
((oτ )ω), . . .
((ατ )ω) . . . z´avislost na svˇetˇe a ˇcase, vyjadˇruje intenze – z´apis ατ ω – typy vyˇsˇs´ıch ˇr´ad˚ u – obsahuj´ı i tˇr´ıdy konstrukc´ı ˇr´adu n – ∗n
´ Uvod do umˇ el´ e inteligence 9/12
27 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Z´akladn´ı typy TILu umoˇzn ˇuj´ı pˇriˇradit typ objekt˚ um z intenzion´aln´ı b´aze jazyka – tˇr´ıda z´akladn´ıch vlastnost´ı (barvy, rozmˇery, postoje, . . . ) popisuj´ıc´ıch stav svˇeta o (omikron, o) . . . pravdivostn´ı hodnoty Pravda (true, T) a Nepravda (false, F) u– pˇresnˇe odpov´ıdaj´ı bˇeˇzn´ym logik´am, typy logick´ych oper´ator˚ (oo), (ooo) ι (jota) . . . tˇr´ıda individu´ı individua ovˇsem ne jako kompletn´ı objekty, ale jako numerick´a identifikace nestrukturovan´e entity τ (tau) . . . tˇr´ıda ˇcasov´ych okamˇzik˚ u (jako ˇcasov´eho kontinua) zachycen´ı z´avislosti na ˇcase; souˇcasnˇe tˇr´ıda re´aln´ych ˇc´ısel ω (omega) . . . tˇr´ıda moˇzn´ych svˇet˚ u zachycen´ı empirick´e z´avislosti na stavu svˇeta ´ Uvod do umˇ el´ e inteligence 9/12
28 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Moˇzn´e svˇety term´ın moˇzn´y svˇet – Gottfried Wilhelm von Leibniz (1646–1716, filozof a matematik) ∀ moˇzn´y svˇet je: – soubor mysliteln´ych fakt˚ u – je konzistentn´ı a maxim´aln´ı ze vˇsech takov´ych soubor˚ u – je objektivn´ı (nez´avisl´y na individu´aln´ım n´azoru) mezi moˇzn´ymi svˇety ∃ pr´avˇe jeden aktu´aln´ı svˇet – jeho znalost ≡ vˇsevˇedoucnost
´ Uvod do umˇ el´ e inteligence 9/12
29 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Moˇzn´e svˇety term´ın moˇzn´y svˇet – Gottfried Wilhelm von Leibniz (1646–1716, filozof a matematik) ∀ moˇzn´y svˇet je: – soubor mysliteln´ych fakt˚ u – je konzistentn´ı a maxim´aln´ı ze vˇsech takov´ych soubor˚ u – je objektivn´ı (nez´avisl´y na individu´aln´ım n´azoru) mezi moˇzn´ymi svˇety ∃ pr´avˇe jeden aktu´aln´ı svˇet – jeho znalost ≡ vˇsevˇedoucnost
moˇzn´y svˇet v TILu = rozhodovac´ı syst´em, pro ∀ prvek intenzion´aln´ı b´aze obsahuje konzistentn´ı pˇriˇrazen´ı hodnot
´ Uvod do umˇ el´ e inteligence 9/12
29 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Moˇzn´e svˇety term´ın moˇzn´y svˇet – Gottfried Wilhelm von Leibniz (1646–1716, filozof a matematik) ∀ moˇzn´y svˇet je: – soubor mysliteln´ych fakt˚ u – je konzistentn´ı a maxim´aln´ı ze vˇsech takov´ych soubor˚ u – je objektivn´ı (nez´avisl´y na individu´aln´ım n´azoru) mezi moˇzn´ymi svˇety ∃ pr´avˇe jeden aktu´aln´ı svˇet – jeho znalost ≡ vˇsevˇedoucnost
moˇzn´y svˇet v TILu = rozhodovac´ı syst´em, pro ∀ prvek intenzion´aln´ı b´aze obsahuje konzistentn´ı pˇriˇrazen´ı hodnot u w1 , ..., w9 ): pˇr´ıklad – realita s 2 objekty a 2 vlastnostmi (9 moˇzn´ych svˇet˚ b´yt huben´y {Laurel, Hardy} {Laurel} {Hardy} ∅
{Laurel, Hardy} × × × w6 ´ Uvod do umˇ el´ e inteligence 9/12
b´yt tlust´y {Laurel} {Hardy} × × × w2 w4 × w7 w8 29 / 34
∅ w1 w3 w5 w9
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Princip intenz´ı v TILu b´yt huben´y
. . . objekt typu (oι)τ ω , funkce z moˇzn´ych svˇet˚ u a ˇcasu do tˇr´ıd individu´ı w . . . promˇenn´a typu ω, moˇzn´y svˇet t . . . promˇenn´a typu τ , ˇcasov´y okamˇzik [b´ yt huben´ y w t] . . . konstruuje (oι)-objekt, tˇr´ıdu individu´ı, kteˇr´ı maj´ı ve svˇetˇe w a ˇcase t vlastnost b´yt huben´y (znaˇc´ıme b´ yt huben´ ywt )
´ Uvod do umˇ el´ e inteligence 9/12
30 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Princip intenz´ı v TILu b´yt huben´y
. . . objekt typu (oι)τ ω , funkce z moˇzn´ych svˇet˚ u a ˇcasu do tˇr´ıd individu´ı w . . . promˇenn´a typu ω, moˇzn´y svˇet t . . . promˇenn´a typu τ , ˇcasov´y okamˇzik [b´ yt huben´ y w t] . . . konstruuje (oι)-objekt, tˇr´ıdu individu´ı, kteˇr´ı maj´ı ve svˇetˇe w a ˇcase t vlastnost b´yt huben´y (znaˇc´ıme b´ yt huben´ ywt )
pokud aplikujeme jen w – z´ısk´ame chronologii
Americk´ y prezidentwact (zkr. Pwact ) . . . ιτ Pwact t0 . . . ι: t0 . . . τ : 1789 1797 1801 J.Adams T.Jefferson nedef G.Washington
´ Uvod do umˇ el´ e inteligence 9/12
30 / 34
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Princip intenz´ı v TILu b´yt huben´y
. . . objekt typu (oι)τ ω , funkce z moˇzn´ych svˇet˚ u a ˇcasu do tˇr´ıd individu´ı w . . . promˇenn´a typu ω, moˇzn´y svˇet t . . . promˇenn´a typu τ , ˇcasov´y okamˇzik [b´ yt huben´ y w t] . . . konstruuje (oι)-objekt, tˇr´ıdu individu´ı, kteˇr´ı maj´ı ve svˇetˇe w a ˇcase t vlastnost b´yt huben´y (znaˇc´ıme b´ yt huben´ ywt )
pokud aplikujeme jen w – z´ısk´ame chronologii
Americk´ y prezidentwact (zkr. Pwact ) . . . ιτ Pwact t0 . . . ι: t0 . . . τ : 1789 1797 1801 J.Adams T.Jefferson nedef G.Washington
intenzion´aln´ı sestup – identifikace extenze pomoc´ı intenze, svˇeta w1 a ˇcasu t1
ω✻ w1 t1
´ Uvod do umˇ el´ e inteligence 9/12
30 / 34
✲
τ
Transparentn´ı intenzion´ aln´ı logika
Typy v TILu
Nejˇcastˇejˇs´ı typy
extenze
intenze
individua
...
ι
individuov´e role
...
ιτ ω
tˇr´ıdy
...
(oι)
vlastnosti
...
(oι)τ ω
relace
...
(oαβ)
vztahy
...
(oαβ)τ ω
pravdivostn´ı hodnoty
...
o
propozice
...
oτ ω , π
funkce
...
(αβ)
empirick´e funkce
...
(αβ)τ ω
ˇc´ısla
...
τ
veliˇciny
...
ττ ω
´ Uvod do umˇ el´ e inteligence 9/12
31 / 34
Transparentn´ı intenzion´ aln´ı logika
Konstrukce
Konstrukce konstrukce v TILu: promˇenn´a typu α, v z´avislosti na valuaci konstruuje α-objekt x ...ι trivializace objektu A typu α, konstruuje pr´avˇe objekt A 0A . . . α, ˇcasto tak´e A . . . α trivializace sloˇzen´e konstrukce – pˇrechod k vyˇsˇs´ım ˇr´ad˚ um aplikace konstrukce X . . . (αβ1 . . . βn ) na konstrukce Y1 ,. . . ,Yn typ˚ u β1 , . . . , βn , konstruuje objekt typu α [XY1 . . . Yn ] . . . α abstrakce konstrukce Y . . . α na promˇenn´ych x1 ,. . . ,xn typ˚ u β1 , . . . , βn , konstruuje objekt/funkci typu (αβ1 . . . βn ) λx1 . . . xn [Y ] . . . (αβ1 . . . βn ) U aplikace i abstrakce se tady jedn´a o z´apis funkc´ı v´ıce promˇenn´ych, ne o ˇc´asteˇcn´e aplikace ´ Uvod do umˇ el´ e inteligence 9/12
32 / 34
Transparentn´ı intenzion´ aln´ı logika
Konstrukce
Pˇr´ıklady anal´yzy podstatn´ych jmen pes, ˇclovˇek
x . . . ι: peswt x, pes/(oι)τ ω
individuum z dan´e tˇr´ıdy individu´ı
prezident
prezident/ιτ ω
individuov´a role
volitelnost
volitelnost/(oιτ ω )τ ω
vlastnost individuov´e role
v´yˇska
v´yˇska/(τ ι)τ ω
empirick´a funkce
v´yrok, tvrzen´ı
p . . . ∗n : v´ yrokwt p, v´yrok/(o∗n )τ ω
konstrukce propozice z dan´e tˇr´ıdy konstrukc´ı propozic
v´alka, sm´ıch, zvonˇen´ı
v´alka/(o(oπ))ω
tˇr´ıda epizod – aktivita, kter´a koresponduje se slovesem
leden, podzim
leden/(o(oτ ))
tˇr´ıda ˇcasov´ych ˇcasov´e intervaly
´ Uvod do umˇ el´ e inteligence 9/12
33 / 34
okamˇzik˚ u
–
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e]
´ Uvod do umˇ el´ e inteligence 9/12
34 / 34
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e] existence neexistuj´ıc´ıho Pes existuje. v PL1:
Jednoroˇzec neexistuje.
∃x(x = pes)
´ Uvod do umˇ el´ e inteligence 9/12
¬∃x(x = jednoroˇzec)
34 / 34
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e] existence neexistuj´ıc´ıho Pes existuje. v PL1:
Jednoroˇzec neexistuje.
∃x(x = pes)
¬∃x(x = jednoroˇzec)
(jednoroˇzec = jednoroˇzec)⇒(∃x(x = jednoroˇzec))
´ Uvod do umˇ el´ e inteligence 9/12
34 / 34
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e] existence neexistuj´ıc´ıho Pes existuje. v PL1:
Jednoroˇzec neexistuje.
∃x(x = pes)
¬∃x(x = jednoroˇzec)
(jednoroˇzec = jednoroˇzec)⇒(∃x(x = jednoroˇzec))
´ Uvod do umˇ el´ e inteligence 9/12
34 / 34
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e] existence neexistuj´ıc´ıho Pes existuje.
Jednoroˇzec neexistuje.
∃x(x = pes)
v PL1:
¬∃x(x = jednoroˇzec)
(jednoroˇzec = jednoroˇzec)⇒(∃x(x = jednoroˇzec)) v TILu:
(*)
λw λt 0¬[Ex wt jednoroˇ zec] hP i df Ex = λw λtλp 0 ι λx[pwt x] ,
Ex . . . (o(oι)τ ω )τ ω
(*) . . . “tˇr´ıda vˇsech individu´ı s vlastnost´ı ‘b´yt jednoroˇzcem’ je v dan´em svˇetˇe a ˇcase pr´azdn´a.”
´ Uvod do umˇ el´ e inteligence 9/12
34 / 34
Transparentn´ı intenzion´ aln´ı logika
Pˇr´ıklady pˇr´ınosu TILu
Pˇr´ıklady pˇr´ınosu TILu propoziˇcn´ı postoje Petr ˇr´ık´a, ˇze Tom vˇeˇr´ı, ˇze Zemˇe je kulat´a. h h ii λw λt ˇr´ık´ awt Petr 0 λw λt vˇ eˇr´ıwt Tom0 λw λt[kulat´ awt Zemˇ e] existence neexistuj´ıc´ıho Pes existuje.
Jednoroˇzec neexistuje.
∃x(x = pes)
v PL1:
¬∃x(x = jednoroˇzec)
(jednoroˇzec = jednoroˇzec)⇒(∃x(x = jednoroˇzec)) v TILu:
(*)
λw λt 0¬[Ex wt jednoroˇ zec] hP i df Ex = λw λtλp 0 ι λx[pwt x] ,
Ex . . . (o(oι)τ ω )τ ω
(*) . . . “tˇr´ıda vˇsech individu´ı s vlastnost´ı ‘b´yt jednoroˇzcem’ je v dan´em svˇetˇe a ˇcase pr´azdn´a.”
intenzionalita, vlastnosti vlastnost´ı, anal´yza epizod, anal´yza gramatick´eho ˇcasu, . . . ´ Uvod do umˇ el´ e inteligence 9/12
34 / 34
