ˇ ´IRODOVEDECK ˇ ´ FAKULTA UNIVERZITY PALACKEHO ´ PR A KATEDRA INFORMATIKY
´ PRACE ´ DIPLOMOVA
Alternativn´ı s´emantika pro atributov´e implikace
2014
Jan Tˇr´ıska
Anotace Pr´ace se zab´yv´a u ´plnou axiomatizac´ı atributov´ych implikac´ı, kter´e popisuj´ı z´avislosti mezi atributy objekt˚ u, kter´e se mˇen´ı v po sobˇe jdouc´ıch ˇcasov´ych okamˇzic´ıch. Tyto atributov´e implikace jsou pravidla ve tvaru kdyˇz-pak vyjadˇruj´ıc´ı pˇr´ıtomnost atribut˚ u objekt˚ u relativnˇe v ˇcase. Jejich v´yznam je urˇcen na z´akladˇe v´yskytu nebo absence atribut˚ u objekt˚ u v po sobˇe jdouc´ıch ˇcasov´ych okamˇzic´ıch. Prezentovan´a axiomatizace je rozˇs´ıˇren´ım klasick´e Armstrongovy u ´pln´e axiomatizace atributov´ych implikac´ı o ˇcasov´e okamˇziky. Klasick´y pˇr´ıpad je pak speci´aln´ı pˇr´ıpad tohoto rozˇs´ıˇren´ı, kdy se uvaˇzuje pouze jeden ˇcasov´y okamˇzik.
Chtˇel bych podˇekovat doc. RNDr. Vil´emu Vychodilovi, Ph.D. za trpˇelivost a ˇcas, kter´y mi vˇenoval, a tak´e za rady a pomoc se zpracov´an´ım t´eto pr´ace.
Obsah ´ 1. Uvod
5
2. Souvisej´ıc´ı pˇ r´ıstupy
7
3. Formule a s´ emantick´ e vypl´ yv´ an´ı
9
4. Axiomatizace
15
5. Vztah k ostatn´ım formalism˚ um
19
Z´ avˇ er
22
Conclusions
23
Reference
24
4
1.
´ Uvod
V pr´aci je pops´an u ´ pln´y axiomatick´y syst´em pravidel ve tvaru kdyˇz-pak, kter´e vyjadˇruj´ı vztahy mezi atributy objekt˚ u, kter´e se mˇen´ı v po sobˇe jdouc´ıch ˇcasov´ych okamˇzic´ıch. Tato pravidla u ´ zce souvis´ı s atributov´ymi implikacemi, kter´ymi se zab´yv´a form´aln´ı konceptu´aln´ı anal´yza [7], ale obsahuj´ı prvek, kter´ym jsou schopny vyj´adˇrit v´yskyt nebo absenci objektov´ych atribut˚ u relativnˇe v ˇcase. Nav´ıc z pohledu toho, ˇze objekty m˚ uˇzou mˇenit sv´e atributy v pr˚ ubˇehu ˇcasu, jsou tato pravidla v pr˚ ubˇehu ˇcasu zachov´ana. Pr´ace vymezuje tyto z´avislosti, jejich v´yznam a ukazuje axiomatizaci s´emantick´eho vypl´yv´an´ı, kter´a vych´az´ı z Armstrongovy axiomatizace [2]. Hlavn´ı z´amˇer byl pˇredpov´ıdat v´yvoj syst´emu v ˇcase na z´akladˇe historick´ych dat. Jednotliv´e stavy syst´emu jsou zaznamen´av´any v diskr´etn´ıch okamˇzic´ıch a jsou pops´any atributy. Pˇredpovˇed’ je pak na z´akladˇe pravidel ve tvaru kdyˇzpak, kter´e se relativnˇe odkazuj´ı na atributy v jin´ych stavech a tato pravidla jsou zachov´ana pro kaˇzd´y absolutn´ı ˇcas. Nakonec se uk´azalo, ˇze se na tento probl´em lze d´ıvat jako na atributov´e implikace z form´aln´ı konceptu´aln´ı anal´yzy (FCA), kde se vhodnˇe pˇrid´a prvek ˇcasu. Pˇripomeˇ nme si tedy nejprve atributov´e implikace a nˇekter´e pojmy z FCA. Vstupem FCA je bin´arn´ı relace I ⊆ X ×Y mezi objekty X a atributy Y , kter´e se ˇr´ık´a form´aln´ı kontext. Ta se ˇcasto zobrazuje ve formˇe tabulky, kde ˇr´adky odpov´ıdaj´ı objekt˚ um, sloupce atribut˚ um a kˇr´ıˇzek/pr´azdn´e m´ısto v tabulce znaˇc´ı, jestli objekt m´a/nem´a dan´y atribut. Hlavn´ı v´ystup FCA je mnoˇzina dvojic shluk˚ u ve vstupn´ıch datech, kter´ym se ˇr´ık´a form´aln´ı koncepty v I. Form´aln´ı koncept je dvojce hA, Bi, kde pro A ⊆ X (naz´yvanou extent) a B ⊆ Y (naz´yvanou intent) plat´ı, ˇze B je mnoˇzina atribut˚ u, kter´e maj´ı vˇsechny objekty z A a obr´acenˇe A je mnoˇzina objekt˚ u, kter´e maj´ı vˇsechny atributy z B. V tabulce pˇr´ısluˇs´ıc´ı I jsou form´aln´ı koncepty nejvˇetˇs´ı obd´eln´ıky skl´adaj´ıc´ı se z kˇr´ıˇzk˚ u. Hlavn´ı vˇeta FCA [7] ˇr´ık´a, ˇze pokud vˇsechny form´aln´ı koncepty I uspoˇr´ad´ame podle mnoˇzinov´e inkluze na extentech, pak dostaneme strukturu naz´yvanou konceptu´aln´ı svaz, kter´y je u ´ pln´ym svazem. Nav´ıc jej´ı druh´a ˇc´ast ˇr´ık´a, ˇze k libovoln´emu u ´ pln´emu svazu existuje form´aln´ı kontext tak, ˇze dan´y svaz je jeho konceptu´aln´ım svazem. Atributov´a implikace nad atributy z Y dan´eho form´aln´ıho kontextu je pak v´yraz ve tvaru A ⇒ B, kde A, B ⊆ Y a vyjadˇruje z´avislost: Pokud m´a objekt vˇsechny atributy ” z A, pak m´a i vˇsechny atributy z B“. Proto v uˇzˇs´ım slova smyslu bychom se mohli na A ⇒ B d´ıvat jako na v´yrokovou formuli ve tvaru implikace mezi konjunkcemi atribut˚ u z Y (kter´e jsou br´any jako v´yrokov´e promˇenn´e). Pro A, B, M ⊆ Y ˇrekneme, ˇze A ⇒ B je pravdiv´a v M pokud plat´ı, ˇze kdyˇz A ⊆ M, pak i B ⊆ M a tento fakt znaˇc´ıme M A ⇒ B. Pokud pak uvaˇzujeme, ˇze Mx je mnoˇzina vˇsech atribut˚ u, kter´e m´a objekt x v I, tedy Mx = {y ∈ Y | hx, yi ∈ I}, pak Mx A ⇒ B je skuteˇcnˇe formalizace v´yznamu A ⇒ B je pravdiv´a pro atributy objektu x, tedy pokud m´a x vˇsechny atributy z A, pak x m´a i vˇsechny atributy
5
z B. Jako pˇr´ıklad vstupu m˚ uˇze b´yt bin´arn´ı relace mezi z´akazn´ıky supermarketu a vˇecmi, kter´e si mohou z´akazn´ıci koupit viz. tabulku 1. Prvn´ı ˇr´adek pak znamen´a, ˇze pan Nov´ak si koupil chleba a s´yr. D´ale m˚ uˇzeme uvaˇzovat atributovou implikaci {s´yr} ⇒ {chleba}, kter´a je pravdiv´a pro vˇsechny z´akazn´ıky, a nebo atributovou implikaci {chleba} ⇒ {s´yr}, kter´a nen´ı pravdiv´a pro z´akazn´ıka Ut´ıkal, protoˇze si koupil chleba, ale nekoupil si k tomu s´yr. z´akazn´ık Nov´ak Mal´a Ut´ıkal Kr´atk´y
chleba ×
ml´eko
pivo
s´yr ×
× × ×
× ×
Tabulka 1. N´akupy z´akazn´ık˚ u Jedn´ım ze z´ajm˚ u FCA je struˇcnˇe popsat mnoˇzinu vˇsech atributov´ych implikac´ı, kter´e jsou splnˇen´e vˇsemi objekty dan´eho form´aln´ıho kontextu. Hlavn´ı pˇr´ıstup [8] k tomuto probl´emu se soustˇred´ı na nalezen´ı neredundantn´ı mnoˇziny atributov´ych implikac´ı, ze kter´e vypl´yvaj´ı pˇresnˇe vˇsechny atributov´e implikace, kter´e jsou splnˇeny v dan´em form´aln´ım kontextu. Kl´ıˇcov´y je tedy pojem vypl´yv´an´ı atributov´ych implikac´ı. Jako v jin´ych logick´ych syst´emech m˚ uˇzeme uvaˇzovat dva z´akladn´ı typy vypl´yv´an´ı, a to s´emantick´e, kter´e je zaloˇzeno na modelech, a syntaktick´e, kter´e je zaloˇzen´e na dokazatelnosti. Mnoˇzinˇe M ⊆ Y ˇr´ık´ame model mnoˇziny Σ atributov´ych implikac´ı, pokud kaˇzd´a A ⇒ B ∈ Σ je pravdiv´a v M. D´ale C ⇒ D s´emanticky plyne ze Σ, ps´ano Σ C ⇒ D, pokud C ⇒ D je pravdiv´a ve vˇsech modelech Σ. S´emantick´e vypl´yv´an´ı atributov´ych implikac´ı m´a u ´ plnou axiomatizaci, coˇz znamen´a, ˇze existuje inferenˇcn´ı syst´em tak, ˇze Σ A ⇒ B pr´avˇe, kdyˇz A ⇒ B lze odvodit z formul´ı ze Σ, ps´ano Σ ⊢ A ⇒ B. Dobˇre zn´am´ym u ´ pln´ym axiomatick´ym syst´emem atributov´ych implikac´ı je Armstrong˚ uv inferenˇcn´ı syst´em [2]. Pro dan´y form´aln´ı kontext I ⊆ X × Y naz´yv´ame mnoˇzinu formul´ı Σ u ´ plnou v I, pokud ze Σ lze dok´azat A ⇒ B pr´avˇe, kdyˇz A ⇒ B je pravdiv´a pro vˇsechny objekty v I. Nav´ıc Σ se naz´yv´a neredundantn´ı, pokud ˇz´adn´a ostr´a podmnoˇzina uˇz nen´ı v I u ´ pln´a. Jedn´ım pˇr´ıkladem neredundantn´ı u ´ pln´e mnoˇziny mohou b´yt takzvan´e Guigues-Duquennovy b´aze [8], kter´e jsou nav´ıc minim´aln´ı vzhledem k poˇctu formul´ı, kter´e obsahuj´ı. Napˇr´ıklad ve form´aln´ım kontextu zn´azornˇen´em v tabulce 1. neredundantn´ı a u ´ pln´a mnoˇzina formul´ı obsahuje pouze atributov´e implikace {s´yr} ⇒ {chleba} a {pivo} ⇒ {chleba}. V pr´aci jsou rozˇs´ıˇreny pˇredchoz´ı u ´ vahy t´ım, ˇze se bere jako vstupn´ı data posloupnost form´aln´ıch kontext˚ u, kter´e vzniknou zaznamen´av´an´ım atribut˚ u objekt˚ u v po sobˇe jdouc´ıch ˇcasov´ych okamˇzic´ıch, kter´ym budeme ˇr´ıkat ˇcasy. Jako pˇr´ıklad vezmˇeme z´aznamy poˇcas´ı ve mˇestech Praha a Ostrava viz. tabulku 2., kde ˇcasy mohou b´yt napˇr´ıklad dny. Zde n´as pak zaj´ımaj´ı z´avislosti mezi atributy 6
m´ısto . . . , Praha Ostrava
d´eˇst’ ×
m´ısto Praha Ostrava
d´eˇst’ × ×
m´ısto Praha Ostrava
t=1 slunce
zima
teplo × , ×
zima × ×
teplo
zima × ×
teplo
× t=2 slunce
t=3 d´eˇst’ slunce ×
,
, ...
Tabulka 2. Z´aznamy poˇcas´ı ve mˇestech v po sobˇe jdouc´ıch dnech relativnˇe v ˇcase, tedy napˇr´ıklad jestliˇze dnes prˇs´ı, pak z´ıtra bude zima“, kde ” pojmy dnes a z´ıtra odkazuj´ı na ˇcasy relativnˇe k souˇcasn´emu ˇcasu. M˚ uˇzeme tedy uvaˇzovat pravidla ve tvaru jm }, {y1i1 , . . . , ynin } ⇒ {z1j1 , . . . , zm
(1)
kde y1 , . . . , yn , z1 , . . . , zm jsou atributy z Y , kter´e maj´ı stejn´y u ´ˇcel jako u klasick´ych atributov´ych implikac´ı a i1 , . . . , in , j1 , . . . , jm jsou cel´a ˇc´ısla vyjadˇruj´ıc´ı ˇcas relativnˇe k souˇcasn´emu okamˇziku. Tedy 0 m˚ uˇzeme ch´apat jako souˇcasn´y okamˇzik (dnes), −1 jako pˇredch˚ udce 0 (vˇcera), 1 jako n´asledn´ıka 0 (z´ıtra), atd. Pro danou posloupnost form´aln´ıch kontext˚ u je pak zaj´ımav´e zkoumat, kdy jsou pravidla jako (1) splnˇena ve vˇsech ˇcasech nebo v dan´em rozsahu ˇcas˚ u. Pokud by se takov´a pravidla urˇcila z dat, pak by se dala pouˇz´ıt k pˇredpovˇedi bl´ızk´e budoucnosti, tedy k pˇredpovˇed’i atribut˚ u v ˇcasech za posledn´ım zaznamenan´ym form´aln´ım kontextem. Jako pˇr´ıklad vezmeme pravidlo {prˇs´ı−1 } ⇒ {zima0 }, kter´e je pravdiv´e pro vˇsechny objekty v ˇcasech t = 1, 2, 3 a pravidlo {slunce0 } ⇒ {teplo1 }, kter´e nen´ı pravdiv´e v ˇcase 1. V t´eto pr´aci jsou formalizov´ana pravidla ve tvaru (1) a s´emantick´emu vypl´yv´an´ı je pˇriˇrazen v´yznam tak, jak byl pr´avˇe pops´an, a pak se pr´ace soustˇred´ı na axiomatizaci. Tak jako pro klasick´e atributov´e implikace existuje i pro tato pravidla syst´em odvozovac´ıch pravidel v Armstrongovˇe stylu, kter´y je u ´ pln´y vzhledem k uveden´emu s´emantick´emu vypl´yv´an´ı.
2.
Souvisej´ıc´ı pˇ r´ıstupy
Na vstupn´ı data, kter´a uvaˇzujeme, se m˚ uˇzeme tak´e d´ıvat jako na triadick´y form´aln´ı kontext [10], kde podm´ınky odpov´ıdaj´ı ˇcasov´ym okamˇzik˚ um. V triadick´e 7
FCA uˇz byly pˇr´ıstupy, kter´e se zab´yvaly atributov´ymi implikacemi [6], nicm´enˇe jsou koncepˇcnˇe a technicky jin´e neˇz ty, kter´e jsou pops´any v t´eto pr´aci. Triadick´y form´aln´ı kontext je struktura T = hX, Y, Z, Ii, kde I ⊆ X × Y × Z je relace mezi objekty X, atributy Y a podm´ınkami Z. Triadick´y kontext m˚ uˇze b´yt ch´ap´an jako mnoˇzina tabulek, kter´e jsou stejn´e jako u FCA, kde kaˇzd´a z nich ud´av´a jak´e maj´ı objekty atributy pˇri dan´e podmn´ınce ze Z. Atributov´a implikace uvaˇzovan´a v [6] je pak v´yraz ve tvaru A ⇒C B, jehoˇz v´yznam je pokud ” m´a objekt pˇri vˇsech podmn´ınk´ach z C vˇsechny atributy z A, pak m´a pˇri vˇsech podmn´ınk´ach z C i vˇsechny atributy z B“. Pokud bychom brali podm´ınky jako ˇcasy, pak by tyto z´avisloti byly omezeny pouze na konkr´etn´ı ˇcasy. Nav´ıc nedok´aˇz´ı vyj´adˇrit, ˇze atributy objektu pˇri jedn´e podm´ınce implikuj´ı atributy objekty pˇri druh´e podm´ınce. V kapitole 5. je pak podrobnˇe rozebr´ano, jak by vypadala fomalizace formul´ı ve tvaru (1) v triadick´em form´aln´ım kontextu. V kontextu asociaˇcn´ıch pravidel [1] byly podobn´e z´avislosti jiˇz studov´any jako mezitransakˇcn´ı asociaˇcn´ı pravidla [12, 14, 11, 5, 9]. Asociaˇcn´ı pravidla formule ve tvaru A ⇒ B a jsou interpretov´ana v tabulk´ach, kde ˇr´adk˚ um se ˇr´ık´a transakce, sloupc˚ um poloˇzky a kˇr´ıˇzek/pr´azn´e m´ısto v tabulce znaˇc´ı, jestli v transakci je/nen´ı pˇr´ıtomna dan´a poloˇzka. Tabulky lze ch´apat jako form´aln´ı kontexty. Asociaˇcn´ı pravidla maj´ı v tabulce skoro stejn´y v´yznam jako atributov´e implikace ve form´aln´ım kontextu, ale obsahuj´ı nav´ıc ˇc´ısla support a confidence, kde support vyjadˇruje kolik procent celkov´eho poˇctu transakc´ı m´a vˇsechny poloˇzky z A a confidence vyjadˇruje kolik procent transakc´ı, kter´e maj´ı vˇsechny poloˇzky z A maj´ı i vˇsechny poloˇzky z B. Pokud u asociaˇcn´ıho pravidla je ˇc´ıslo confidence rovno 100, pak ho m˚ uˇzeme ch´apat jako atributovou implikaci. U mezitransakˇcn´ıch pravidel jsou transakce tabulek, ve kter´ych se intepretuj´ı, oznaˇceny ˇ ısla m˚ cel´ymi ˇc´ısly [14] nebo celoˇc´ıseln´ym vektorem [12, 11, 5]. C´ uˇzeme ch´apat jako ˇcas nebo vzd´alenost v prostoru. Pokud budeme br´at transakce jako z´aznamy stavu syst´emu, pak dan´a tabulka je z´aznamem v´yvoje syst´emu v ˇcase (prostoru) nebo tak´e napˇr´ıklad v ˇcase i prostoru, pokud jsou transakce oznaˇceny vektory. Ale to je jen nepodstatn´y detail t´ykaj´ıc´ı se interpretace. Mezitransakˇcn´ı asociaˇcn´ı pravidla, jak uˇz n´azev napov´ıd´a, obsahuj´ı v pˇredpokladu a d˚ usledku poloˇzky oznaˇcen´e nez´aporn´ym cel´ym ˇc´ıslem nebo nez´aporn´ym celoˇc´ıseln´ym vektorem, kter´y se relativnˇe odkazuje na jinou transakci. Kaˇzd´e pravidlo je normovan´e, tedy mus´ı obsahovat nˇejakou poloˇzku s ˇc´ıslem 0 nebo s nulov´ym vektorem. Nav´ıc u kaˇzd´eho pravidla lze naj´ıt nejvˇetˇs´ı ˇc´ıslo nebo nejvˇetˇs´ı ˇc´ısla u kaˇzd´e sloˇzky vektoru, kter´e ud´avaj´ı posuvn´e okno. Pro dan´e pravidlo lze pak tabulku rozloˇzit na mnoˇzinu ˇ ıslo support pak ud´av´a podtabulek, kde kaˇzd´a se vleze do posuvn´eho okna. C´ kolik procent podtabulek obsahuje pˇredpoklad pravidla vzhledem k celkov´emu poˇctu podtabulek a ˇc´ıslo confidence ud´av´a kolik procent podtabulek, kter´e obsahuj´ı pˇredpoklad obsahuj´ı i d˚ usledek. Pˇr´ıstupy se zab´yvaj´ı hlavnˇe algoritmy na urˇcen´ı tˇechto z´avislost´ı z dat. Prakticky byla mezitransakˇcn´ı asociaˇcn´ı pravidla aplikov´ana na pˇredpov´ıd´an´ı kurz˚ u cen na burze [12], pˇredpov´ıd´an´ı poˇcas´ı v Hong Kongu [5] a zjiˇstˇen´ı ˇcasov´ych z´avislost´ı mezi slanost´ı a teplotou moˇre pobl´ıˇz Tai8
wanu [9]. Tato pravidla by mohla b´yt v podobn´em vztahu k n´ami uvaˇzovan´ym pravidl˚ um, jako klasick´a asociaˇcn´ı pravidla ke klasick´ym atributov´ym implikac´ım.
3.
Formule a s´ emantick´ e vypl´ yv´ an´ı
Kapitola se vˇenuje formalizaci formul´ı, jejich v´yznamu a s´emantick´emu vypl´yv´an´ı. Pˇredpokl´adejme, ˇze mnoˇzina atribut˚ u Y je nepr´azdn´a a koneˇcn´a a cel´a ˇc´ısla budou znaˇcit ˇcasov´e okamˇziky (ˇcasy). D˚ uvod pouˇzit´ı cel´ych ˇc´ısel jako ˇcasy je, ˇze vstupn´ı data jsou ve formˇe form´aln´ıch kontext˚ u zaznamenan´ych v diskr´etn´ıch okamˇzic´ıch a je jich pouze koneˇcnˇe mnoho, a proto je toto oznaˇcen´ı postaˇcuj´ıc´ı. Pak definujeme mnoˇzinu TY = {y i | y ∈ Y a i ∈ Z},
(2)
kde kaˇzd´y prvek y i ∈ TY je atribut y v ˇcase i (na TY se m˚ uˇzeme d´ıvat jako na kart´ezsk´y souˇcin Y × Z). Pak pravidla ve tvaru (1) formalizujeme n´asledovnˇe: ˇ Definice 3.1. Casov´ a implikace je formule ve tvaru A ⇒ B, kde A, B jsou koneˇcn´e podmnoˇziny TY . ˇ Casy atribut˚ u v pˇredpokladu a d˚ usledku ˇcasov´ych implikac´ı maj´ı vyjadˇrovat ˇcas relativn´ı k ˇcasu aktu´aln´ımu. Zam´yˇslen´y v´yznam ˇcasov´e implikace A ⇒ B je tedy: Pro vˇsechny ˇcasy t, pokud m´a objekt vˇsechny atributy z A, kde t bereme jako aktu´aln´ı ˇcas, pak objekt m´a i vˇsechny atributy z B, kde t bereme jako aktu´aln´ı ˇcas. Jelikoˇz chceme, aby formule platila pro vˇsechny konkr´etn´ı ˇcasy, je potˇreba relativn´ı ˇcasy pˇredpokladu i d˚ usledku formule posunout do konkr´etn´ıch ˇcas˚ u. Proto zav´ad´ıme n´asleduj´ıc´ı pojem: Definice 3.2. Posunut´ım mnoˇziny M ⊆ TY o ˇcas j, ps´ano M + j, budeme rozumˇet pˇriˇcten´ı j k ˇcasu kaˇzd´eho atributu v M, tedy M + j = {y i+j | y i ∈ M}. Pro sloˇzitˇejˇs´ı v´yrazy budeme uvaˇzovat, ˇze M +j+i bude zkratka za (M +j)+i, aby byl z´apis jednoduˇsˇs´ı. D´ale jeˇstˇe budeme v´yrazem M − j oznaˇcovat mnoˇzinu M + (−j). Nyn´ı uvedeme nˇekter´e vlastnosti posunut´ı. Vˇ eta 3.1. (monotonie) Pro kaˇzd´e A, B ⊆ TY a ˇcas i plat´ı, ˇze pokud A ⊆ B, pak A + i ⊆ B + i. D˚ ukaz. Pˇredpokl´adejme A ⊆ B a vezmeme libovoln´y y a+i ∈ A+i. Jelikoˇz y a ∈ A, pak z pˇredpokladu plyne, ˇze y a ∈ B, a tedy y a+i ∈ B + i. 9
Vˇ eta 3.2. (distributivita) Mˇejme syst´em mnoˇzin Nj ⊆ TY (j ∈ J) a ˇcas i. Pak plat´ı n´asleduj´ıc´ı: T T j∈J Nj + i = j∈J (Nj + i). D˚ ukaz. T
j∈J
Nj + i = {y a+i | y a ∈
T
j∈J
Nj } =
T
j∈J {y
b+i
| y b ∈ Nj } =
T
j∈J (Nj
+ i)
Vˇ eta 3.3. (asociativita) Pro kaˇzdou M ⊆ TY a ˇcasy i, j plat´ı (M + i) + j = M + (i + j). D˚ ukaz. (M + i) + j = {y a+j | y a ∈ (M + i)} = {y (b+i)+j | y b ∈ M} = {y b+(i+j) | y b ∈ M} = M + (i + j)
Nyn´ı definujeme v´yznam ˇcasov´e implikace. ˇ Definice 3.3. Casov´ a implikace A ⇒ B je pravdiv´a v M ⊆ TY , pokud pro kaˇzd´y ˇcas i plat´ı, ˇze jestliˇze A + i ⊆ M, pak B + i ⊆ M
(3)
a tento fakt znaˇc´ıme M A ⇒ B. ´ mka. (a) Vˇsimnˇeme si, ˇze na z´akladˇe monotonie posunut´ı (vˇeta 3.1.) Pozna m˚ uˇzeme ekvivalentnˇe vyj´adˇrit (3) jako jestliˇze A ⊆ M − i, pak B ⊆ M − i. Tedy m´ısto posouv´an´ı pˇredpokladu a z´avˇeru ˇcasov´e implikace m˚ uˇzeme posouvat M. (b) A ⇒ B nen´ı pravdiv´a v M, ps´ano M 2 A ⇒ B, pr´avˇe, kdyˇz existuje i tak, ˇ i tedy slouˇz´ı jako protipˇr´ıklad. ˇze A + i ⊆ M, ale B + i * M. Cas (c) Pokud by se v mnoˇzin´ach A, B a M vyskytovaly pouze atributy v ˇcase 0, pak by M A ⇒ B byla klasick´a pravdivost atributov´e implikace, tedy pokud A ⊆ M, pak B ⊆ M. Vˇsimnˇeme si, ˇze ˇcasov´e implikace A ⇒ B, pro kter´e plat´ı B ⊆ A, jsou pravdiv´e ve vˇsech podmnoˇzin´ach TY . 10
Vˇ eta 3.4. Pro kaˇzdou mnoˇzinu M ⊆ TY a ˇcasovou implikaci A ⇒ B takovou, ˇze B ⊆ A, plat´ı, ˇze M A ⇒ B. D˚ ukaz. Vezmˇeme libovolnou mnoˇzinu M ⊆ TY a ˇcasovou implikaci A ⇒ B takovou, ˇze B ⊆ A. Abychom uk´azali, ˇze plat´ı M A ⇒ B staˇc´ı uk´azat, ˇze pro kaˇzd´y ˇcas i, pro kter´y je A + i ⊆ M plat´ı, ˇze i B + i ⊆ M. Vezmeme tedy libovoln´y ˇcas i a pˇredpokl´adejme, ˇze A + i ⊆ M. Z pˇredpokladu v´ıme, ˇze B ⊆ A, a tedy z monotonie posunu (vˇeta 3.1.) dostaneme B + i ⊆ A + i. To ale znamen´a, ˇze i B + i ⊆ M. D´ale tak´e existuje mnoˇzina, ve kter´e jsou pravdiv´e vˇsechny ˇcasov´e implikace. Dalˇs´ı vˇeta ˇr´ık´a, ˇze touto mnoˇzinou je TY . Vˇ eta 3.5. Pro kaˇzdou ˇcasovou implikaci A ⇒ B plat´ı, ˇze TY A ⇒ B. D˚ ukaz. Vezmˇeme libovolnou ˇcasovou implikaci A ⇒ B a uk´aˇzeme, ˇze TY A ⇒ B, tedy pro kaˇzd´y ˇcas i, pro kter´y je A + i ⊆ TY mus´ı platit b´yt i B + i ⊆ TY . Vezmeme tedy libovoln´y ˇcas i a budeme pˇredpokl´adat, ˇze A + i ⊆ TY . Jelikoˇz ale B ⊆ TY , pak nutnˇe plat´ı i B + i ⊆ TY + i = TY d´ıky monotonii posunu (vˇeta 3.1.) a definici TY , coˇz je ale to, co jsme chtˇeli dok´azat. Mnoˇzinu M, ve kter´e vyhodnocujeme A ⇒ B, m˚ uˇzeme br´at jako reprezentaci atribut˚ u jednoho objektu, kter´y se mˇen´ı v ˇcase. A tedy k ospravedlnˇen´ı zam´yˇslen´eho v´yznamu m˚ uˇzeme vz´ıt libovolnou posloupnost form´aln´ıch kontext˚ u i Ii ⊆ X × Y (i ∈ Z) a poloˇz´ıme Mx = {y | hx, yi ∈ Ii }. Pak Mx A ⇒ B m´a pˇresnˇe zam´yˇslen´y v´yznam, tedy pro vˇsechny ˇcasy t, pokud objekt m´a vˇsechny ” atributy z A (v ˇcase t), pak m´a i vˇsechny atributy z B (v ˇcase t)“. Pak pravdivost A ⇒ B v posloupnosti kontext˚ u Ii (i ∈ Z) m˚ uˇze b´yt ch´ap´ana tak, ˇze pro kaˇzd´y objekt x ∈ X plat´ı Mx A ⇒ B. Napˇr´ıklad pokud budeme br´at posloupnost 1 2 kontext˚ u z tabulky 2., pak MPraha = {. . . , d´eˇst’ , teplo1 , d´eˇst’ , zima2 , zima3 , . . . }. Budeme uvaˇzovat n´asleduj´ıc´ı pojem modelu: Definice 3.4. Mˇejme mnoˇzinu ˇcasov´ych implikac´ı Σ, kterou naz´yv´ame teorie. Pak model teorie Σ je mnoˇzina M ⊆ TY , ve kter´e jsou pravdiv´e vˇsechny implikace z teorie Σ. Mnoˇzinu vˇsech model˚ u budeme oznaˇcovat Mod(Σ), tedy Mod(Σ) = {M ⊆ TY | pro kaˇzdou A ⇒ B ∈ Σ plat´ı M A ⇒ B}. Obecnˇe mnoˇzina vˇsech model˚ u dan´e teorie je nekoneˇcn´a a m˚ uˇzou existovat i teorie, kter´e nemaj´ı ˇz´adn´y koneˇcn´y model na rozd´ıl od model˚ u mnoˇzin atributov´ych implikac´ı nad koneˇcnou Y , kde modely jsou vˇzdy koneˇcn´e. Pro pˇr´ıklad m˚ uˇzeme vz´ıt teorii {∅ ⇒ {y 0 }}. Pro mnoˇzinu vˇsech model˚ u d´ale plat´ı, ˇze je uzavˇren´a na libovoln´e pr˚ uniky a posunut´ı. 11
Definice 3.5. O mnoˇzinˇe S ⊆ 2TY ˇrekneme, ˇze je uzavˇren´a na posuny, pokud pro kaˇzdou M ∈ S a kaˇzd´y ˇcas i je i M + i ∈ S. Vˇ eta 3.6. Pro kaˇzdou teorii Σ plat´ı, ˇze Mod(Σ) je uzavˇren´a na libovoln´e pr˚ uniky a posuny. D˚ ukaz. UzavˇrenostTna pr˚ uniky : Vezmˇeme teorii Σ, mnoˇziny Nj ∈ Mod(Σ) (j ∈ J), a uk´aˇzeme, ˇze j∈J Nj ∈ Mod(Σ).TVezmeme tedy libovolnou A ⇒ B T ∈ Σ, ˇcas i, budeme pˇredpokl´adat, ˇze A + i ⊆ j∈J N , a uk´ a ˇ z eme, ˇ z e i B + i ⊆ j∈J Nj . T j Jelikoˇz z pˇredpokladu m´ame, ˇze A + i ⊆ j∈J Nj , pak nutnˇe mus´ı b´yt A + i ⊆ Nj pro kaˇzd´e j ∈ J. Pak ale z pˇredpokladu, ˇze kaˇzd´a Nj ∈ Mod(Σ) T m´ame, ˇze i B + i ⊆ N pro kaˇ z d´ e j ∈ J. To ale znamen´ a , ˇ z e B + i ⊆ j j∈J Nj , a tedy T j∈J Nj ∈ Mod(Σ). Uzavˇrenost na posuny : Vezmˇeme libovolnou mnoˇzinu M ⊆ TY , teorii Σ, ˇcas i a pˇredpokl´adejme, ˇze M ∈ Mod(Σ). Staˇc´ı uk´azat, ˇze pro kaˇzdou A ⇒ B ∈ Σ plat´ı M + i A ⇒ B. Vezmeme tedy libovolnou A ⇒ B ∈ Σ, libovoln´y ˇcas j a pˇredpokl´adejme, ˇze A + j ⊆ M + i, coˇz z monotonie posunu znamen´a, ˇze (A + j) − i ⊆ (M + i) − i, a pak z asociativity posunu dostaneme A + (j − i) ⊆ M + (i − i) = M. Jelikoˇz j − i je tak´e ˇcas, pak z pˇredpokladu M ∈ Mod(Σ) dostaneme, ˇze B + (j − i) ⊆ M, a tedy zase z asociativity a monotonie posunu dostaneme B + j ⊆ M + i. To ale uˇz znamen´a, ˇze M + i ∈ Mod(Σ), protoˇze jsme brali A ⇒ B ∈ Σ libovolnˇe. Jelikoˇz mnoˇzina vˇsech model˚ u je uzavˇren´a na libovoln´e pr˚ uniky, pak to znamen´a, ˇze tvoˇr´ı uz´avˇerov´y syst´em. K nˇemu pak m˚ uˇzeme uvaˇzovat indukovan´y uz´avˇerov´y oper´ator: Definice 3.6. S´emantick´y uz´avˇer mnoˇziny M podle teorie Σ je zobrazen´ı [· · ·]Σ : 2TY → 2TY d´ano pˇredpisem T [M]Σ = {N ∈ Mod(Σ) | M ⊆ N}. Vˇ eta 3.7. S´emantick´y uz´avˇer je uz´avˇerov´y oper´ator. D˚ ukaz. Tvrzen´ı plyne pˇr´ımo ze vztahu uz´avˇerov´ych syst´em˚ u a uz´avˇerov´ych oper´ator˚ u. Pˇresto d˚ ukaz rozebereme podrobnˇeji. 1. (extenzivita) M ⊆ [M]Σ Kaˇzd´a mnoˇzina v pr˚ uniku obsahuje M, pak tedy i jejich pr˚ unik ji obsahuje. 2. (monotonie) Pokud A ⊆ B, pak [A]Σ ⊆ [B]Σ . Pˇredpokl´adejme, ˇze A ⊆ B. Z vˇety 3.6. v´ıme, ˇze [B]Σ je model a nav´ıc z extenzivity a pˇredpokladu dostaneme A ⊆ B ⊆ [B]Σ . To znamen´a, ˇze [B]Σ je jedna z mnoˇzin z pr˚ uniku v [A]Σ , a tedy [A]Σ ⊆ [B]Σ .
12
3. (idempotence) [[M]Σ ]Σ = [M]Σ Staˇc´ı uk´azat pouze ”⊆”, protoˇze druh´a inkluze plyne z extenzivity. Ale to je hned vidˇet, protoˇze [M]Σ ⊆ [M]Σ a [M]Σ je model (vˇeta 3.6.).
S´emantick´y uz´avˇer [M]Σ je tedy nejmenˇs´ı moˇzn´y model teorie Σ, kter´y obsahuje mnoˇzinu M. Jak uˇz bylo uvedeno, modely mohou b´yt i nekoneˇcn´e, a tedy i mnoˇzina [M]Σ m˚ uˇze b´yt obecnˇe nekoneˇcn´a. Nav´ıc plat´ı, ˇze s´emantick´y uz´avˇer M m˚ uˇze b´yt vyj´adˇren jako sjednocen´ı uz´avˇer˚ u koneˇcn´ych podmnoˇzin M, coˇz znamen´a, ˇze mnoˇzina Mod(Σ) je algebraick´ym uz´avˇerov´ym syst´emem. Vˇ eta 3.8. Pro kaˇzdou teorii Σ plat´ı S [M]Σ = {[N]Σ | N je koneˇcn´a podmnoˇzina M}. D˚ ukaz. Vezmˇeme mnoˇzinu M = {N | N je koneˇ S cn´a podmnoˇzina M}. ”⊆”: Z definice staˇc´ı uk´azat, ˇze mnoˇzina N ∈M [N]Σ obsahuje mnoˇzinu M a je model Σ. Jelikoˇz M obsahuje vˇsechny koneˇcn´e podmnoˇziny M, pak jejich sjednocen´ım mus´ı b´yt mnoˇzina M. D´ale z extenzivity S s´emantick´ehoS uz´avˇeru v´ıme, ˇze pro kaˇzdou N ∈ M plat´ı N ⊆ [N]Σ , a tedy plat´ı i M = M ⊆ SN ∈M [N]Σ . Nyn´ı vezmˇeme libovolnou A ⇒ B ∈ Σ a pˇredpokl´adejme, ˇze A + i ⊆ N ∈M [N]Σ . Pak ale jelikoˇz A + i je koneˇcn´a, mus´ı pro kaˇzd´y y j ∈ A + Si existovat nˇejak´a Nyj ∈ M tak, ˇze y j ∈ [Nyj ]Σ . To ale znamen´a, ˇze NA+i = yj ∈A+i Nyj je taky koneˇcn´a podmnoˇzina M, tedy NA+i ∈ M. Nav´ıc z monotonie s´emantick´eho uz´avˇeru j ]Σ ⊆ [NA+i ]Σ . Pak ale A + i ⊆ [NA+i ]Σ , coˇ pro kaˇzd´y y j ∈ A + i plat´ı [NyS z znamen´a, ˇze B + i ⊆ [NA+i ]Σ ⊆ N ∈M [N]Σ . ”⊇”: Z extenzivity s´emantick´eho uz´avˇeru pro S kaˇzdou N ⊆ M plat´ı [N]Σ ⊆ [M]Σ . Tedy i pro kaˇzdou N ∈ M, a pak plat´ı i N ∈M [N]Σ ⊆ [M]Σ . Je zaj´ımav´e, ˇze ke kaˇzd´emu algebraick´emu uz´avˇerov´emu syst´emu lze najit teorii tak, ˇze tento syst´em je pr´avˇe mnoˇzina vˇsech model˚ u. Vˇ eta 3.9. Necht’ S ⊆ 2TY je algebraick´y uz´avˇerov´y syst´em, kter´y je uzavˇren´y na libovoln´e posuny. Pak existuje teorie Σ tak, ˇze S = Mod(Σ). D˚ ukaz. Vezmˇeme algebraick´y uz´avˇerov´y syst´em S ⊆ 2TY , kter´y je uzavˇren´y na libovoln´e posuny. S tedy tvoˇr´ı uz´avˇerov´y syst´em a to znamen´a, ˇze k nˇemu existuje indukovan´y uz´avˇerov´y oper´ator CS definovan´y n´asledovnˇe: T CS (M) = {N ∈ S | M ⊆ N}. Nyn´ı uvaˇzujme teorii Σ = {A ⇒ B | A ⊆ TY , B ⊆ CS (A) a A, B jsou koneˇcn´e} 13
a uk´aˇzeme, ˇze S = Mod(Σ). ”⊆”: Vezmeme libovolnou M ∈ S, A ⇒ B ∈ Σ, ˇcas i a pˇredpokl´adejme, ˇze A + i ⊆ M. Nyn´ı uk´aˇzeme, ˇze B + i ⊆ M. Z pˇredpokladu A + i ⊆ M a monotonie posunu a oper´atoru CS postupnˇe dostaneme, ˇze A ⊆ M −i a CS (A) ⊆ CS (M −i). Jelikoˇz M ∈ S, pak z pˇredpokladu uzavˇrenosti S na posuny plat´ı i M − i ∈ S, a tedy CS (M − i) = M − i. To znamen´a, ˇze B ⊆ CS (A) ⊆ M − i, a tedy B + i ⊆ M. ”⊇”: Staˇc´ı vz´ıt libovolnou M ∈ Mod(Σ) a uk´azat, ˇze CS (M) = M. Jedna inkluze plyne z extenzivity CS a my uk´aˇzeme tu druhou. Vezmeme ˇcasov´e implikace Aj ⇒ Bj ∈ Σ (j ∈ J) tak, ˇze Aj ⊆ M. Jelikoˇz S jeSalgebraick´y uz´avˇerov´y syst´em a Aj jsou vˇsechny koneˇcn´e podmnoˇziny M, pak j∈J CS (Aj ) = CS (M). D´ asov´e implikace Aj ⇒ Bi (i ∈ I) tak, ˇze Sale z definice pro kaˇzdou Aj jsou v Σ ˇcS S B = C (A ). To ale znamen´ a , ˇ z e B = C ze i S j j i∈I j∈J j∈J S (Aj ). Pak z toho, ˇ S M je model pro i = 0 dostaneme j∈J Bj = CS (M) ⊆ M. Nyn´ı se budeme soustˇredit na s´emantick´e vypl´yv´an´ı a jeho vlastnosti. ˇ Definice 3.7. Casov´ a implikace A ⇒ B s´emanticky plyne z teorie Σ, ps´ano Σ A ⇒ B, pokud pro kaˇzdou M ∈ Mod(Σ) plat´ı, ˇze M A ⇒ B. N´asleduj´ıc´ı vˇeta ospravedlˇ nuje fakt, ˇze ˇcasy atribut˚ u u ˇcasov´e implikace jsou ˇ ık´a, ˇze z A ⇒ B s´emanticky plynou vˇsechny ˇcasov´e implikace, kter´e relativn´ı. R´ vzniknou z A ⇒ B posunut´ım pˇredpokladu i d˚ usledku o stejn´y ˇcas. Vˇ eta 3.10. Pro kaˇzdou ˇcasovou implikaci A ⇒ B a ˇcas i plat´ı, ˇze {A ⇒ B} A + i ⇒ B + i. D˚ ukaz. Abychom uk´azali {A ⇒ B} A + i ⇒ B + i, je potˇreba uk´azat, ˇze pro vˇsechny M ∈ Mod({A ⇒ B}) plat´ı M A + i ⇒ B + i. Vezmeme tedy libovoln´y model M ∈ Mod({A ⇒ B}) tak, ˇze (A+i)+j ⊆ M, tedy A+i ⊆ M −j. Z vˇety 3.6. m´ame M − j ∈ Mod({A ⇒ B}), tedy B + i ⊆ M − j, a d´ale (B + i) + j ⊆ M. Ale to uˇz znamen´a, ˇze {A ⇒ B} A + i ⇒ B + i. Podobnˇe jako u atributov´ych implikac´ı m˚ uˇzeme ovˇeˇrit, jestli implikace A ⇒ B s´emanticky plyne z teorie Σ pomoc´ı nejmenˇs´ıho modelu generovan´eho mnoˇzinou A. Ale nejdˇr´ıve si uk´aˇzeme jednu pomocnou vˇetu, kter´a ukazuje, ˇze i s´emantick´y uz´avˇer m´a zaj´ımavou vlastnost vzhledem k posunut´ı. Vˇ eta 3.11. Bud’ Σ teorie, a pak pro mnoˇzinu A ⊆ TY plat´ı [A + i]Σ = [A]Σ + i.
14
D˚ ukaz. ”⊆”: Jelikoˇz Mod(Σ) je uzavˇren´a na posuny, pak [A]Σ + i ∈ Mod(Σ), a jelikoˇz A ⊆ [A]Σ , pak plat´ı A + i ⊆ [A]Σ + i. To ale z definice s´emantick´eho uz´avˇeru znamen´a, ˇze [A + i]Σ ⊆ [A]Σ + i. ”⊇”: Jelikoˇz Mod(Σ) je uzavˇren´a na posuny, pak [A + i]Σ − i ∈ Mod(Σ), a jelikoˇz A + i ⊆ [A + i]Σ , pak plat´ı A ⊆ [A + i]Σ − i. To ale z definice s´emantick´eho uz´avˇeru znamen´a, ˇze [A]Σ ⊆ [A + i]Σ − i, tedy [A]Σ + i ⊆ [A + i]Σ . Vˇ eta 3.12. Pro kaˇzdou teorii Σ a ˇcasovou implikaci A ⇒ B je n´asleduj´ıc´ı ekvivalentn´ı: 1. Σ A ⇒ B 2. [A]Σ A ⇒ B 3. B ⊆ [A]Σ D˚ ukaz. ”1 ⇒ 2”: Pokud plat´ı Σ A ⇒ B, pak pro kaˇzd´y model M plat´ı M A ⇒ B. To ale znamen´a, ˇze plat´ı i pro [A]Σ ∈ Σ. ”2 ⇒ 3”: Pokud plat´ı [A]Σ A ⇒ B, pak pro ˇcas 0 z toho, ˇze A = A+0 ⊆ [A]Σ dostaneme B ⊆ [A]Σ . ”3 ⇒ 1”: Pˇredpokl´adejme, ˇze plat´ı B ⊆ [A]Σ a vezmeme M ∈ Mod(Σ) a ˇcas i, tak ˇze A + i ⊆ M. Pak A ⊆ M − i, a tedy [A]Σ ⊆ [M − i]Σ . Pak spolu s pˇredpokladem a vˇetou 3.11. dostaneme B ⊆ [M]Σ − i, a tedy B + i ⊆ [M]Σ . To ale uˇz znamen´a, ˇze Σ A ⇒ B.
4.
Axiomatizace
V t´eto kapitole je pops´an odvozovac´ı syst´em ˇcasov´ych implikac´ı a pojem syntaktick´eho vypl´yv´an´ı. Syntaktick´e vypl´yv´an´ı je zaloˇzeno na rozˇs´ıˇren´ı Armstrongova axiomatick´eho syst´emu [2] o fakt, ˇze ˇcasy ve formul´ıch jsou relativn´ı. Pokud A, B jsou koneˇcn´e, odvod’ A ∪ B ⇒ A. Z A ⇒ B a B ∪ C ⇒ D odvod’ A ∪ C ⇒ D. Pro ˇcas i z A ⇒ B odvod’ A + i ⇒ B + i.
(Ax) (Cut) (Shf)
Pravidlo (Shf), kter´e je oproti Armstrongovu syst´emu nav´ıc, budeme naz´yvat pravidlo ˇcasov´eho posunu. D´ale standardnˇe definujeme pojem d˚ ukazu a syntaktick´eho vypl´yv´an´ı neboli dokazatelnosti. Definice 4.1. D˚ ukaz z teorie Σ je koneˇcn´a posloupnost ˇcasov´ych implikac´ı ϕ1 , . . . , ϕn , kde kaˇzd´a ϕi 1. je z teorie Σ, nebo 15
2. vznikla odvozen´ım pomoc´ı (Ax), (Cut) nebo (Shf) z ϕ1 , . . . , ϕi−1 . ˇ Casov´ a implikace A ⇒ B je dokazateln´a z teorie Σ, ps´ano Σ ⊢ A ⇒ B, pokud existuje d˚ ukaz ze Σ tak, ˇze ϕn = A ⇒ B. N´asleduj´ıc´ı tvrzen´ı je zn´am´ym v´ysledkem pro dokazatelnost Armstronga syst´emu [13], a jelikoˇz odvozovac´ı syst´em, kter´y uvaˇzujeme, je rozˇs´ıˇren´ım Armstronga syst´emu, pak pro nˇej toto tvrzen´ı plat´ı tak´e. Vˇ eta 4.1. {A ⇒ B, A ⇒ C} ⊢ A ⇒ B ∪ C, {B ⇒ C} ⊢ A ∪ B ⇒ A ∪ C, {A ⇒ B ∪ C} ⊢ A ⇒ B, {A ⇒ B, B ⇒ C} ⊢ A ⇒ C.
(Add) (Aug) (Pro) (Tra)
D˚ ukaz. (Add): 1 2 3 4 5
A⇒B B∪C ⇒B∪C A∪C ⇒B∪C A⇒C A⇒B∪C
pˇredpoklad (Ax) (Cut) z 1 a pˇredpoklad (Cut) z 3 a
1 2 3
B⇒C A∪C ⇒A∪C A∪B ⇒A∪C
pˇredpoklad z teorie (Ax) (Cut) z 1 a 2
1 2 3
A⇒B∪C B∪C ⇒B A⇒B
pˇredpoklad z teorie (Ax) (Cut) z 1 a 2
z teorie 2 z teorie 4
(Aug):
(Pro):
(Tra): 1 2 3
A⇒B B⇒C A⇒C
pˇredpoklad z teorie pˇredpoklad z teorie (Cut) z 1 a 2
16
´ mka. Pro zjednoduˇsen´ı m˚ Pozna uˇzeme pˇredchoz´ı pouˇz´ıvat jako odvozovac´ı pravidla, protoˇze v d˚ ukazu je m˚ uˇzeme nahradit jejich d˚ ukazy, kter´e pouˇz´ıvaj´ı pouze odvozovac´ı pravidla (Ax) a (Cut). Abychom uk´azali, ˇze vˇse, co je dokazateln´e z dan´e teorie, z n´ı i s´emanticky plyne, je potˇreba uk´azat, ˇze vˇsechna pravidla jsou korektn´ı, tedy pro kaˇzd´e pravidlo ”Z A1 ⇒ B1 , . . . , An ⇒ Bn odvod’ C ⇒ D”mus´ı platit {A1 ⇒ B1 , . . . , An ⇒ Bn } C ⇒ D. Vˇ eta 4.2. Pro koneˇcn´e mnoˇziny A, B ⊆ TY plat´ı ∅ A ∪ B ⇒ A. D˚ ukaz. Vezmˇeme libovolnou M ∈ Mod(∅), a jelikoˇz A ⊆ A∪B, pak d´ıky vˇetˇe 3.4. plat´ı M A ∪ B ⇒ A. Vˇ eta 4.3. Pro koneˇcn´e mnoˇziny A, B, C, D ⊆ TY plat´ı {A ⇒ B, B ∪ C ⇒ D} A ∪ C ⇒ D. D˚ ukaz. Vezmˇeme libovolnou M ∈ Mod({A ⇒ B, B ∪ C ⇒ D}), a pˇredpokl´adejme, ˇze (A ∪ C) + i ⊆ M. (A ∪ C) + i = {y j+i | y j ∈ A nebo y j ∈ C} = {y j+i | y j+i ∈ A + i nebo y j+i ∈ C + i} = (A + i) ∪ (C + i). Jelikoˇz M je model, pak urˇcitˇe plat´ı i B + i ⊆ M, a tedy (C + i) ∪ (B + i) ⊆ M. Ale pak plat´ı i D + i ⊆ M. Vˇ eta 4.4. (korektnost) Pro koneˇcnou teorii Σ a ˇcasovou implikaci A ⇒ B plat´ı, ˇze pokud Σ ⊢ A ⇒ B, pak Σ A ⇒ B. D˚ ukaz. D˚ ukaz provedeme indukc´ı pˇres d´elku d˚ ukazu A ⇒ B. Pˇredpokl´adejme, ˇze pro kaˇzd´e j ≤ i−1 plat´ı Σ ϕj . D´ale kaˇzd´a formule ϕi z d˚ ukazu je bud’ ze Σ, tedy trivi´alnˇe plat´ı Σ ϕi , a nebo ϕi vznikla z pˇredchoz´ıch formul´ı pomoc´ı pravidla (Ax), (Cut) nebo (Shf). Jelikoˇz vˇsechna pravidla jsou korektn´ı (vˇety 4.2., 4.3. a 3.10.), pak z pˇredpokladu plat´ı i Σ ϕi . Pro dok´az´an´ı u ´ plnosti budeme potˇrebovat jeˇstˇe uk´azat, ˇze pokud Σ A ⇒ B, pak Σ ⊢ A ⇒ B. V n´asleduj´ıc´ı vˇetˇe je dok´azan´e obmˇenˇen´e tvrzen´ı. Vˇ eta 4.5. Mˇejme koneˇcnou teorii Σ a ˇcasovou implikaci A ⇒ B. Pokud Σ 0 A ⇒ B, pak existuje M ∈ Mod(Σ) tak, ˇze M 2 A ⇒ B. D˚ ukaz. Vezmˇeme koneˇcnou Σ a pˇredpokl´adejme, ˇze Σ 0 A ⇒ B. Pak pro kaˇzd´e nez´aporn´e cel´e ˇc´ıslo n poloˇz´ıme A0Σ = A, S An+1 = AnΣ ∪ {F + i | E ⇒ F ∈ Σ a E + i ⊆ AnΣ }, Σ S n AωΣ = ∞ n=0 AΣ . 17
Nyn´ı staˇc´ı uk´azat, ˇze AωΣ je hledan´y model M. Vezmˇeme E ⇒ F ∈ Σ a ˇcas i tak, ˇze E + i ⊆ AωΣ . Jelikoˇz E + i je koneˇcn´a mnoˇzina, pak mus´ı existovat n tak, ˇze E + i ⊆ AnΣ , a tedy z definice plat´ı F + i ⊆ An+1 ⊆ AωΣ , coˇz znamen´a, ˇze Σ ω ω AΣ ∈ Mod(Σ). D´ale dok´aˇzeme, ˇze pokud B ⊆ AΣ , pak Σ ⊢ A ⇒ B. K tomu n´am staˇc´ı uk´azat, ˇze pro kaˇzd´e n a kaˇzdou koneˇcnou D ⊆ AnΣ plat´ı Σ ⊢ A ⇒ D, protoˇze pak staˇc´ı jen vz´ıt D = B. Pˇredpokl´adejme, ˇze tvrzen´ı plat´ı pro n a pro vˇsechny koneˇcn´e podmnoˇziny AnΣ . Nyn´ı vezmˇeme n + 1, koneˇcnou D ⊆ An+1 Σ a koneˇcnou D ′ = {hE ⇒ F, ii | E ⇒ F ∈ Σ a E + i ⊆ AnΣ } S takovou, ˇze D ⊆ {F + i | hE ⇒ F, ii ∈ D ′ } ∪ AnΣ . Z indukˇcn´ıho pˇredpokladu pro kaˇzdou hE ⇒ F, ii ∈ D ′ m´ame Σ ⊢ A ⇒ E + i, protoˇze E + i ⊆ AnΣ . Pak d˚ ukaz A ⇒ E + i prodlouˇz´ıme o 1 2 3 4
A⇒E +i E⇒F E+i⇒F +i A⇒F +i
posledn´ı formule z d˚ ukazu pˇredpoklad z teorie (Shf) z 2 (Tra) z 1 a 3
a m´ame d˚ ukaz A ⇒ F + i, tedy Σ ⊢ A ⇒ F + i. A jelikoˇz D a D ′ jsou koneˇcn´e, pak Σ ⊢ A ⇒ D dostaneme pouˇzit´ım indukˇcn´ıho pˇredpokladu a koneˇcnˇe mnoha aplikacemi (Add). Pak z naˇseho poˇc´ateˇcn´ıho pˇredpokladu Σ 0 A ⇒ B dostaneme B * AωΣ . D´ale pro i = 0 m´ame A + i = A ⊆ AωΣ , ale tedy B + i = B * AωΣ , coˇz znamen´a, ˇze Σ 2 A ⇒ B. Korektnost a pˇredchoz´ı vˇeta uˇz dohromady d´avaj´ı vˇetu o u ´ plnosti. Vˇ eta 4.6. (´ uplnost) Pro kaˇzdou koneˇcnou teorii Σ a ˇcasovou implikaci A ⇒ B plat´ı, ˇze Σ A ⇒ B pr´avˇe, kdyˇz Σ ⊢ A ⇒ B. D˚ ukaz. Vˇeta je d˚ usledkem korektnosti a pˇredchoz´ı vˇety. Na mnoˇzinu AωΣ , kter´a byla uvedena v d˚ ukazu vˇety 4.5., se m˚ uˇzeme d´ıvat jako na konstruktivn´ı popis [A]Σ , protoˇze tyto mnoˇziny jsou stejn´e. D˚ usledek 4.1. Pro kaˇzdou koneˇcnou A ⊆ TY a koneˇcnou teorii Σ plat´ı, ˇze [A]Σ = AωΣ . D˚ ukaz. ”⊆”: Z d˚ ukazu vˇety 4.5. je vidˇet, ˇze AωΣ je model obsahuj´ıc´ı A, tedy [A]Σ ⊆ AωΣ . ”⊇”: Z d˚ ukazu vˇety 4.5. je tak´e vidˇet, ˇze pro kaˇzdou koneˇcnou D ⊆ AωΣ plat´ı Σ ⊢ A ⇒ D. Tedy z u ´ plnosti m´ame Σ A ⇒ D a z vˇety 3.12., pak dostaneme, ˇze D ⊆ [A]Σ . Jelikoˇz to plat´ı pro kaˇzdou koneˇcnou podmnoˇzinu, pak to plat´ı i pro jejich sjednocen´ı, a tedy AωΣ ⊆ [A]Σ . 18
´ mka. Nakonec poznamenejme, ˇze pojmy s´emantick´eho a syntakPozna tick´eho vypl´yv´an´ı jsou vskutku jin´e neˇz u klasick´e FCA. M˚ uˇzeme uvaˇzovat mnoˇzinu atribut˚ u TY , a pak kaˇzd´a ˇcasov´a implikace bude tak´e atributovou implikac´ı. Pak k s´emantick´emu vypl´yv´an´ı z definice 3.7. m˚ uˇzeme uvaˇzovat klasick´e s´emantick´e vypl´yv´an´ı, kde nebudeme br´at v u ´ vahu speci´aln´ı roli ˇcas˚ u. To sam´e aplikujeme na dokazatelnost, tedy klasick´y pojem dostaneme vynech´an´ım pravidla (Shf). Pak napˇr´ıklad z Σ = {{a−1 } ⇒ {b1 }, {b3 } ⇒ {c1 }} lze dok´azat {a1 } ⇒ {b3 } pomoc´ı (Shf), a pak {a1 } ⇒ {c1 } pomoc´ı (Tra). Na druh´e stranˇe ale ze Σ nelze dok´azat {a1 } ⇒ {c1 } bez (Shf).
5.
Vztah k ostatn´ım formalism˚ um
Tato kapitola se zab´yv´a vztahem formul´ı, pravdivosti a s´emantick´eho vypl´yv´an´ı z kapitoly 3. k v´yrokov´e tempor´aln´ı logice [3, 4] a k triadick´e FCA [10]. U atributov´ych implikac´ı jsme ˇr´ıkali, ˇze m˚ uˇzou b´yt ch´ap´any jako formule ˇ v´yrokov´e logiky. Casov´e implikace pak m˚ uˇzou b´yt ch´ap´any jako formule tempor´aln´ı v´yrokov´e logiky a podmnoˇziny TY jako Kripkeho modely v´yrokov´eho jazyka, kter´y obsahuje atributy z Y jako v´yrokov´e symboly. Konkr´etnˇe pro M ⊆ TY m˚ uˇzeme uvaˇzovat KM = hW, e, ri, kde mnoˇzina svˇet˚ u W = Z, relace dosaˇzitelnosti r ⊆ W × W je definov´ana jako hw, w + 1i ∈ r pro kaˇzd´y w ∈ Z a e(w, y) = 1, pokud y w ∈ M jinak e(w, y) = 0. Pro vyj´adˇren´ı vztah˚ u mezi ˇcasy z ˇcasov´ych implikac´ı zavedeme modality G, jehoˇz v´yznam je v n´asleduj´ıc´ım ” svˇetˇe“, a H, jehoˇz v´yznam je v pˇredchoz´ım svˇetˇe“. Pak reprezentujeme ˇcasovou ” implikaci tedy formuli ve tvaru (1) jako (△i1 y1 N · · · N △in yn ) ⇒ (△j1 z1 N · · · N △jm zm ),
(4)
kde N je konjunkce a if i = 0, y, i i−1 △ y = G△ y, if i > 0, H△i+1 y, if i < 0.
Pak s touto notac´ı je (1) pravdiv´a v M pr´avˇe, kdyˇz pˇr´ısluˇsn´a formule ve tvaru (4) je pravdiv´a v KM ve vˇsech svˇetech w ∈ W , kde hodnota Gϕ v K a w je dan´a hodnotou ϕ v K a w ′ tak, ˇze hw, w ′i ∈ r (a analogicky pro H). Tedy aˇz na r˚ uznou formalizaci interpretace ˇcasov´ych implikac´ı m˚ uˇze b´yt ch´ap´ana jako interpretace urˇcit´ych mod´aln´ıch formul´ı v Kripkeho modelech. Nakonec se pod´ıv´ame na ˇcasov´e implikace a pravdivost v kontextu triadick´e FCA. Jak bylo ps´ano v u ´ vodu, tak posloupnost form´aln´ıch kontext˚ u Ii ⊆ X × Y (i ∈ Z) by mohla b´yt ch´ap´ana jako triadick´y form´aln´ı kontext. Konkr´etnˇe pro triadick´y form´aln´ı koncept T = hX, Y, Z, Ii m´ame hx, y, ji ∈ I pr´avˇe, kdyˇz ˇ hx, yi ∈ Ij . Casov´ a implikace pak m˚ uˇze b´yt interpretov´ana v tomto triadick´em kontextu: 19
Definice 5.1. Formule A ⇒ B je pravdiv´a v triadick´em kontextu T = hX, Y, Z, Ii, ps´ano T A ⇒ B, pokud pro kaˇzd´y x ∈ X a Mx = {y i | hx, y, ii ∈ I} plat´ı Mx A ⇒ B. Klasick´y v´ysledek u atributov´ych implikac´ı ˇr´ık´a, ˇze atributov´a implikace je pravdiv´a ve form´aln´ım kontextu pr´avˇe, kdyˇz je pravdiv´a ve vˇsech jeho intentech. Nav´ıc A ⇒ B je pravdiv´a v triadick´em kontextu pokud mnoˇzina B je podmnoˇzinou intentu generovan´eho mnoˇzinou A. V naˇsem pˇr´ıpadˇe m˚ uˇzeme prok´azat podobnou charakterizaci. Pro dan´y T = hX, Y, Z, Ii definujeme oper´atory ↑ : 2TX → 2TY a ↓ : 2TY → 2TX n´asledovnˇe: Pro kaˇzdou A ⊆ TX (definovan´a jako (2), kde X nahrad´ıme za Y ) a B ⊆ TX m´ame A↑ = {y j ∈ TY | hx, y, i + ji ∈ I for all xi ∈ A}, B ↓ = {xi ∈ TX | hx, y, i + ji ∈ I for all y j ∈ B}. Dvojce oper´ator˚ u ↑ a ↓ tvoˇr´ı antitonn´ı Galoisovu konexi, tedy pro mnoˇziny A ⊆ TX a B ⊆ TY plat´ı A ⊆ B ↓ pr´avˇe, kdyˇz B ⊆ A↑ . Pak sloˇzen´y oper´ator ↓↑ : 2TY → 2TY je uz´avˇerov´y oper´ator. Vˇ eta 5.1. Pro kaˇzd´y triadick´y kontext T = hX, Y, Z, Ii a formuli A ⇒ B je n´asleduj´ıc´ı ekvivalentn´ı: 1. T A ⇒ B, 2. A↓ ⊆ B ↓ , 3. B ⊆ A↓↑ . D˚ ukaz. T A ⇒ B plat´ı pr´avˇe, kdyˇz pro kaˇzd´y x ∈ X plat´ı Mx A ⇒ B. D´ale A + i ⊆ Mx plat´ı pr´avˇe, kdyˇz pro kaˇzd´y y j ∈ A plat´ı hx, y, j + ii ∈ I, coˇz je pr´avˇe, kdyˇz xi ∈ A↓ . Stejn´e pozorov´an´ı m˚ uˇzeme udˇelat pro B, a tedy pro kaˇzd´y x ∈ X plat´ı Mx A ⇒ B pr´avˇe, kdyˇz A↓ ⊆ B ↓ . 1 je tedy ekvivalentn´ı s 2. Ekvivalence 2 a 3 plyne hned z vlastnosti Galoisovy konexe h↓ , ↑ i. Na z´akladˇe vˇety 5.1. m˚ uˇzeme uk´azat analogii k v´ysledku o pravdivosti atributov´ych implikac´ı v kontextech jako implikace splnˇen´e intenty vˇsech koncept˚ u. ↑ ↓ K tomu ale jeˇstˇe budeme potˇrebovat n´asleduj´ıc´ı tvrzen´ı o vztahu oper´ator˚ u , k posunut´ı. Lemma 5.1. Pro mnoˇzinu B ⊆ TY a ˇcas k plat´ı (B + k)↓ = B ↓ − k. D´ ale plat´ı i du´aln´ı tvrzen´ı pro ↑ .
20
D˚ ukaz. Vezmˇeme libovolnou B ⊆ TY a ˇcas k. Pak (B + k)↓ = {xi ∈ TX | hx, y, i + ji ∈ I pro kaˇzd´y y j ∈ B + k}. Pokud poloˇzime j ′ = j − k, pak dostaneme ′
(B + k)↓ = {xi ∈ TX | hx, y, i + j ′ + ki ∈ I pro kaˇzd´y y j ∈ B} Nav´ıc pokud poloˇz´ıme i′ = i + k, dostaneme ′
′
(B + k)↓ = {xi −k ∈ TX | hx, y, i′ + j ′ i ∈ I pro kaˇzd´y y j ∈ B} ′
′
= {xi ∈ TX | hx, y, i′ + j ′ i ∈ I pro kaˇzd´y y j ∈ B} − k = B ↓ − k. Pro
↑
by se tvrzen´ı uk´azalo stejnˇe.
Vˇ eta 5.2. Pro kaˇzd´y triadick´y kontext T = hX, Y, Z, Ii a formuli A ⇒ B plat´ı, ˇze T A ⇒ B pr´avˇe, kdyˇz M ↓↑ A ⇒ B pro kaˇzdou M ⊆ TY . D˚ ukaz. ⇐ plyne z vˇety 5.1. pro M = A a i = 0. K prok´az´an´ı druh´e strany pˇredpokl´adejme, ˇze T A ⇒ B a A + i ⊆ M ↓↑ . Pak z vlastnosti Galoisovy konexe a pˇredchoz´ı lemmy m´ame M ↓ ⊆ (A + i)↓ = A↓ − i. Pak z pˇredpokladu, vˇety 5.1. a monotonie posunu dostaneme M ↓ ⊆ A↓ − i ⊆ B ↓ − i = (B + i)↓ , a tedy B + i ⊆ M ↓↑ .
21
Z´ avˇ er V t´eto pr´aci jsme pˇredstavili ˇcasov´e implikace a jejich v´yznam na z´akladˇe vyhodnocov´an´ı v modelech pomoc´ı posunu do konkr´etn´ıch ˇcas˚ u. Formule jsou pravdiv´e, pokud jsou zachov´any ve vˇsech ˇcasech. Definovali jsme s´emantick´e vypl´yv´an´ı, uk´azali uz´avˇerov´e vlastnosti syst´em˚ u model˚ u a poskytli charakterizaci na z´akladˇe nejmenˇs´ıch model˚ u. Nav´ıc jsme uk´azali axiomatizaci, kter´a rozˇsiˇruje klasickou axiomatizaci o dodateˇcn´e pravidlo ˇcasov´eho posunu. P˚ uvodnˇe ˇcasov´e implikace obsahovaly pouze koneˇcn´e mnoˇziny atribut˚ u v ˇcasech, kter´e jsou z´aporn´e nebo se rovnaj´ı nule a pravdivost ˇcasov´e implikace A ⇒ B v M jsme definovali v urˇcit´em rozsahu ˇcas˚ u. Podm´ınka (3.3.) nemusela platit pro vˇsechny ˇcasy, ale pouze pro ˇcasy i takov´e, ˇze mnoˇziny A + i a B + i obsahuj´ı pouze atributy v ˇcasech, kter´e jsou v r´amci dan´eho rozsahu. D´ıky zaveden´ı ˇcasov´eho rozsahu u pravdivosti se m˚ uˇzeme u s´emantick´eho vypl´yv´an´ı omezit pouze na modely, kter´e obsahuj´ı pouze atributy v ˇcasech, kter´e jsou v dan´em rozsahu. S´emantick´y uz´avˇer je tedy vˇzdy koneˇcn´y. D´ale jsme pracovali pouze s implikacemi, jejichˇz d˚ usledek obsahuje aspoˇ n jeden atribut v ˇcase, kter´y je vˇetˇs´ı nebo roven neˇz vˇsechny ˇcasy atribut˚ u z pˇredpokladu a z´aroveˇ n pˇredpoklad obsahuje aspoˇ n jeden atribut v ˇcase, kter´y je menˇs´ı nebo roven neˇz vˇsechny ˇcasy atribut˚ u z d˚ usledku. S´emantick´e vypl´yv´an´ı ˇcasov´e implikace A ⇒ B z mnoˇziny tˇechto implikac´ı pak lze charakterizovat pomoc´ı nejmenˇs´ıho modelu generovan´eho mnoˇzinou A. Nav´ıc pokud bereme pouze tyto ˇcasov´e implikace, pak oproti obecn´ym ˇcasov´ym implikac´ım je odvozovac´ı pravidlo (Cut) korektn´ı. Navrhli jsme algoritmus pro v´ypoˇcet s´emantick´eho uz´avˇeru, kter´y je rozˇs´ıˇren´ım zn´am´eho algoritmu LinClosure [13]. Tato formalizace zabrala hodnˇe ˇcasu, ale naneˇstˇest´ı se uk´azalo, ˇze axiomatizace, kter´a byla stejn´a jako ta, kter´a je uvedena v kapitole 4., nen´ı u ´ pln´a vzhledem k s´emantick´emu vypl´yv´an´ı. Po r˚ uzn´ych u ´ prav´ach jsme se nakonec rozhodli zruˇsit omezen´ı na ˇcasy a tato verze formalizace je pops´ana v t´eto pr´aci. Jak jsme uk´azali, tak nyn´ı uˇz plat´ı vˇeta o u ´ plnosti, ale bohuˇzel s´emantick´y uz´avˇer m˚ uˇze b´yt nekoneˇcn´a mnoˇzina. Mnoˇzina AωΣ , kter´a je uvedena v d˚ ukazu vˇety 4.5. slouˇz´ı jako form´aln´ı z´aklad pro algoritmus na zjiˇstˇen´ı, jestli ˇcasov´a implikace s´emanticky plyne z dan´e teorie (vˇeta 3.12.). V pr´aci algoritmus uveden nen´ı, protoˇze zat´ım nen´ı jasn´e, jak by mˇel v´ypoˇcet vypadat, aby se nemusel poˇc´ıtat cel´y uz´avˇer. Dalˇs´ım pˇredmˇetem b´ad´an´ı pak bude tak´e popis neredundantn´ı mnoˇziny ˇcasov´ych implikac´ı, kter´a je u ´ pln´a v datech.
22
Conclusions In this work we introduced time implications and their semantics based on evaluating in models using the shift to concrete time points. The formulas are true if they are preserved in all time points. We defined semantic entailment, showed closure properties of systems of models, and provided a characterization based on least models. Furthermore we showed axiomatization which extends classic axiomatization by an additional rule of the time shift. Originally time implications contained only finite sets of attributes in time points which are negative or equal to zero and we defined the truth of time implication A ⇒ B in M in particular time scope. Condition (3.3.) didn’t have to be satisfied for all times but only for times i such that sets A + i and B + i contains only attributes in times which are within the current scope. Thanks to the introduction of time scope in truth and also in semantic entailment, we can limit models only to models which contain only attributes in times which are within the current scope. Semantic closure is then always finite. Next we worked only with implications such that their consequent contains at least one attribute in time which is greater or equal than all times of attributes in antecedent and their antecedent contains at least one attribute in time which is less or equal than all times of attribute in consequent. Semantic entailment of time implication A ⇒ B from sets of implications of this type can be then characterized by the least model generated by the set A. Moreover when we consider only this time implications, the inference rule (Cut) is sound in contrast with general time implications. We designed an algorithm for computing the semantic closure which is an extension of known algorithm LinClosure [13]. This formalization took lot of time but unfortunately we discovered that the axiomatization which was similar to the axiomatization in section 4. is not complete with respect to semantic entailment. After some modifications we decided to remove the limitation on time point and this version of formalization is described in this work. As we showed, the completness theorem now holds but unfortunately the semantic closure can be an infinite set. The set AωΣ which is stated in theorem 4.5. is used as a formal basis for algorithm on indicating whether a particular theory semantically entails a time implication (theorem 3.12.). The algorithm is not included in this work because it is not clear yet how should the computation look like to not compute the whole semantic closure. Future research will focus on description of non-redundant set of time implications which is complete in data.
23
Reference [1] Agrawal R., Imielinski T., Swami A.: Mining association rules between sets of items in large databases. In Proc. of the ACM SIGMOD Intl. Conf. on Management of Data (1993), pp. 207–216. [2] Armstrong W.W.: Dependency structures of data base relationships. In: Rosenfeld, J.L., Freeman, H. (eds.) Information Processing 74: Proceedings of IFIP Congress., North Holland, Amsterdam (1974), pp. 580–583. [3] Gabbay D.M.: Model theory for tense logics. Annals of Mathematical Logic 8 (1-2), 185–236 (1975) [4] Gabbay D.M.: Tense systems with discrete moments of time, part I. Journal of Philisophiical Logic 1 (1), 35–44 (1972) [5] Feng L., Dillon T., Liu J. Inter-transactional association rules for multidimensional contexts for prediction and their application to studying meteorological data. Data and Knowledge Engineering, 37 (2001), pp. 85–115. [6] Ganter B., Obiedkov S.: Implications in triadic formal contexts. In: Wolff K.E., Pfeiffer H.D., Delugach H.S. (eds.) Conceptual Structures at Work, Lecture Notes in Computer Science, vol. 3127, pp. 186–195. Springer Berlin Heidelberg (2004) [7] Ganter B., Wille R.: Formal Concept Analysis: Mathematical Foundations. Springer, Berlin, 1999. [8] Guigues J.L., Duquenne V.: Familles minimales d’implications informatives resultant d’un tableau de donn´ees binaires. Math. Sci. Humaines 95 (1986), pp. 5–18. [9] Huang Y.P., Kao L.J., Sandnes F.E.: Efficient mining of salinity and temperature association rules from ARGO data. Expert Systems with Applications 35 (2008), pp. 59–68. [10] Lehmann F., Wille R.: A triadic approach to formal concept analysis. In: Ellis G., Levinson R., Rich W., Sowa J.F. (eds.) Conceptual Structures: Applications, Implementation and Theory, Lecture Notes in Computer Science, vol. 954, pp. 32–43. Springer Berlin Heidelberg (1995) [11] Liu J., Feng L., Han J.: Beyond Intra-Transaction Association Analysis: Mining Multi-Dimensional Inter-Transaction Association Rules. ACM Transactions on Information Systems, 18 (2000), pp. 423–454.
24
[12] Lu H., Han J., Feng L.: (1998) Stock Movement Prediction And NDimensional Inter-Transaction Association Rules. In Proc. of the ACM SIGMOD Workshop on Research Issues on Data Mining and Knowledge Discovery (1998), pp. 12:1–12:7. [13] Maier D.: Theory of Relational Databases. Computer Science Press, Rockville, MD, USA, 1983. [14] Tung K.H., Lu H., Han J., Feng L.: Breaking the barrier of transactions: Mining inter-transaction association rules. In Proc. ACM SIGKDD Intl. Conf. Knowledge Discovery and Data Mining (1999), pp. 297–301.
25
