KAPITOLA 2. LOGICKE' MODELY ARGUMENTA'CIE 7 zamy'z't,any' ako pri'stup k teo'rii poznania cez rozhovor, diskusiu.
Filozof Rainer Hegselmann [Heg 85] analyzoval za'kladne' kroky, ktore' vedu' k vhodnej formaliza'cii dialektiky, rozobral meto'dy, heuristiky a tech- niky, ktore' sa daju' rozumne pou?i'vaz.. Formalizoval tie? za'kladny' model pre dialekticke' usudzovanie. Pou?i'va preo` na'zov forma'lna dialektika, aby bol zrejmy' rozdiel medzi o`ou a Aristotelovou dialektikou, ktora' forma'lne na'- stroje postra'da.
Ronald Loui [Lou 91, Lou 93] zasa priamo sku'mal vhodnosz. forma'lnej dialektiky ako za'klad pre nemonoto'nne a anulovatet,ne' usudzovanie, kei" be- rieme oht,ad na vy'poe`tove' obmedzenia. V jeho pri'stupe sa pravidla', ktore' pricha'dzaju' do konfliktu, pova?uju' za pla'ny (strate'gie) pre deliberati'vny proces. Tvrdi', ?e dialekticke' protokoly su' vhodne' pre take'to usudzovanie, kei" ma'me obmedzene' zdroje, a kei" je vy'poe`et se'riovy'. Louiho sa vo svojej pra'ci zaobera' tie? ht,adani'm odvodzovaci'ch vzorov v pra'vnej argumenta'cii a konceptualizovani'm argumentae`ny'ch hier, ktore' poma'haju' objasniz., ako sa da' take'to odvodzovanie s obmedzeny'mi zdrojmi realizovaz..
Gerard Vreeswijk [Vre 93] vyvinul teo'riu argumenta'cie, ktoru' nazval abs- traktny' argumentae`ny' syste'm. Pova?uju'c tu'to teo'riu za za'klad, sku'mal dia- lekticke' proble'my modeluju'c procedu'ru presviede`ania ako rozhovor medzi dvoma stranami, proponentom a oponentom.
Thomas Gordon [Gor 94] formuloval thThe Pleadings Gamess ako nor- mati'vnu formaliza'ciu a vy'poe`tovy' model pra'vnej obhajoby. Do^sledky argu- mentov a protiargumentov sa modeluju' pomocou podmienene'ho vyply'vania. Konflikty sa riez'ia diskusiou (argumentovni'm) o platnosti a priorite pravidiel.
Henry Prakken a Giovanni Sartor [PrS 96] vytvorili syste'm na zruz'itet,nu' argumenta'ciu, aby z'tudovali niektore' logicke' pojmy v pra'vnych sporoch. Tvr- dili, ?e aby teo'ria argumenta'cie bola realisticka', mala by vediez. meniz. priority argumentov a to tie? ako vy'sledok argumenta'cie. To viedlo k druhe'mu sys- te'mu, v ktorom u? priority neboli pevne', ale tie? sa o nich dalo argumentovaz..
Pri'stup Barta Verheija [Ver 96] k argumenta'cii je dvojake'ho druhu. Na jednej strane analyzoval u'lohu pravidiel a do^vodov a ich do^le?ity'ch vlastnosti' v argumenta'cii, na druhej strane uva?oval aj o u'lohe procesu argumenta'cie, analyzoval, e`o ure`uje, ?e na istej u'rovni tohto procesu ma' byz. dany' argument zruz'eny'.
2.3 Porovna'vanie argumentov Loui [Lou 87] prezentoval forma'lnu ideu thruz'enia medzi argumentamiss, ktora' sa sna?ila uplato`ovaz. myz'lienky pravdepodobnostne'ho a indukti'vneho od- vodzovania na kolekcia'ch ruz'itet,ny'ch pravidiel. Porovnanie bolo zalo?ene' na
KAPITOLA 2. LOGICKE' MODELY ARGUMENTA'CIE 8 z'truktu're argumentov. Bolo viac krite'rii', ako napr. z'pecifickosz. pravidla, pria- moe`iarosz., viac do^kazov alebo preferovanie nejakej premisy.
Za spomenutie stoji' tie? pra'ca Davida Poola [Poo 88]. Jeho syste'm The- orist dovot,oval konfliktne' scena're, ktore' sa dali porovna'vaz.. Krite'riom bola z'pecifickosz.. Poole tie? ponu'kol novy' pri'stup na riez'enie proble'mu viacna'sob- ny'ch extenzii' v nemonoto'nnom usudzovani'. Tvrdil, ?e defaulty su' mo?ny'mi hypote'zami, ktore' mo^?u vysvet,ovaz. ota'zky v danej teo'rii, ky'm su' konzist- nentne' so zvyz'kom dostupny'ch poznatkov.
Geffner a Pearl [GeP 92] prezentovali teo'riu dokazovania ruz'itet,ny'ch kon- diciona'lov, ktora' bola zalo?ena' na myz'lienkach provna'vania argumentov. Ta'to teo'ria bola odvodena' z modelovo-teoretickej se'mantiky so z'truktu'rou preferovany'ch modelov. Rela'cia usporiadania odra'?a pojem z'pecifickosti mo- delu.
Henry Prakken [Pra 96] sku'mal preferencie pri porovna'vani' argumentov a kombinovani' viacery'ch spo^sobov ruz'enia v pra'vnom spore. Pri porovna'vani' uva?oval o hierarchii, z'pecifickosti a e`ase, ky'm sa za'ver dostane do platnosti.
Bart Verheij [Ver 96] uva?oval ro^zne typy napa'dania argumentov roz- z'i'reni'm Pollockove'ho vyvra'tenia a podkopania. Vytvoril forma'lny model, v ktorom argument mo^?e byz. porazeny' sekvene`ny'm zoslabovani'm (pospa'jani'm tak vet,a do^vodov, ?e za'ver u? jednoducho nemo^?e platiz.) alebo paralelny'm zosilo`ovani'm (spolupra'ca dvoch argumentov porazi' jeden z dvoch argumen- tov). Vz'eobecnejz'i'm druhom ruz'enia mo^?e kolekti'vna pora'?ka, kei" skupina argumentov je porazena' ako celok, ale ?iadny jednotlivy' argument zo sku- piny nie je porazeny'. Nedeterministicke' zruz'enie je, kei" je niekot,ko mo?nosti' vy'beru argumentov a tento vy'ber je nedeterministicky'.
Kapitola 3 Vy'chodiska'
3.1 Dungova argumentae`na' teo'ria Phan Minh Dung vyvinul argumentae`nu' teo'riu, ktora' je rozz'i'reni'm logic- ke'ho programovania. Jej hlavnou myz'lienkou je akceptovatet,nosz. argumen- tov. Ukazuje tie?, ?e va"e`z'ina do^le?ity'ch pri'stupov k nemonoto'nnemu usudzo- vaniu v UI a logicke'mu programovaniu sa zda' byz. z'pecia'lnym pri'padom jeho teo'rie argumenta'cie.
Dung ht,ada' ra'mec, ktory' by bol vhodny' pre se'mantiku rozz'i'reny'ch lo- gicky'ch programov s explicitnou nega'ciou. Rozz'i'reny' logicky' program P sa sklada' z kla'uz tvaru:
L
0
L
1
; : : : ; L
m
; not-L
m+1
; : : : ; not-L
m+n
;
kde L
i
su' objekti'vne litera'ly. Objekti'vny litera'l je A alebo :A, kde A je
ato'm. Litera'ly tvaru not-L nazy'vame subjekti'vne a su' to predpoklady, na ktory'ch je zalo?eny' do^kaz. Kei"?e akceptovanie do^kazu za'visi' od akcepto- vania predpokladov, na ktory'ch je za'visly', argumentovaz. za za'ver znamena' argumentovaz. za predpoklady, na ktory'ch je za'ver za'visly'. A teda, na ar- gumenty sa da' pozeraz. ako na mno?iny predpokladov, alebo ekvivalentne, ako na mno?iny za'kladny'ch inz'tancii' subjekti'vnych litera'lov. Argument A podporuje objekti'vny litera'l L, ak existuje do^kaz pre L zalo?eny' na predpo- kladoch v A. Argument doka'?e poraziz. sa'm seba, ak podporuje za'roveo` L aj :L, kde L je objekti'vny litera'l.
Dung rozliz'uje dva spo^soby atakovania argumentu:
ffl Argument A atakuje A
0
redukciou ad absurdum (RAA-atak), ak A [ A
0
doka'?e poraziz. sama seba.
ffl Argument A atakuje argument A
0
za'kladny'm u'tokom (ground attack)
(g-atak), ak existuje predpoklad not-L v A
0
, taky', ?e A podporuje L.
9
KAPITOLA 3. VY'CHODISKA' 10
Ak ma'me logicky' program P , jeho se'mantika je definovana' se'mantikou argumentae`ne'ho ra'mca:
AF (P ) =! AR
P
; ataky; g-ataky ?;
kde su' splnene' nasleduju'ce podmienky:
ffl AR
P
oznae`uje mno?inu vz'etky'ch argumentov vzht,adom na P
ffl ataky = RAA-ataky [ g-ataky
Kei" ma'me mno?inu argumentov S taku', ?e ?iadne dva elementy S sa ne- atakuju' navza'jom, hovori'me, ?e S je nekonfliktna'. Argument A je akceptova- tet,ny' vzht,adom na mno?inu S, ak pre t,ubovot,ny' argument B, ktory' atakuje A, je B g-atakovane' nejaky'm argumentom A
0
2 S. Nekonfliktna' mno?ina ar-
gumentov S je prijatet,na', ak ka?dy' argument v S je akceptovatet,ny' vzht,adom na S.
Dung pre tento ra'mec definoval ro^zne se'mantiky, zalo?ene' na myz'lienke extenzii':
ffl preferovana' extenzia - maxima'lna prijatet,na' mno?ina argumentov. Uka'-
zal, ?e taka'to v?dy existuje
ffl stabilna' extenzia - nekonfliktna' mno?ina argumentov S je stabilnou ex-
tenziou, ak S g-atakuje vz'etky argumenty, ktore' nepatria do S. Ta'to se'- mantika je zhodna' s answer-set se'mantikou rozz'i'reny'ch logicky'ch prog- ramov.
ffl uzemnena' (grounded) extenzia - najmenz'i' pevny' bod charakteristickej
funkcie ra'mca AF definovanej takto: F
AF
(S) = fA j A je akceptova-
tet,na' vzht,adom na Sg.
ffl u'plna' extenzia - prijatet,na' mno?ina argumentov S je u'plnou extenziou,
ak ka?dy' argument, ktory' je akceptovatet,ny' vzht,adom na S, patri' do S.
Nesko^r Dung predstavil dokonca ez'te viac abstraktny' argumentae`ny' ra'- mec, kde je atak medzi argumentmi reprezentovany' iba jednou bina'rnou rela'ciou. Ta'to nova' teo'ria zdiet,a va"e`z'inu vlastnosti', ktore' ma' tento syste'm. Autor tie? ukazje, ?e jeho teo'ria argumenta'cie je zovz'eobecneni'm ro^znych zna'mych formaliza'cii' nemonoto'nneho usudzovania.
KAPITOLA 3. VY'CHODISKA' 11 3.2 Theorist Abstraktny', argumentae`no-teoreticky' ra'mec pre defaultove' usudzovanie je zalo?eny' na myz'lienkach pa'na Poola. Poole opi'sal v [Poo 88] origina'lny pri'- stup k defaultove'mu usudzovaniu a tento pri'stup aj implementoval.
l^tandardny' pri'stup k nemonoto'nnemu usudzovaniu je taky', ?e vytvori'me logiku, v ktorej je definovany' nejaky' inferene`ny' stroj, ktory' nazy'vame aj genera'torom hypote'z a ten ma' schopnosz. odvodzovaz. (navrhovaz., generovaz.) hypote'zy.
Poole navrhol namiesto konz'trukcie novej logiky schopnej usudzovaz. ne- monoto'nne zmeniz. uhol poht,adu. K defaultove'mu usudzovaniu navrhol pri- stupovaz. ako k tvoreniu teo'rii', ako k vy'beru hypote'zy z danej mno?iny hypo- te'z, umo?o`uju'cich vysvetliz. nejake' pozorovania. Usudzovanie take'hoto typu mo?no cha'paz. ako konz'trukciu konzistentnej teo'rie zo zna'mych faktov a vy- braty'ch hypote'z tak, aby bolo mo?ne' vysvetliz. dane' pozorovania.
V syste'me su' tri mno?iny prvora'dovy'ch formu'l, ktore' zada'va u?i'vatet,:
F je mno?ina uzavrety'ch formu'l, ktore' vola'me fakty. Tieto su' pova?ovane'
za pravdive' v svete, ktory' modelujeme.
\Delta je mno?ina formu'l, ktore' hraju' u'lohu mo?ny'ch hypote'z, ktory'ch za'kladne'
inz'tancie mo^?u byz. pou?ite' na vysvett,ovanie, ak su' konzistentne'.
C je mno?ina formu'l, ktore' su' obmedzeniami. Tieto ure`uju', e`o mo^?e byz.
odvodene' a e`o nie.
Predpoklada'me, ?e F [ C je konzistentne'.
Jazyk obsahuje deklara'cie fact, default a constraint, pomocou ktory'ch tieto mno?iny zada'vame. Argumentami su' nejake' formuly. Posledna' z dekla- ra'cii' je ure`ena' na situa'cie, v ktory'ch ma' defaultova' teo'ria viac extenzii' a tvorca syste'mu chce niektore' z nich vylu'e`iz. ako anoma'lie. Ota'zky sa fromu- luju' deklara'ciou explain. Jej argumentom je tie? formula.
Defini'cia 3.1 Scena'r z (F ; \Delta ) je mno?ina D[F , kde D je mno?ina vz'etky'ch za'kladny'ch inz'tancii' elementov z \Delta , taka', ?e D [ F [ C je konzistentne'.
Defini'cia 3.2 Ak g je uzavreta' formula, potom vysvetlenie g z (F ; \Delta ) je scena'r (F ; \Delta ), z ktore'ho vyply'va g.
Tak?e, g sa da' vysvetliz. z (F ; \Delta ), ak existuje mno?ina D za'kladny'ch inz'tancii' elementov z \Delta , take', ?e
F [ D j= g a F [ D [ C je konzistentne'.
F [ D je potom vysvetlenie g.
KAPITOLA 3. VY'CHODISKA' 12 Defini'cia 3.3 Extenzia z (F ; \Delta ) je mno?ina vz'etky'ch logicky'ch do^sledkov maxima'lneho (vzht,adom na inklu'ziu) scena'ra z (F ; \Delta ).
Deklara'cia constraint tie? umo?o`uje po?adovaz., aby scena'r bol konzis- tentny' s formulou, ktora' je argumentom constrainu.
Odpovei"ou na ota'zku explain OE je no, ak OE nevyply'va z maxima'lneho scena'ra alebo yes spolu so zoznamom hypote'z, ktore' treba prijaz. do scena'ra, ak z take'hoto rozz'i'rene'ho scena'ra vyply'valo OE.
Jazyk obshuje ez'te deklara'ciu predict, ktorej argumentom je formula. Od- povei"ou je yes spolu z mno?inou vz'etky'ch vysvetleni', ak formula je v ka?dej extenzii, inak vra'ti no a scena'r, z ktore'ho sa formula vysvetliz. neda'.
V syste'me je mo?ne' rozliz'ovaz. medzi extenziami, kde krite'riom je va"e`z'ia z'pecifickosz..
Syste'm Theorist bol implementovany' v Prologu a umo?o`oval experimen- tovaz. s defaultovy'm usudzovani'm, ale aj s diagnosticky'm usudzovani'm alebo ue`eni'm.
Kapitola 4 Argumentae`ny' ra'mec V [BDK 97] predstavili Bondarenko, Dung, Kowalski a Toni abstraktny' ra'- mec pre defaultove' usudzovanie, ktory' ako z'pecia'lne pri'pady zaha`o`a Theorist, defaultovu' logiku, logicke' programovanie, autoepistemicku' logiku a nemono- to'nne moda'lne logiky.
Tento ra'mec sa da' cha'paz. ako zovz'eobecnenie Theoristu. Toto zovz'eobec- nenie dovot,uje rozz'i'riz. t,ubovot,nu' teo'riu formulovanu' v monoto'nnej logike mno?inou viet, ktore' nazy'vame hypote'zy alebo predpoklady, ktore' su' spolu s teo'riou schopne' vysvetliz. nejake' pozorovanie. Ta'to mno?ina mo^?e byz. isty'm spo^sobom vyvra'tena' alebo porazena'. Teo'riu nazy'vame tie? mno?inou faktov.
Hypote'za mo^?e byz. vyvra'tena' alebo porazena', ak sa da' doka'zaz. jej thpro- tikladss. Mno?inu porazi'me, ak porazi'me nejaku' hypote'zu jej patriacu. Ak sa v nejakej mno?ine nacha'dza hypote'za aj je protiklad, hovori'me o konflikte.
Se'mantika take'hoto ra'mca hovori' o tom, ake' vlastnosti ma' maz. ta'to mno- ?ina, teda e`o pova?ujeme za akceptovatet,ne' rozz'i'renie teo'rie alebo mno?iny faktov.
Do^vere`ive' se'mantiky: Naivna' se'mantika - mno?inu faktov rozz'i'rime o maxima'lnu mno?inu hy-
pote'z, ktore' su' nekonfliktne'
Stabilna' se'mantika - mno?ina hypote'z je nekonfliktna' a spolu s mno?inou
faktov zaha`o`a nega'cie ostatny'ch hypote'z, ktore' nie su' v danom rozz'i'reni'
Pri'pustna' se'mantika - mno?ina hypote'z je akceptovatet,na', ak je nekon-
fliktna' a jej dedukti'vny uza'ver sa ubra'ni proti ka?de'mu u'toku (bra'niz. znamena' atakovaz. vz'etky hypote'zy, ktore' atakuju' jej uza'ver, atakovaz. hypote'zu znamena' odvodiz. jej protiklad)
13
KAPITOLA 4. ARGUMENTAE`NY' RA'MEC 14 Preferene`na' se'mantika - je maxima'lne pri'pustna' (?iadna vlastna' pod-
mno?ina nie je pri'pustna')
U'plna' se'mantika - je pri'pustna' a obsahuje vz'etky hypote'zy, ktore' bra'ni
Skepticke' se'mantiky: Dobre zalo?ena' se'mantika - mno?ina hypote'z, ktore' sa nacha'dzaju' v ka?-
dej u'plnej mno?ine
Cirkumskripcia - mno?ina hypote'z, ktore' sa nacha'dzaju' v ka?dej maxi-
ma'lnej nekonfliktnej mno?ine
4.1 Za'kladne' po jmy a defini'cie Defini'cia 4.1 Dedukti'vny syste'm je dvojica (L; R), kde
ffl L je forma'lny jazyk so spoe`i'tatet,ny'm mno?stvom viet ffl R je mno?ina odvodzovaci'ch pravidiel tvaru
ff
1
; : : : ; ff
n
ff
kde ff; ff
1
; : : : ; ff
n
2 L a n * 0
Vz'imnime si, ?e axio'my ff mo^?u byz. vyjadrene' ako odvodzovacie pravidla' s n = 0.
e^ubovot,na' mno?ina viet T ` L sa nazy'va teo'ria. Odvodenie z mno?iny T je postupnosz. fi
1
; : : : ; fi
m
, kde m ? 0, v ktorej
8i = 1; : : : ; m,
ffl fi
i
2 T , alebo
ffl existuje
ff
1
;:::;ff
n
fi
i
z R, kde ff
1
; : : : ; ff
n
2 ffi
1
; : : : fi
i\Gamma 1
g.
T ` ff znamena', ?e existuje odvodenie z T , kde posledna' veta je ff (inak povedane', ff sa da' odvodiz. z T ).
T h(T ) je mno?ina fff 2 L j T ` ffg. Kei"?e vz'etky odvodenia maju' konee`nu' da*?ku, ka?dy' dedukti'vny syste'm (L; R) je kompaktny' v zmysle, ?e kei" T ` ff, potom T
0
` ff pre nejaku'
konee`nu' podmno?inu T
0
z T .
Taktie? ka?dy' dedukti'vny syste'm je monoto'nny, t.j. ak T ` T
0
, potom
T h(T ) ` T h(T
0
).
KAPITOLA 4. ARGUMENTAE`NY' RA'MEC 15 Defini'cia 4.2 Nech (L; R) je dedukti'vny syste'm. Argumentae`ny' ra'mec vzht,a- dom na (L; R) je trojica (T; Ab; _ ), kde
ffl T; Ab ` L a Ab 6= ;, ffl _ je zobrazenie z Ab do L, kde ff oznae`uje thprotikladss ff
Pod protikladom rozumieme, ?e ff a ff su' tvrdenia, ktore' sa navza'jom vylue`uju'. Mo^?u to byz. napr. symboly p; :p alebo vety typu thIdem zajtra do Prahy.ss, thIdem zajtra do Bena'tok.ss.
Teo'ria T vyjadruje mno?inu faktov, Ab zasa mno?inu hypote'z, pomocou ktorej spolu s faktami chceme vysvetliz. nejake' pozorovanie.
V i"alz'om texte budeme pou?i'vaz. iba skratku argumentae`ny' ra'mec v zmysle argumentae`ny' ra'mec vzht,adom na pri'sluz'ny' dedukti'vny syste'm.
V kontraste s predcha'dzaju'cim formalizmom [BTK 93], ktore'ho vylep- z'eni'm je tento ra'mec, sa nesna?i'me redukovaz. pojem protikladu na pojem nekonzistentnosti. Ani kei" logika v pozadi' dovot,uje nekonzistentnosz., nepred- poklada'me, ?e nekonzistencia implikuje vz'etky vety jazyka.
Defini'cia 4.3 Nech (T; Ab; _ ) je argumentae`ny' ra'mec a \Delta ` Ab,
ffl \Delta je nekonfliktna' pra've vtedy, kei" pre ka?de' ff 2 Ab, T [ \Delta 6` ff; ff, ffl \Delta je maxima'lne nekonfliktna' pra've vtedy, kei" \Delta je nekonfliktna' a ne-
existuje nekonfliktna' \Delta
0
oe \Delta
Kei" ma'me nejaku' mno?inu predpokladov \Delta , mo^?eme urobiz. dedukti'vny uza'ver T h(T [ \Delta ) teo'rie T [ \Delta . Tento dedukti'vny uza'ver sa v literatu're o nemonoto'nnej logike nazy'va extenzia. My budeme pojem extenzie pou?i'vaz. pre mno?inu \Delta , v zmysle rozz'i'renie teo'rie o mno?inu \Delta .
Uvedieme ez'te do^le?itu' vetu, ktora' hovori' o existencii maxima'lnej nekon- fliktnej mno?iny, ak existuje aspoo` jedna nekonfliktna' mno?ina:
Veta 4.1 Pre ka?du' nekonfliktnu' mno?inu hypote'z \Delta existuje maxima'lna nekonfliktna' mno?ina hypote'z \Delta
0
taka', ?e \Delta ` \Delta
0
.
Do^kaz: Nech ff
0
; ff
1
; : : : ; ff
n
; : : : je vymenovanie hypote'z z Ab n \Delta . Nech
ffl \Delta
0
= \Delta ,
ffl \Delta
n+1
= \Delta
n
[ fff
n
g, ak \Delta
n
[ fff
n
g je nekonfliktna', a
\Delta
n+1
= \Delta
n
inak.
KAPITOLA 4. ARGUMENTAE`NY' RA'MEC 16
Nech \Delta
0
= [
i
\Delta
i
. Zrejme, \Delta ` \Delta
0
a je t,ahko vidiez., ?e \Delta
0
je maxima'lna
nekonfliktna' mno?ina. 2
Osvie?ime si aj forma'lnu defini'ciu interpreta'cie, ktoru' budeme pou?i'vaz. v nasleduju'cej kapitole.
Defini'cia 4.4 Interpreta'cia jazyka J je dvojica (I; U ), kde:
ffl U je univerzum (dome'na), nejaka' mno?ina (objektov) ffl I je funkcia, ktora'
- ka?dej konz'tante prirai"uje neajky' prvok z U , - ka?de'mu funke`ne'mu symbolu (nenulovej arity n) funkciu z U
n
do
U ,
- ka?dej vy'rokovej premennej jedinu' hodnotu z dvojice (t; f ) (pravda,
nepravda); niekedy sa pou?i'va aj (1, 0),
- ka?de'mu predika'tove'mu symbolu (nenulovej arity n) podmno?inu
U
n
(rela'ciu ae).
Interpreta'ciu termu definujeme rekurzi'vne. Vyu?ijeme, ?e konz'tanta'm su' pri- radene' prvky z U . Predpokladajme, ?e ka?dy' term t
i
, kde i = 1; : : : ; n je in-
terpretovany', t.j. I(t
i
) je nejaky' prvok z U . Potom I(f )(I(t
1
); : : : ; I(t
n
)) je
prvok z U .
Teraz uvedieme pri'klady prepisu niektory'ch logicky'ch formalizmov po- mocou argumentae`ne'ho ra'mca:
4.2 Theorist Nech (L; R) je dedukti'vny syste'm pre klasicku' prvora'dovu' logiku. Abduk- ti'vny ra'mec [Poo 88] je dvojica (T; Ab), kde T ` L je konzistentna' a Ab ` L. Scena'r je konzistentna' teo'ria T [ \Delta , kde \Delta ` Ab. Extenzia T h(T [ \Delta ) je logicky' uza'ver maxima'lneho (vzht,adom na inklu'ziu) scena'ra.
Argumentae`ny' ra'mec prislu'chaju'ci k (T; Ab) je (T; Ab; _ ), kde ff = :ff, pre ka?de' ff 2 Ab.
KAPITOLA 4. ARGUMENTAE`NY' RA'MEC 17 4.3 Logicke' programovanie Predpokladajme, ako zvye`ajne pri logickom programovani', ?e se'mantika lo- gicke'ho programu s premenny'mi, je dana' mno?inou vz'etky'ch jej za'kladny'ch inz'tancii' Herbrandovske'ho univerza prislu'chaju'ceho jazyku logicke'ho prog- ramu.
Herbrandovske' univerzum prislu'chaju'ce k dane'mu logicke'mu programu pozosta'va zo vz'etky'ch za'kladny'ch termov, ktore' sa daju' skonz'truovaz. z kon- z'tantny'ch a funke`ny'ch symbolov jazyka logicke'ho programu.
Nech HB je Herbrandovska' ba'za, t.j. mno?ina vz'etky'ch za'kladny'ch ato'- mov, ktore' sa vyskytuju' v Herbrandovskom univerze.
Nech HB
not
je mno?ina fnot ff j ff 2 HBg .
Nech mno?ina Lit = HB [ HB
not
.
Norma'lny logicky' program je mno?ina kla'uz tvaru
ff fi
1
; : : : ; fi
n
kde ff 2 HB; fi
1
; : : : ; fi
n
2 Lit, a n * 0.
Argumentae`ny' ra'mec prislu'chaju'ci k norma'lnemu logicke'mu programu T je (T; HB
not
; _ ) vzht,adom na (L; R), kde
ffl L = Lit [ fff fi
1
; : : : ; fi
n
j ff 2 HB a fi
1
: : : ; fi
n
2 Lit a n * 0g;
ffl R je mno?ina vz'etky'ch odvodzovaci'ch pravidiel tvaru
ff fi
1
; : : : ; fi
n
fi
1
; : : : fi
n
ff
kde ff 2 HB a fi
1
: : : ; fi
n
2 Lit a n * 0;
ffl not ff = ff, pre ka?de' not ff 2 HB
not
.
4.4 Defaultova' logika Nech (L
0
; R
0
) je dedukti'vny syste'm pre klasicku' prvora'dovu' logiku. Defaul-
tova' teo'ria je dvojica (T; D), kde
ffl T ` L
0
ffl D je mno?ina defaultovy'ch pravidiel tvaru
ff; M fi
1
; : : : ; M fi
n
fl
;
kde ff; fi
1
; : : : ; fi
n
; fl 2 L
0
, a n * 0
KAPITOLA 4. ARGUMENTAE`NY' RA'MEC 18
Nech (T; D) je defaultova' teo'ria. K nej prislu'chaju'ci dedukti'vny syste'm (L; R) a argumentae`ny' ra'mec (T; Ab; _ ) je definovany' takto:
ffl L = L
0
[ fM ff j ff 2 L
0
g
ffl R = R
0
[ D
ffl Ab = fM fi j fi 2 L
0
a M fi sa vyskytuje iba v defaultovy'ch pravidla'ch
z Dg
ffl M ff = :ff
4.5 Autoepistemicka' logika Nech (L; R) je dedukti'vny syste'm, kde L je moda'lny jazyk s moda'lnym opera'torom K a R je mno?ina odvodzovaci'ch pravidiel. Zamy'z't,any' vy'znam Kff je, ?e vieme, ?e ff plati'.
Argumentae`ny' ra'mec prislu'chaju'ci k autoepistemickej teo'rii T je (T; Ab; _ ), kde
ffl Ab = fKff j ff 2 Lg [ f:Kff j ff 2 Lg ffl :Kff = ff a Kff = :Kff pre ka?de' ff 2 L
4.6 Nemonoto'nne moda'lne logiky Nemonoto'nne moda'lne logiky sa daju' vyjadriz. dedukti'vnymi syste'mami tvaru (L; R), kde L je prvora'dovy' moda'lny jazyk, ktory' ma' moda'lny opera'tor K a R je mno?ina odvodzovaci'ch pravidiel pre jazyk L. Ro^zne zvolene' mno?iny R zodpovedaju' ro^znym moda'lnym logika'm, ale ka?de' R obsahuje vz'etky inz'tancie thvynucovaciehoss pravidla:
ff Kff
Argumentae`ny' ra'mec prislu'chaju'ci k teo'rii T ` L je trojica (T; Ab; _ ), kde
ffl Ab = f:Kff j ff 2 Lg ffl :Kff = ff pre ka?de' ff 2 L
Kapitola 5 Do^vere`ive' se'mantiky V tejto e`asti popi'z'eme Kripkeho z'truku'ru pre argumentae`ny' ra'mec vhodnu' na vyjadrenie do^vere`ivy'ch se'mantik.
Kripkeho z'truktu'ra je silna' se'manticka' z'truktu'ra. Sklada' sa z mno?iny mo?ny'ch svetov a mno?iny rela'cii. Pod mo?ny'm svetom si mo^?eme predstaviz. nejaky' stav sveta, kontext alebo mno?inu presvede`eni'. Rela'cia, nazy'vana' aj rela'cia dostupnosti definuje, ako sa vieme z jedne'ho mo?ne'ho sveta dostaz. do iny'ch svetov. Ty'mto spo^sobom vieme vyjadriz. su'vislosti medzi mo?ny'mi svetmi.
Forma'lne:
Defini'cia 5.1 Kripkeho z'truktu'ra je dvojica (W; R), kde
ffl W je mno?ina mo?ny'ch svetov ffl R je mno?ina rela'cii', pre ae 2 R je ae ` W \Theta W
Ez'te raz zopakujeme hlavnu' myz'lienku a prijmeme oznae`enia, ktore' bu- deme pou?i'vaz. v i"alz'om texte.
Argumentae`ny' ra'mec sa sklada' z dvoch mno?i'n - mno?iny faktov T a mno?iny hypote'z - Ab.
Z mno?iny hypote'z vyberieme podmno?inu \Delta , ktora' bude maz. iste' roz- umne' vlastnosti.
Rozumne' mno?iny hypote'z budeme teraz vytva'raz. postupne prida'vani'm vhodnej hypote'zy alebo mno?iny hypote'z k mno?ine faktov. To vyjadri'me rela'ciou dostupnosti.
Defini'cia 5.2 Modelom mno?iny faktov T nazy'vame iterpreta'ciu, v ktorej su' splnene' vz'etky vety z T .
Modelom mno?iny T [ \Delta nazy'vame interpreta'ciu, v ktorej su' splnene' vz'etky vety z T [ \Delta .
19
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 20
Ko^li lepz'ej e`itatet,nosti budeme namiesto T [ \Delta ` ff pou?i'vaz. oznae`enie \Delta `
T
ff.
Mo?ny'mi svetmi budu' dvojice - interpreta'cia jazyka a nejaka' podmno?ina mno?iny hypote'z, prie`om budeme pracovaz. iba s rozumny'mi interpreta'ciami, teda s taky'mi, kde su' vz'etky vety pravdive'.
Rela'cia dostupnosti bude bina'rna rela'cia troch druhov:
1. rela'cia - prida' do mno?iny hypote'z vz'etky vety, ktore' sa daju' z danej
mno?iny odvodiz.
2. rela'cia - prida' t,ubovot,nu' hypote'zu alebo prida' hypte'zu, ktora' nespo^sobi'
konflikt (ale len k nekonfliktnej mno?ine)
3. rela'cia - rela'cia atakovania Defini'cia 5.3 Kripkeho z'truktu'ra pre (T; Ab; _ ) bude dvojica (W; R), kde
ffl W - mno?ina mo?ny'ch svetov, kde mo?ny'm svetom je dvojica (I; \Delta ),
kde I je model mno?iny T [ \Delta , \Delta ` Ab
ffl R - bina'rna rela'cia, R ` W \Theta W
R = ae
p
[ ae
o
[ ae
a
, kde
- ae
o
- rela'cia odvodenia
ae
o
= f(w; w
0
) j 9\Delta
0
: \Delta
0
= fff j ff 2 Ab n \Delta : \Delta `
T
ffg, kde
w = (I; \Delta ) a w
0
= (I
0
; \Delta [ \Delta
0
)g
- ae
P
= ae
p
[ ae
p
0
- rela'cia pridania
ae
p
= f(w; w
0
) j 9ff 2 Ab n \Delta ; kde w = (I; \Delta ) a w
0
= (I
0
; \Delta [ fffg)
a ak \Delta je nekonfliktna' mno?ina, potom aj \Delta [ fffg je nekonfliktna' mno?ina g
ae
p
0
= f(w; w
0
) j 9ff 2 Ab n \Delta ; kde w = (I; \Delta ) a w
0
= (I
0
; \Delta [ fffg)g
- ae
a
- rela'cia atakovania
w = (I; \Delta ); w
0
= (I
0
; \Delta
0
); \Delta 6= \Delta
0
ae
a
= f(w; w
0
) j 9ff 2 \Delta
0
: \Delta `
T
ffg
Interpreta'cie I a I
0
patriace dvom ro^znym mo?ny'm svetom nemusia byz.
nutne ro^zne.
Rela'cia pridania sa sklada' z dvoch rela'cii'. Jedna zachova'va nekonfliktnosz., druha' nemusi'. Ak nebude povedane' inak, budeme pojem rela'cia pridania pou?i'vaz. v zmysle rela'cia pridania, ktora' zachova'va nekonfliktnosz..
Vy'znam rela'cie atakovania je trochu iny' ako prvy'ch dvoch, ktore' vyjad- rovali dostupnosz.. Ide iba o popi'sanie vzz.ahu atakovania. Takisto hovori'me,
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 21 ?e w atakuje w
0
, ak existuje (w; w
0
) 2 ae
a
. Ak w atakuje w
0
, nemusi' hnei" w
0
atakovaz. w a opae`ne.
Defini'cia 5.4 Hovori'me, ?e medzi mo?ny'mi svetmi w a w
0
je hrana rela'cie
R pra've vtedy, kei" (w; w
0
) 2 R.
Vzz.ah medzi mo?ny'mi svetmi ure`uju' rela'cie dostupnosti. Po hrana'ch re- la'cie sa vieme dostaz. z jedne'ho mo?ne'ho sveta do druhe'ho. Mo^?eme teda zadefinovaz. pojem cesty po hrana'ch rela'cie, ktory' vyu?ijeme pri ht,adani' roz- umny'ch mno?i'n.
Defini'cia 5.5 Cesta po hrana'ch rela'cie R je postupnosz. mo?ny'ch svetov w
i
taky'ch, ?e medzi mo?ny'mi svetmi w
i
a w
i+1
existuje hrana rela'cie R.
Ak bude z kontextu jasne', o aku' rela'ciu sa jedna', budeme pou?i'vaz. len oznae`enie hrana. Taktie? predpokladajme, aby sme sa vyhli cyklom, ?e v ceste nie su' dva rovnake' hrany.
Defini'cia 5.6 Hovori'me, ?e cesta po hrana'ch rela'cie R terminuje v mo?nom svete w, ak u? neexistuje mo?ny' svet w
0
a hrana rela'cie R taka', ?e (w; w
0
) 2 R.
Pre ka?du' zo se'manti'k ma'me inu' predstavu rozumnej mno?iny. Pojem model argumentae`ne'ho ra'mca budeme pou?i'vaz. v zmysle mo?ny' svet w = (I; \Delta ) Kripkeho z'truktu'ry pre dany' argumentae`ny' ra'mec, kde mno?ina \Delta bude maz. rozumne' vlastnosti podt,a pri'sluz'nej se'mantiky.
Taktie?, ak nie je povedane' inak, vz'ade predpoklada'me argumentae`ny' ra'mec (T; Ab; _ ) a k nemu Kripkeho z'truktu'ru (W; R).
Vo vz'eobecnosti budeme rozumne' mno?iny ht,adaz. tak, ?e zae`neme v mo?- nom svete (I; ;) a i"alej budeme pokrae`ovaz. po hrana'ch pri'sluz'ny'ch rela'cii'. Pre tento mo?ny' svet po?adujeme, aby bol nekonfliktny', teda ; 6` ff; ff, aby sme mohli pou?iz. hrany rela'cie ae
p
. V realite sa v?dy sna?i'me maz. teo'riu v
pozadi' (mno?inu faktov) nekonfliktnu', inak to vet,mi neda'va zmysel.
5.1 Naivna' se'mantika Najjednoduchz'ia mo?nosz., ako vybraz. nejaku' rozumnu' mno?inu, je vybraz. nekonfliktnu' mno?inu. V tejto se'mantike budeme pova?ovaz. za dobre' rozz'i'- renie mno?iny T taku' mno?inu \Delta , ktora' je spolu s T maxima'lne nekonfliktna'.
Defini'cia 5.7 Naivny' model argumentae`ne'ho ra'mca je taky' mo?ny' svet w = (I; \Delta ), kde \Delta je nekonfliktna' a maxima'lna vzht,adom na inklu'ziu.
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 22 Veta 5.1 Mo?ny' svet w = (I; \Delta ) je naivny'm modelom argumentae`ne'ho ra'mca, ak existuje cesta po hrana'ch rela'cie pridania, ktora' zae`i'na v mo?- nom svete (I
0
; ;) a terminuje vo w.
Do^kaz: Uka'?eme, ?e ak existuje cesta po hrana'ch rela'cie pridania, ktora' zae`i'na v nejakom modeli T a terminuje vo w = (I; \Delta ), potom \Delta vo w je maxima'lna a nekonfliktna' mno?ina.
Ht,adajme teda vhodnu' cestu. Zae`neme v nejakom modeli T . Kei"?e ka?dy' taky'to model je aj mo?ny'm svetom, oznae`i'me si ho w
0
= (I
0
; ;).
Zoberme si t,ubovot,ny' mo?ny' svet w
1
= (I
1
; fffg), kde ff 2 Ab a T [
fffg je nekonfliktne'. I
1
je t,ubovot,na' interpreta'cia, ktora' spa*o`a ff. Kei"?e ; je
nekonfliktna', (w
0
; w
1
) 2 ae
p
a ma'me zae`iatoe`nu' hranu. Taky'chto hra'n mo^?e
byz. viac, na'm stae`i', ak bude existovaz. aspoo` jedna. Ak nie, prehla'sime w
0
za naivny' model.
I"alej sa dostaneme po hrana'ch rela'cie pridania ae
p
len vtedy, ak k ff pri-
da'me vetu, ktora' nespo^sobi' konflikt a ta'to mno?ina viet bude v pri'sluz'nej interpreta'cii' pravdiva'. (Ta'to interpreta'cia sa mo^?e meniz..) Taky'mto postup- ny'm prida'vani'm konz'truujeme cestu po hrana'ch rela'cie ae
p
.
Cestu skone`i'me, ak sa dostaneme do mo?ne'ho sveta, z ktore'ho u? nevy- cha'dza hrana rela'cie ae
p
. Teda cesta na'm terminuje a tento posledny' mo?ny'
svet oznae`i'me w = (I; \Delta ).
2
Pozna'mka 5.1 Veta (4.1) hovori', ?e ak existuje nejaka' nekonfliktna' mno- ?ina, potom existuje maxima'lna nekonfliktna' mno?ina. Ale ta'to mno?ina je potencia'lne nekonee`na'. Teoreticky sa vieme k nej dostaz. aj po hrana'ch rela'- cie pridania, lebo skone`i'me v nekonee`ne, ale ak tento postup pova?ujeme za aky'si na'vod, ako prakticky na'jsz. dobru' mno?inu, tak neskone`i'me nikdy.
5.2 Stabilna' se'mantika V tejto se'mantike pova?ujeme za rozumnu' taku' mno?inu, ktorou sme schopni' vysvetliz. nejake' pozorovanie a za'roveo` vyvra'tiz. vz'etky ostatne' hypote'zy z Ab.
Inak povedane', mno?ina je stabilna' v tom zmysle, ?e mno?inu hypote'z vieme rozdeliz. na hypote'zy, ktore' platia a hypote'zy, ktore' vieme vyvra'tiz. (teda neplatia).
Defini'cia 5.8 Nech (T; Ab; _ ) je argumentae`ny' ra'mec,
ffl mno?ina hypote'z \Delta ` Ab atakuje hypote'zu ff 2 Ab pra've vtedy, kei"
T [ \Delta ` ff
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 23
ffl mno?ina hypote'z \Delta ` Ab atakuje mno?inu hypote'z \Delta
0
` Ab pra've
vtedy, kei" \Delta atakuje nejaku' hypote'zu ff 2 \Delta
0
Lema 5.1 Nekonfliktna' mno?ina hypote'z \Delta ` Ab neatakuje samu seba. Do^kaz: Vyply'va priamo z defini'cii' (4.3) a (5.8) 2 Defini'cia 5.9 Nech (T; Ab; _ ) je argumentae`ny' ra'mec. Mno?ina hypote'z \Delta ` Ab je uzavreta' pra've vtedy, kei" \Delta = fff 2 Ab j T [ \Delta ` ffg.
Lema 5.2 Uzavreta' mno?ina hypote'z \Delta ` Ab je nekonfliktna' pra've vtedy, kei" \Delta neatakuje samu seba.
Do^kaz: Nech \Delta je uzavreta', t.j. \Delta = fff 2 Ab j T [ \Delta ` ffg.
): Vyply'va z predcha'dzaju'cej vety. (: Sporom. Nech \Delta neatakuje samu seba ^ \Delta je konflikna'. Potom (9ff 2
Ab) T [ \Delta ` ff; ff. Kei"?e \Delta neatakuje samu seba, ff 62 \Delta alebo ff 62 \Delta . Ale to znamena', ?e \Delta nie je uzavreta'. Spor.
2
Lema 5.3 Maxima'lna nekonfliktna' mno?ina hypote'z \Delta ` Ab je ure`ite uzav- reta'.
Do^kaz: Sporom. Nech \Delta je maxima'lna a nekonfliktna' a nie je uzavreta'. Potom (9ff 2 Ab n \Delta ) T [ \Delta ` ff. Teraz ma'me dve mo?nosti: ff 2 \Delta - spor s nekonfliktnosz.ou alebo ff 62 \Delta - spor s maxima'lnosz.ou. 2
Defini'cia 5.10 Mno?ina hypote'z \Delta je stabilna' pra've vtedy, kei"
ffl \Delta je uzavreta' ffl \Delta neatakuje sama seba ffl \Delta atakuje ka?du' hypote'zu ff =2 \Delta Defini'cia 5.11 Stabilny' model argumentae`ne'ho ra'mca je taky' mo?ny' svet w = (I; \Delta ), kde \Delta je stabilna' mno?ina.
Konz'trukcia je zalo?ena' na tom, ?e vytva'rame maxima'lne nekonfliktnu' mno?inu. V do^kaze nasleduju'cej vete uka'?eme ako na'jsz. taku'to mno?inu pomocou rela'cii' Kripkeho z'truktu'ry a tie?, ?e ak je maxima'lne nekonfliktna' a atakuje vz'etky hypote'zy, ktore' nepatria do tejto mno?iny, tak je stabilna'.
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 24 Veta 5.2 Mo?ny' svet w = (I; \Delta ) je stabilny'm modelom argumentae`ne'ho ra'mca, ak
ffl existuje cesta po hrana'ch rela'cie pridania ae
p
, ktora'
- zae`i'na v (I
0
; ;)
- terminuje vo w
ffl 8ff 2 Ab n \Delta existuje hrana rela'cie atakovania (w; w
ff
) 2 ae
a
, kde w
ff
=
(I
ff
; fffg) je nejaky' mo?ny' svet
Do^kaz:
ffl Konz'trukcia cesty po hrana'ch rela'cie ae
p
, ktora' zae`i'na v nejakom modeli
T a terminuje vo w a to, ?e \Delta je maxima'lna a nekonfliktna', je rovnake' ako v do^kaze pre naivny' model argumentae`ne'ho ra'mca.
ffl Ez'te treba uka'zaz., ?e naozaj stae`i' na'jsz. maxima'lnu nekonfliktnu' mno-
?inu a skontrolovaz. atakovanie ostatny'ch hypote'z.
Z predcha'dzaju'cich liem (5.1, 5.2, 5.3) vyply'va, ?e ak je mno?ina maxi- ma'lna a nekonfliktna', potom je uzavreta' a neatakuje samu seba. Uka'- ?eme ez'te, ?e ak je \Delta stabilna', potom musi' byz. maxima'lna a nekon- fliktna'.
Nech je \Delta stabilna' a
- nech nie je nekonfliktna'. Potom 9ff 2 Ab : T [ \Delta ` ff; ff. Ak
ff 2 \Delta (alebo ani nemusi') a ff 62 \Delta , potom nie je uzavreta'. Ak fff; ffg ` \Delta , potom \Delta atakuje sama seba. Spor.
- nech nie je maxima'lna. Potom 9ff 2 Ab n \Delta : \Delta [ fffg je nekon-
fliktna', t.j. T [ \Delta 6` ff, ale aby \Delta bola stabilna', musi' T [ \Delta ` ff. Spor.
Teda \Delta je stabilna' , \Delta je maxima'lna, nekonfliktna' a atakuje vz'etky ostatne' hypote'zy.
Nakoniec stae`i' skontrolovaz. atakovanie. Ak w atakuje vz'etky w
ff
, t.j.
9(w; w
ff
) 2 ae
a
8ff 2 Ab n \Delta , tak je stabilny'm mo?ny'm svetom argumen-
tae`ne'ho ra'mca.
2
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 25 5.3 Pri'pustna' se'mantika Z argumentae`ne'ho ht,adiska sa zda' byz. stabilna' se'mantika zbytoe`ne obme- dzuju'ca, preto?e musi'me v?dy braz. oht,ad na vz'etky hypote'zy v mno?ine Ab, prie`om niektore' pova?ujeme za pravdive' a ostatne' musia byz. vyvra'tene'. Na druhej strane, naivna' se'mantika, kde dovoli'me aku'kot,vek nekonfliktnu' mno- ?inu hypote'z, je pri'liz' libera'lna, lebo dovot,uje intuiti'vne neakceptovatet,ne' mno?iny. Se'mantika, ktora' je niekde medzi nimi, sa nazy'va pri'pustna'. Za akceptovatet,nu' pova?uje t,ubovot,nu' taku' mno?inu viet, ktora' sa vie ubra'niz. proti ka?de'mu u'toku.
Ubra'niz. sa u'toku znamena' atakovaz. ka?du' mno?inu hypote'z, ktora' ata- kuje naz'u mno?inu. Forma'lnejz'ie je to vyjadrene' v nasleduju'cej defini'cii:
Defini'cia 5.12 Uzavreta' mno?ina hypote'z \Delta ` Ab je pri'pustna' pra've vtedy, kei"
ffl \Delta neatakuje samu seba ffl pre ka?du' uzavretu' mno?inu hypote'z \Delta
0
` Ab plati': ak \Delta
0
atakuje \Delta ,
tak \Delta atakuje \Delta
0
Defini'cia 5.13 Pri'pustny' model argumentae`ne'ho ra'mca je taky' mo?ny' svet w = (I; \Delta ), kde \Delta je pri'pustna' mno?ina.
Pri'pustna' mno?ina musi' byz. v prvom rade uzavreta' a neatakuju'cu samu seba. Podt,a lemy (5.2) stae`i' ht,adaz. uzavretu' a nekonfliktnu' mno?inu. Budeme to robiz. pomocou rela'cii' pridania ae
p
a odvodenia ae
o
a vyu?iti'm nasleduju'cej
lemy:
Lema 5.4 Odvodenie zachova'va nekonfliktnosz.. Do^kaz: Nech \Delta je nekonfliktna' mno?ina, t.j. (8ff 2 Ab) T [ \Delta ` ff; ff
To znamena', ?e nevieme z \Delta odvodiz. naraz ff aj ff a v odvodeni' prida'vame len to, e`o v odvodiz. vieme.
Inak povedane': ak by \Delta
0
= ffi j T [ \Delta ` fig ' fff; ffg, potom by T [ \Delta `
ff; ff. Spor. 2
Ak sme naz'li kandida'ta na pri'pustnu' mno?inu, treba ez'te skontrolovaz., e`i sa ubra'ni ka?de'mu u'toku od ka?dej uzavretej mno?iny.
Mo?ny' svet, kde \Delta je uzavreta' mno?ina, budeme nazy'vaz. uzavrety'm mo?- ny'm svetom.
Lema 5.5 ae
p
` ae
p
0
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 26 Do^kaz: Zrejme' z defini'cie, kei"?e ae
p
ma' oproti ae
p
0
ez'te jednu vlastnosz. naviac.
2
Veta 5.3 Mo?ny' svet w = (I; \Delta ) je pri'pustny'm modelom argumentae`ne'ho ra'mca, ak
ffl existuje cesta po hrana'ch rela'cii' odvodenia a pridania, ktora'
- zae`i'na v (I
0
; ;)
- do w vcha'dza hranou rela'cie odvodenia
ffl pre nejaky' iny' mo?ny' svet w
0
= (I
0
; \Delta
0
), kde \Delta
0
je uzavreta' mno?ina a
existuje (w
0
; w) 2 ae
a
, potom existuje aj (w; w
0
) 2 ae
a
Do^kaz: Uka'?eme, ?e ak nejaky' mo?ny' svet w = (I; \Delta ) spa*o`a podmienky vety, potom je pri'pustny'm modelom.
ffl Potrebujeme uka'zaz., ?e ak existuje cesta, ktora' zae`i'na v nejakom mo-
deli T a do w vcha'dza hranou rela'cie odvodenia, potom w je mo?ny' svet, kde \Delta je uzavreta' a neatakuje samu seba.
Podt,a lemy (5.2) na'm stae`i' ht,adaz. uzavretu' a nekonfliktnu' mno?inu. Zae`neme z t,ubovot,ne'ho modelu T . Nech w
0
= (I; ;). Pra'zdna mno?ina
je nekonfliktna'.
Teraz ma'me 2 mo?nosti, pridaz. nejaku' hypote'zu alebo pridaz. mno?inu hypote'z, ktore' sa daju' odvodiz..
- Pridanie hypote'zy mo^?eme realizovaz. prechodom po hrane (w
0
; w
1
) 2
ae
p
, ktora' na'm podt,a defini'cie zachova' nekonfliktnosz..
- Pridanie mno?iny hypote'z zasa prechodom po hrane rela'cie odvo-
denia ae
o
, ktora' podt,a lemy (5.4) tie? zachova' nekonfliktnosz..
Je zrejme', ?e predcha'dzaju'ca u'vaha plati' aj pre t,ubovot,ny' mo?ny' svet na ceste po hrana'ch ty'chto rela'cii'.
Prechodom po hrane rela'cie odvodenia teda dostaneme uzavretu' mno- ?inu, lebo ta'to rela'cia na'm prida' vz'etky vety, ktore' z danej mno- ?iny vieme odvodiz., e`o spa*o`a defini'ciu uzavretosti. Vz'imnime si, ?e po ka?dej hrane (w
i
; w
i+1
) 2 ae
o
, kde \Delta
i
6= \Delta
i+1
existuje ez'te aj hrana
(w
i+1
; w
i+1
) 2 ae
o
, lebo podt,a defini'cie mo^?eme pridaz. aj pra'zdnu mno-
?inu, ale len v pri'pade, ?e sa neda' odvodiz. nie` ine'. To mo^?eme vyu?iz., aby do mo?ne'ho sveta, ktory' ma' byz. uzavrety' a nekonfliktny', v?dy
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 27
vcha'dzala hrana rela'cie ae
o
, aj kei" prida'me hypote'zu a neda' sa nie` od-
vodiz..
Teda ka?dy' mo?ny' svet, do ktore'ho vcha'dza rela'cia odvodenia, obsahuje mno?inu, ktora' je uzavreta' a neatakuje samu seba. Oznae`me si tohto kandida'ta na pri'pustny' model w = (I; \Delta ).
ffl Ez'te treba skontrolovaz., e`i sa w ubra'ni proti ka?de'mu uzavrete'mu mo?-
ne'mu svetu, ktory' nao`ho u'toe`i'.
Nech w
0
je mo?ny' svet, ktory' atakuje w, to vieme zistiz. z mo?ne'ho sveta
w, tak, ?e existuje hrana (w
0
; w) 2 ae
a
. Tento mo?ny' svet podt,a defini'cie
musi' byz. uzavrety'. Kei"?e nemusi' obsahovaz. mno?inu, ktora' neatakuje samu seba a stae`i' iba uzavretosz., musi' existovaz. cesta z w
0
= (I
0
; ;) do
w
0
po hrana'ch rela'cie pridania ae
p
0
, ktora' nepredpoklada' nekonfliktnosz..
Vy'poe`et cesty pre ka?dy' uzavrety' mo?ny' svet w
0
sa odliz'uje od vy'poe`tu
pre w len pou?iti'm inej rela'cie pridania a ty'm, ?e ideme thopae`ny'mss, t.j. od w
0
do w
0
.
Pre ka?dy' taky'to mo?ny' svet w
0
, ktory' atakuje w, musi' aj w atakovaz.
w
0
, teda musi' existovaz. hrana rela'cie (w; w
0
) 2 ae
a
. V opae`nom pri'pade
w nie je pri'pustny'm modelom argumentae`ne'ho ra'mca.
2
5.4 Preferene`na' se'mantika V tejto se'mantike pova?ujeme za rozumnu' len taku' pri'pustnu' mno?inu, ktora' je maxima'lna vzht,adom na inklu'ziu.
Defini'cia 5.14 Mno?ina hypte'z \Delta ` Ab je preferovana' pra've vtedy, kei" \Delta je maxima'lne (vzht,adom na inklu'ziu) pri'pustna'.
Defini'cia 5.15 Preferovany' model argumentae`ne'ho ra'mca je taky' mo?ny' svet w = (I; \Delta ), kde \Delta je preferovana' mno?ina.
Veta 5.4 Mo?ny' svet w = (I; \Delta ) je preferovany'm modelom argumentae`ne'ho ra'mca, ak
ffl existuje cesta po rela'cia'ch odvodenia a pridania, ktora'
- zae`i'na v (I
0
; ;)
- terminuje vo w hranou rela'cie odvodenia
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 28
- pre nejaky' iny' mo?ny' svet w
0
= (I
0
; \Delta
0
), kde \Delta
0
je uzavreta' mno-
?ina a existuje (w
0
; w) 2 ae
a
, potom existuje aj (w; w
0
) 2 ae
a
Do^kaz: Uka'?eme, ?e ak mo?ny' svet w = (I; \Delta ) spa*o`a podmienky vety, potom je preferovany'm modelom.
Vz'imnime si, ?e jediny'm rozdielom oproti vete (5.3) je, ?e vo w musi' teraz cesta kone`iz., teda cestu konz'truujeme a w ht,ada'me rovnako ako v predcha'- dzajucej vete, len?e na'm nestae`i', aby do w vcha'dzala hrana rela'cie odvodenia a potom mohla cesta pri'padne pokrae`ovaz.. Cesta kone`i' vtedy, kei" u? nevieme i"alej pokrae`ovaz. ?iadnou hranou rela'cie odvodenia alebo pridania. Jediny'm proble'mom by mohlo byz., ?e na konci sa mo^?eme zacykliz. po rela'ciach typu (w
i
; w
i+1
) 2 ae
o
, kde \Delta
i
= \Delta
i+1
^ I
i
6= I
i+1
. Ale kei"?e po?adujeme, aby v ceste
neboli dve rovnake' hrany cesty, skone`i'me po vye`erpani' vz'etky'm interpreta'cii'.
2
5.5 U'plna' se'mantika Kei" u? pova?ujeme nejaku' mno?inu \Delta za dobru' (akceptovatet,nu', rozumnu'), nie je nie` na tom, kei" zaradi'me do mno?iny \Delta aj hypote'zu ff, ktora' je bra'nena' mno?inou \Delta a i"alej prida'me hypote'zu, ktora' je bra'nena' mno?inou \Delta [ fffg, ati". (V zmysle: kto nie je proti na'm, je s nami.)
Opakovane' prida'vanie taky'chto hypote'z mo^?e viesz. k mno?ine, ktoru' na- zy'vame u'plna', ktora' obsahuje nielen \Delta , ale aj vz'etky hypote'zy, ktore' \Delta bra'ni.
Defini'cia 5.16 Mno?ina hypote'z \Delta bra'ni hypote'zu ff pra've vtedy, kei" pre ka?du' uzavretu' mno?inu hypote'z \Delta
0
plati', ?e ak \Delta
0
atakuje ff, potom \Delta atakuje
\Delta
0
n \Delta .
Defini'cia 5.17 Nech (T; Ab; _ ) je argumentae`ny' ra'mec a \Delta ` Ab mno?ina hypote'z,
Def (\Delta ) = fff j \Delta bra'ni ffg
Priamo z defini'cii' plynie nasleduju'ca veta: Veta 5.5 Mno?ina hypote'z \Delta je pri'pustna' pra've vtedy, kei"
ffl \Delta je uzavreta' ffl \Delta ` Def (\Delta )
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 29
Vz'imnime si, ?e mno?ina hypote'z je pri'pustna' pra've vtedy, kei" ju obsa- huje mno?ina hypote'z, ktoru' bra'ni, ale je u'plna' pra've vtedy, kei" je indenticka' s mno?inou, ktoru' bra'ni:
Defini'cia 5.18 Mno?ina hypote'z \Delta je u'plna' pra've vtedy, kei"
ffl \Delta je uzavreta' ffl \Delta = Def (\Delta )
Hnei" z defini'cie vyply'va, ?e ka?da' u'plna' mno?ina hypote'z je pri'pustna'. Na druhej strane, nie ka?da' pri'pustna' mno?ina je u'plna'. Ale:
Veta 5.6 Ka?da' stabilna' mno?ina hypote'z je u'plna'. Do^kaz: Pozri [BDK 97]. 2 Defini'cia 5.19 U'plny' model argumentae`ne'ho ra'mca je taky' mo?ny' svet w = (I; \Delta ), kde \Delta je u'plna' mno?ina.
U'plny' model budeme ht,adaz. tak, ?e na'jdeme nejaky' uzavrety' model. K uzavretej mno?ine budme potom prida'vaz. hypote'zy, ktore' su' bra'nene' touto mno?inou a pri'padne ez'te tu'to mno?inu uzatva'raz..
Ak by ta'to mno?ina u? bola u'plna', nevieme k nej u? pridaz. ?iadnu hypo- te'zu, ktoru' bra'ni.
Rozz'i'rime teda Kripkeho z'truktu'ru o rela'ciu, ktora' na'm prida' vetu, ktora' je bra'nena' naz'ou mno?inou.
Defini'cia 5.20
Nech (W; R) je Kripkeho z'truktu'ra pre argumentae`ny' ra'mec. Nech U = fw j w = (I; \Delta ); kde \Delta je uzavreta' mno?inag je mno?ina uzavrety'ch modelov.
Potom (W
U
; R
U
) je tie? Kripkeho z'truktu'ra, kde
ffl W
U
= W
ffl R
U
= R [ ae
b
, kde
rela'cia bra'nenia ae
b
= f(w; w
0
) j (9ff 2 Ab n \Delta ) 8w
u
= (I
u
; \Delta
u
) 2 U :
ak w
u
atakuje w
ff
= (I
ff
; fffg), potom w atakuje w
00
= (I
00
; \Delta n \Delta
u
)g, a
w = (I; \Delta ), w
0
= (I
0
; \Delta [ fffg)
Veta 5.7 Mo?ny' svet w = (I; \Delta ) je u'plny'm modelom argumentae`ne'ho ra'mca, ak existuje cesta po hrana'ch rela'cii' odvodenia a bra'nenia, ktora'
KAPITOLA 5. DO^VERE`IVE' SE'MANTIKY 30
ffl zae`i'na v nejakom uzavretom mo?nom svete w
u
2 U
ffl terminuje vo w hranou rela'cie odvodenia
Do^kaz:
Ht,adajme cestu, ktora' bude maz. po?adovane' vlastnosti. Aby sme mohli zae`az., potrebujem maz. nejaky' uzavrety' mo?ny' svet. Kvo^li prida'vaniu bra'neny'ch hypote'z vz'ak potrebujeme vz'etky uzavrete' mo?ne' svety.
K uzavrete'mu mo?ne'mu svetu sa vieme dostaz. po hrana'ch rela'cii' ae
p
0
a ae
o
rovnako, ako v druhej e`asti do^kazu pre pri'pustny' model. Takto dostaneme
mno?inu U = fw
u
j w
u
= (I
u
; \Delta
u
), kde \Delta
u
je uzavreta' mno?ina g.
Vyberme teraz t,ubovot,ny' mo?ny' svet w
u
2 U . Tento mo?ny' svet je uzav-
rety', teda nevieme i'sz. i"alej po hrane rela'cie odvodenia. Jediny'm spo^sobom, ako sa dostaz. i"alej, je i'sz. po hrane rela'cie bra'nenia. Ta' v podstate kopi'ruje defini'ciu bra'nenia a dostaneme sa o`ou do mo?ne'ho sveta, ktory' bude maz. pra've o jednu vetu ff, ktoru' bra'nime, viac.
I"alej mo^?eme bui" pridaz. i"alz'iu bra'nenu' vetu alebo sku'siz., e`i sa ez'te neda' niee`o odvodiz.. Skone`i'me, kei" sa u? nebudeme mo^cz. pohnu'z. po ?iadnej hrane. Posledna' hrana v tom pri'pade bude hrana odvodenia. (Ak sme do w priz'li po hrane z ae
b
, tak ez'te existuje (w; w) 2 ae
o
).
2
Kapitola 6 Skepticke' se'mantiky V skeptickej se'mantike priji'mame za'ver vtedy, kei" ten patri' do ka?dej exten- zie teo'rie. V pri'pade argumentae`ne'ho ra'mca, tieto extenzie musia maz. vz'etky nejaku' rovnaku' rozumnu' vlastnosz..
Pre ka?du' do^vere`ivu' se'mantiku vieme na'jsz. pri'sluz'nu' mno?inu. A kei"?e skepticka' verzia pova?uje za rozumnu' len taku' mno?inu, ktora' priji'ma vety, ktore' patria do ka?dej extenzie, budeme konz'truovaz. pra've taku'to mno?inu. A to tak, ?e rozz'i'rime Kripkeho z'truktu'ru definovanu' pre potreby do^vere`ivy'ch se'manti'k o rela'ciu, ktora' vyrobi' tento prienik a tak dostaneme po?adovanu' mno?inu.
V [BDK 97] bolo uka'zane', ?e skepticka' verzia u'plnej se'mantiky je zovz'e- obecnenie dobre zalo?ej se'mantiky logicke'ho programovania a skepticka' ver- zia naivnej se'mantiky (kde ka?dy' model je Herbrandovky' model) je zhodna' s cirkumskripciou.
Defini'cia 6.1
Nech K = (W; R) je Kripkeho z'truktu'ra pre argumentae`ny' ra'mec. Nech U = f(I; \Delta ) 2 W j \Delta je u'plna' mno?ina a I je modelom T [ \Delta g. Nech K
U
= (W
U
; R
U
) je tie? Kripkeho z'truktu'ra pre argumentae`ny' ra'mec,
kde
ffl W
U
= W
ffl R
U
= R [ ae
i
, kde ae
i
= f(w; w
0
) 2 ae
P
j (9ff) (8(I
u
; \Delta
u
) 2 U ) : ff 2 \Delta
u
;
w = (I; \Delta ); w
0
= (I
0
; \Delta [ fffg)g.
Pozna'mka 6.1 Vz'imnime si, ?e rela'cia ae
i
je iba rozz'i'reni'm ae
P
o jednu vlast-
nosz.. Pri konz'trukcii rozumnej mno?iny my sme teda rovnako dobre vystae`ili s ae
P
, ale museli by sme bli?z'ie z'pecifikovaz. vlastnosti cesty.
31
KAPITOLA 6. SKEPTICKE' SE'MANTIKY 32 6.1 Dobre zalo?ena' se'mantika Dobre zalo?ena' se'mantika logicke'ho programovania [GRS 88] je skepticka' se'mantika, ktora' akceptuje za'ver pra've vtedy, kei" plati' v ka?dej kompletnej extenzii. To vedie k nasleduju'cemu zovz'eobcneniu v naz'om ra'mci.
Defini'cia 6.2 Mno?ina hypote'z \Delta je dobre zalo?ena' pra've vtedy, kei" \Delta je prienikom vz'etky'ch u'plny'ch mno?i'n hypote'z.
Defini'cia 6.3 Mno?ina vz'etky'ch u'plny'ch modelov je U = f(I; \Delta ) 2 W j \Delta je u'plnou mno?inou a I je modelom g.
Veta 6.1 Mo?ny' svet w = (I; \Delta ) je dobre zalo?eny'm modelom argumentae`- ne'ho ra'mca, ak existuje cesta po hrana'ch rela'cie ae
i
, ktora' zae`i'na v nejakom
u'plnom mo?nom svete w
;
a terminuje vo w.
Do^kaz: O ka?dom mo?nom svete vieme rozhodnu'z., e`i je u'plny' tak, ?e na'j- deme cestu (ako v do^kaze vety 5.7), ktora' k nemu vedie. Takto vieme na'jsz. mno?inu U = fw
u
j w
u
je u'plny' mo?ny' svet g.
Podt,a defini'cie rela'cie ae
i
sa z jedne'ho mo?ne'ho sveta vieme dostaz. len do
take'ho mo?ne'ho sveta, ktory' ma' naviac jednu vetu, ktora' je v ka?dej u'plnej mno?ine.
Cesta sa skone`i', kei" u? nebudeme vediez. pridaz. ?iadnu vetu. Tento mo?ny' svet oznae`i'me w = (I; \Delta ). 2
Veta 6.2 Nech P je norma'lny logicky' program a (P; Ab _ ) k nemu prislu'- chaju'ci argumentae`ny' ra'mec. Potom \Delta ` Ab je dobre zalo?ena' mno?ina vzht,adom na (T; Ab; _ ) pra've vtedy, kei" fp j P [ \Delta ` pg [ f:p j not p 2 \Delta g je dobre zalo?eny' model P.
Do^kaz: Ta'to veta vyply'va priamo z vy'sledku uka'zane'ho v [Dun 95a]. 2
6.2 Cirkumskripcia Kei"?e cirkumskripcia [McC 80] je zvye`ajne definovana' modelovo-teoreticky, interpretujeme ju syntakticky, v termi'noch mno?i'n hypote'z, kde ka?dy' mo- del je Herbrandovsky' model. To je pri'pad, kei" teo'ria T neobsahuje ?iadne funke`ne' symboly a spa*o`a vetu o jedinee`nostii na'zvov a vetu o uzavretej do- me'ne.
Kei" ka?dy' model je Herbrandovsky' model, cirkumskripcia je skeptickou verziou Theoristu. Kei"?e v Theoriste mo^?e ka?da' mno?ina hypote'z Ab byz.
KAPITOLA 6. SKEPTICKE' SE'MANTIKY 33 t,ubovot,nou podmno?inou jazyka L, pre naz'u pra'cu s cirkumskripciou bude mno?ina Ab pozosta'vaz. zo za'kladny'ch litera'lov pre predika'ty, ktore' su' pevne' a zo za'kladny'ch negati'vnych litera'lov pre predika'ty, ktore' su' minima'lne.
Forma'lnejz'ie, nech T je teo'ria v prvora'dovom jazyku L. Nech P je mno- ?ina predika'tovy'ch symbolov z L, ktory'ch interpreta'cia ma' byz. minimalizo- vana', Z mno?ina predika'tovy'ch symbolov, ktory'ch interpreta'cia sa ma' meniz. a Q mno?ina zvyz'ny'ch predika'tovy'ch symbolov L, ktory'ch interepreta'cia ma' byz. pevna'. Ab = HB
P
:
[ HB
Q
:
[ HB
Q
, kde
ffl HB
P
:
je mno?ina vz'etky'ch viet tvaru
:p(t
1
; : : : ; t
n
)
kde p 2 P ffl HB
Q
:
je mno?ina vz'etky'ch viet tvaru
:q(t
1
; : : : ; t
n
)
kde q 2 Q ffl HB
Q
je mno?ina vz'etky'ch viet tvaru
q(t
1
; : : : ; t
n
)
kde q 2 Q a t
1
; : : : ; t
n
su' ground termy konz'truovatet,ne' zo symbolov jazyka L.
Uka'?eme (kei" ka?dy' model je Herbrandovsky' model), ?e veta ff vyply'va z cirkumskripcie T pra've vtedy, kei" ff plati' vo vz'etky'ch maxima'lnych nekon- fliktny'ch extenzia'ch (T; Ab; _ ), kde fi = :fi.
V z'tandardnej formula'cii' podt,a [Lif 94], veta vyply'va z cikumskripcie T; CIRC[T ; P; Z], minimalizuju'c predika'tove' symboly v P a dovot,uju'c in- terpreta'ciu predika'tovy'ch symbolov z Z meniz. pra've vtedy, kei" veta plati' v ka?dom (P; Z)-minima'lnom modeli T , definovanom takto: Nech M a N su' modely T . Potom N ^
P;Z
M pra've vtedy, kei" sa M a N li'z'ia iba v inter-
preta'cii' P a Z a interpreta'cia P v N je podmno?inou jej interpreta'cie v M . Model M teo'rie T je (P; Z)-minima'lny pra've vtedy, kei" pre ka?dy' model N teo'rie T taky' ?e N ^
P;Z
M je M ^
P;Z
N .
Veta 6.3 Ak ka?dy' model T je Herbrandovsky' model T , potom
1. ka?dy' (P; Z)-minima'lny model M teo'rie T je modelom maxima'lnej
nekonfliktnej extenzie (T; Ab; _ )
KAPITOLA 6. SKEPTICKE' SE'MANTIKY 34
2. ka?dy' model maxima'lnej nekonfliktnej extenzie (T; Ab; _ ) je (P; Z)-
minima'lny model T .
Do^kaz:
1. Nech M je (P; Z)-minima'lny Herbrandovsky' model T . Nech \Delta je mno-
?ina hypote'z M
P
:
[ M
Q
:
[ M
Q
, kde pre S = P alebo S = Q je
M
S
:
= f:ff 2 HB
S
:
j ff 62 M g a M
S
= fff 2 HB
S
j ff 2 M g. Z
(P; Z)-minimality M je zrejme', ?e M
P
:
je maxima'lne a teda T [ M
P
:
[
M
Q
:
[ M
Q
` M
P
.
Preto T [ \Delta je maxima'lna a nekonfliktna'. Okrem toho, z konz'trukcie \Delta vidi'me, ?e M je zrejme modelom T [ \Delta .
2. Nech M je model maxima'lnej nekonfliktnej extenzie T [ \Delta . Z maxima-
lity T [ \Delta vieme, ?e pre ka?dy' ato'm q v predika'te Q plati', ?e q 2 \Delta alebo :q 2 \Delta . I"alej, z maximality T [ \Delta tie? vieme, ?e pre ka?dy' ato'm p v predika'te P plati', ?e ak :p 2 \Delta , potom T [ \Delta ` p. Teda vz'etky modely T [ \Delta sa zhoduju' s extenziami P alebo Q. Predpokladajme teraz, ?e M nie je (P; Z)-minima'lny. Potom musi' existovaz. model N taky', ?e N ^
P;Z
M . Teda N a M sa zhoduju' v extenzii Q a ka?dy'
P-ato'm, ktory' je nepravdivy' v M , je takisto nepravdivy' v N . Preto je N modelom T [ \Delta , ktory' sa nezhoduje s M v extenzii P. Spor.
2
Priamo z tejto vety a z defini'cie cirkumskripcie vyply'va, ?e Do^sledok 6.1 Ak ka?dy' model T je Herbrandovsky' model T , potom pre ka?du' vetu ff 2 L plati': ff plati' v CIRC(T; P; Z) pra've vtedy, kei" ff plati' v ka?dej maxima'lnej nekonfliktnej extenzii (T; Ab; _ ).
Vyu?ijeme predcha'dzaju'ci do^sledok a budeme ht,adaz. prienik maxima'lne nekonfliktny'ch mno?i'n. Za interpreta'cie zoberieme len Herbrandovske' inter- preta'cie.
Konz'trukcia a do^kaz budu' rovnake' ako v predcha'dzaju'com pri'pade, len miesto u'plny'ch mno?i'n pou?ijeme maxima'lne nekonfliktne'.
Defini'cia 6.4
Nech K = (W; R) je Kripkeho z'truktu'ra pre argumentae`ny' ra'mec. Nech C = f(I; \Delta ) 2 W j \Delta je maxima'lna nekonfliktna' mno?ina a I je Herbrandovsky'm modelom T [ \Delta g.
Nech K
C
= (W
C
; R
C
) je tie? Kripkeho z'truktu'ra pre argumentae`ny' ra'mec,
kde
KAPITOLA 6. SKEPTICKE' SE'MANTIKY 35
ffl W
C
= W
ffl R
C
= R [ ae
i
, kde ae
i
= f(w; w
0
) 2 ae
P
j (9ff) (8w
m
= (I
m
; \Delta
m
) 2 C) :
ff 2 \Delta
C
g.
Pozna'mka 6.2 Rovnako ako v pozna'mke (6.1) pripomi'name, ?e by sme vy- stae`ili z rela'ciou ae
P
.
Veta 6.4 Nech w = (I; \Delta ) je mo?ny' svet, kde I je Herbrandovska' interpre- ta'cia a \Delta je prienikom vz'etky'ch maxima'lnych nekonfliktny'ch extenzii'. Potom ka?da' veta ff 2 L plati' v CIRC(T; P; Z) pra've vtedy, kei" plati' v mo?nom svete w.
Do^kaz: Vyply'va z defini'cie cirkumskripcie, z predcha'dzaju'cej vety a de- fini'cie rela'cie ae
i
, ktora' vytvori' prienik vz'etky'ch maxima'lne nekonfliktny'ch
extenzii' T . 2
Kapitola 7 Za'ver Argumenta'cia je jedny'm z poht,adov na nemonoto'nne usudzovanie. Jej vy'ho- dou je. . .;
V tejto pra'ci boli predstavene' hlavne' myz'lienky a pra'ce o anulovatet,nej argumenta'cii.
Vybrali sme si jeden kokre'tny formalizmus takejto argumenta'cie a vybu- dovali preo` kripkeovsku' se'mantiku. Pre po^vodne definovane' se'mantiky sme definovali Kripkeho z'truktu'ry a doka'zali, ?e sa vieme po hrana'ch rela'cie dostupnosti takejto Kripkeho z'truktu'ry dostaz. do po^vodnou se'mantikou de- finovanej rozumnej mno?iny.
Vy'hodou Kripkeovskej se'mantiky je, ?e poskytuje aky'si na'vod, ako by sa dali rozumne' mno?iny poe`i'taz., ale kei"?e na'z' pri'stup je abstraktny', uva?ujeme dokonca t,ubobot,ne' interpreta'cie, vy'poe`et by bol, ako je v ty'chto pri'padoch be?ne', vet,mi na'roe`ny'.
36
Literatu'ra [BDK 97] Bondarenko, A., Dung, P., Kowalski, R., Toni, F. An abstract,
argumentation-theoretic framework for default reasoning. Artificial In- telligence 93 (1997), No. 1-2, 63-101
[BTK 93] Bondarenko, A., Toni, F., Kowalski, R., A., An assumption-
based framework for non-monotonic reasoning. Proc. 2nd International Workshop on Programming and Non-monotonic Reasoning. (A. Nerode and L. Pereira eds.) MIT Press (1993), 171-189
[Del 86] Delgrande, J., A propositional logic for natural kinds. In Proc. Cana-
dian Society for Computational Studies of Artificial Intelligence. (Aug. 1986), pp 44-48
[Doy 79] Doyle, J., A Truth Maintenance System. Artificial Intelligence 12,
231-272
[Doy 80] Doyle, J., A Model for Deliberation, Action and Introspection. Ph.
D. thesis, MIT
[Dun 95a] Dung, P., M., An Argumentation Theoretic Foundatin of Logic
Programming. Journal of Logic Programming, Vol 22, No 2, Feb. 1995, 151-177
[Dun 95b] Dung, P., M., On the acceptability of arguments and its fundamen-
tal role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence 77, 321-357
[GeP 92] Geffner, H., Pearl, J., Conditional entailment: Bridging two appro-
aches to default reasoning. Artificial Intelligence 53, 209-244
[Gor 94] Gordon, T., F., Computational dialectics. In First Workshop on
Computational Dialectics (Aug. 1994). Twelfth National Conference on Artificial Intelligence - AAAI '94
37
LITERATU'RA 38 [GRS 88] Van Gelder, A., Ross, K., A., Schlipf, J., S., Unfound sets and
the well-founded semantics for general logic programs. Proc. ACM SIGMOD-SIGACT, Symposium on Principles of Database Systems, (1988)
[GuL 89] Guha, R., V., Lenat, D., B., The Cyc representation language Tech-
nical report, ACT-CYC-454/452-89, MCC
[Heg 85] Hegselmann, R., Formal Dialektik: Ein Beitrag zu einer Theorie des
rationalen Argumentierens. Felix Meiner Verlag
[Hol 00] Holldobler, S., Computational Logic. working material, 2000 [Lif 94] Lifschitz, V., Circumscription. Handbook of Logic in Artificial Intel-
ligence and Logic Programming 3 (D. Gabbay, C. Hogger, J.A. Robin- son, eds.) Oxford University Press (1994) 297-352
[LiS 89] Lin, F., Shoham, Y., Argument Systems: a univorm basis for non-
monotonic reasoning. In Proceeding of the 1st International Conference on Knowledge Representation and Reasoning. (1989), 245-255, Morgan Kaufmann Publishers
[LiS 92] Lin, F., Shoham, Y., A logic of knowledge and justified assumptions.
Artificial Intellgence 57, (1992), 271-289
[Llo 94] Lloyd, J., W., Foundations of Logic Programming. Springer-Verlag,
1984
[Lou 87] Loui, R., P., Defeat Among Arguments: A System of Defeasible In-
fernce. Computational Intelligence 3, 100-106
[Lou 91] Loui, R., P., Ampliative inference, computation and dialectic. In R.
Cummins and J. Pollock Eds., AI and Philosophy.
[Lou 93] Loui, R., P., Process and policy: resource-bounded, non-
demonstrative reasoning. Computational Intelligence 2, 5
[McC 80] McCarthy, J., Circumscription - a form of non-monotonic reaso-
ning Artificial Intelligence 13, (1980), 27-39
[Nut 88] Nute, D., Defeasible Reasoning. In J. H. Fetzer Ed., Aspects of Ar-
tificial Intelligence, pp. 251-288. Norwell, MA: Kluwer Academic Pub- lishers
[Pol 74] Pollock, J., Knowledge and Justification. Princeton.
LITERATU'RA 39 [Pol 87] Pollock, J., Defeasibe Reasoning Cognitive Science 11, 481-518 [Poo 88] Poole, D., A Logical Framework for Default Reasoning Artificial
Intelligence 36(1), 27-47, 1998
[Pra 96] Prakken, H., Logical Tools for Modelling Legal Arguments. Ph. D.
thesis, Vrije University, Amsterdam, Holland
[PrS 96] Prakken, H., Sartor, G., A system for defeasible argumentation, with
defeasible priorities. In Proc. of the International Conference on For- mal Aspects of Practical Reasoning, Bonn, Germany (1996), Springer Verlag
[Res 77] Resher, N., Dialectics, a Controversy-Oriented Apporach to the The-
ory of Knowledge. State University of New York Press, Albany, USA
[Rei 80] Reiter, R., A logic for default reasoning Artificial Intelligence 13,
(1980), 27-47
[SiL 92] Simari, G., R., Loui, R., P., A Mathematical Treatment of Defeasible
Reasoning and its Implementation. Artificial Intelligence 53, 125-157
[Sim 89] Simari, G., R., A Mathematical Treatment of Defeasible Reasoning
and its Implementation. Ph. D. thesis, Washington University, Depart- ment of Computer Science (Saint Louis, Missouri, EE.UU.)
[Sef 97] l^efra'nek, J., Dynamic Kripke structures. CAEPIA'97. Actas de la
VII Conferencia de la Associacio'n Espanola para la Inteligencia Artifi- cial, Malaga 1997, 271-283
[Sef 99] l^efra'nek, J., Belief, knowledge, revisions, and a semantics of non-
monotonic reasoning. In LPNMR'99. Proc. of the 5th Int. Conference Logic Programing and Non-Monotonic Reasoning, El Paso, TX, Sprin- ger, 1999
[Sef 00] l^efra'nek, J., A Kripkean semantics for dynamic logic programming. [Sef 00b] l^efra'nek, J., Inteligencia ako vy'poe`et. IRIS, 2000 [Tou 58] Toulmin, S., The Uses of Arguments. Cambridge University Press [Ver 96] Verheij, B., Rules, Reasons, Arguments: formal studies of argumen-
tation and defeat. Ph. D. thesis, Maastricht University, Holland
[Vre 93] Vreeswijk, G., A., Studies in Defeasible Argumentation. Ph. D. the-