CAISL: Simpli ica ion Logic o Condi ional
A ibu e Implica ions
Es ella Rod ´ıguez-Lo enzo1, Pablo Co de o1, Manuel Enciso1, Rokia Missaoui2,
´
Angel Mo a1
1Uni e sidad de M´alaga, Andaluc´ıa Tech, Spain,
e-mail: {es ella odlo ,amo a}@c ima.uma.es, {pco de o,enciso}@uma.es
2Uni e si ´e du Qu´ebec en Ou aouais, Canada,
e-mail: { okia.missaoui}@uqo.ca
Abs ac . In his wo k, we p esen a sound and comple e axioma ic
sys em o condi ional a ibu e implica ions (CAI s) in T iadic Concep
Analysis (TCA). Ou app oach is s ongly based on he Simpli ica ion
pa adigm, allowing a mo e sui able app oach o au oma ed easoning
han hose based on A ms ong’s Axioms. We also p esen an au oma ed
me hod o p o e he de i abili y o a CAI om a se o CAI s.
1 In oduc ion
Implica ions in FCA ep esen associa ions be ween wo a ibu e se s, deno ed
by X→Y, and cap u e an impo an knowledge hidden in he inpu da a. They
also allow an al e na e ep esen a ion o he concep la ice and open he doo
o hei au oma ed managemen h ough logic. Such a managemen is used, o
ins ance, o cha ac e ize ep esen a ions o he whole knowledge by means o he
no ion o implica ional sys ems. The e exis di e en axioma ic sys ems in FCA,
he i s one is called A ms ong’s Axioms [1], bu la e , o he equi alen logics
eme ged [4, 5, 9].
The i s s udy on iadic implica ions has been in es iga ed by Biede mann [2]
and hen an ex ended wo k has been poposed by Gan e and Obiedko [6]. In
addi ion o a o mal de ini ion o implica ions and hei language, we belie e ha
he in oduc ion o a sound and comple e in e ence sys em is needed o eason
abou such implica ions and de e mine whe he a gi en implica ion can be de i ed
om an implica ion basis. Soundness ensu es ha implica ions de i ed by using
he axioma ic sys em a e alid in he o mal con ex and comple eness gua an ees
ha all alid implica ions can be de i ed om he implica ional sys em.
As a as we know, he e does no exis an axioma ic sys em in T iadic Concep
Analysis. The main goal o his pape is hen o de ine a new axioma ic sys em
based on Simpli ica ion Logic [4] as an al e na e iew o he in e ence sys em
ecen ly de eloped by he au ho s [12]. This new way also allows an e icien
au oma ed easoning, commonly called he implica ion p oblem, o de e mine i
a condi ional a ibu e implica ion (CAI ) can be de i ed om a se o CAI s.
Gi en a se o dependencies Σand a u he dependency σ, he implica ion
p oblem means ha one would like o check whe he σholds in all da ase s
sa is ying Σ. This p oblem occu s in esea ch a eas such as da abase heo y and
knowledge easoning, and i s solu ion allows he sea ch o associa ions in an in e -
ac i e and explo a o y way a he han an exhaus i e manne . Using A ms ong’s
axioms, many polynomial ime algo i hms o implica ion p oblem decision ha e
been de ined and he closu e o an a ibu e se has been exploi ed o sol e i .
The emainde o his pape is o ganized as ollows. In Sec ion 2 we p o ide
a backg ound on TCA. Sec ion 3 b ie ly p esen s a logic o condi ional a ibu e
implica ions called CAIL [12] while Sec ion 4 desc ibes a new axioma ic sys em
called CAISL ha is mo e sui able o sol ing he implica ion p oblem in he
iadic amewo k. In Sec ion 5 we es ablish equi alences de i ed om CAISL
be ween se s o CAI sand show how we can syn ac ically ans o m and simpli y
a se o CAI s while p ese ing hei seman ics in he CAISL con ex . To check
whe he a CAI holds o a gi en se o CAI s, we p opose and illus a e a new p o-
cedu e in Sec ion 6. Finally, Sec ion 7 summa izes ou con ibu ion and p esen s
u he wo k.
2 T iadic concep analysis
As a na u al ex ension o Fo mal Concep Analysis (FCA), heo e ical ounda ions
o T iadic Concep Analysis ha e been in es iga ed by Lehmann and Wille [8] who
we e inspi ed by he philosophical amewo k o Cha les S. Pei ce [11] o h ee
uni e sal ca ego ies. The inpu is a o mal iadic con ex desc ibing objec s in
e ms o a ibu es ha hold unde gi en condi ions and he ou pu is a con-
cep ila ice ha allows he gene a ion o iadic associa ion ules, including
implica ions [2, 6, 7, 10].
De ini ion 1. A iadic con ex K=hG, M, B, Iiconsis s o h ee se s: a se o
objec s (G), a se o a ibu es (M) and a se o condi ions (B) oge he wi h a
e na y ela ion I⊆G×M×B. A iple (g, m, b)in Imeans ha objec gpossesses
a ibu e munde condi ion b.
Figu e 1 shows a iadic con ex K:= hG, M, B, Ii, whe e G={1,2,3,4,5}
is a se o cus ome s, M={P,N,R,K,S}a se o supplie s and B={a,b,d,e}
ep esen s a se o p oduc s. The e na y ela ion gi es in o ma ion abou he cus-
ome s and he supplie s om whom hey buy p oduc s. Fo ins ance, Cus ome
1 buys om Supplie P p oduc s a,b and e.
KP N R K S
1 abe abe ad ab a
2 ae bde abe ae e
3 abe e ab ab a
4 abe be ab ab e
5 ae ae abe abd a
Fig. 1. A iadic con ex
The de i a ion ope a o s in iadic concep analysis we e in oduced in [8]. I
X1,X2and X3a e subse s o G,Mand B espec i ely, hen one can ge :
X0
1={(aj, ak)∈M×B|(ai, aj, ak)∈I o all ai∈X1}.
(X2, X3)0={ai∈G|(ai, aj, ak)∈I o all (aj, ak)∈X2×X3}.
In a simila way, X0
2, (X1, X3)0,X0
3and (X1, X2)0can be de ined. As shown
in [13], he abo e amily o ope a o s, by se ing a subse o objec s, a ibu es
o condi ions ( espec i ely) yields Galois connec ions. In his pape , we use he
amily o Galois connec ions associa ed wi h condi ion subse s. Tha is, gi en
C ⊆ Bwe conside he Galois connec ion be ween he la ices (2M,⊆) and (2G,⊆)
as he pai o mappings:
(−,C)0: 2G−→ 2M(−,C)0: 2M−→ 2G
X17−→ (X1,C)0X27−→ (X2,C)0
Thus, o each X1⊆Gand X2⊆M, one has X2⊆(X1,C)0i and only i
X1⊆(X2,C)0.
In a simila way as in dyadic FCA, he composi ion o bo h de i a ion ope a-
o s leads o he no ion o iadic concep .
De ini ion 2. A iadic concep o a iadic con ex is a iple (A1, A2, A3)wi h
A1⊆G,A2⊆M,A3⊆Band A1×A2×A3⊆Isuch ha o X1⊆G, X2⊆M,
and X3⊆Bwi h X1×X2×X3⊆I, he con ainmen s A1⊆X1, A2⊆X2,and
A3⊆X3always lead o (A1, A2, A3)=(X1, X2, X3). The subse s A1,A2and A3
a e called he ex en , he in en and he modus o he iadic concep (A1, A2, A3)
espec i ely.
The e a e a ew kinds o iadic implica ions wi h di e en seman ics. Biede -
mann [3] de ines a iadic implica ion o be an exp ession o he o m: (A→B)C
whe e Aand Ba e a ibu e se s and Cis a se o condi ions. This implica ion
is in e p e ed as: I an objec has all a ibu es om Aunde all condi ions om
C, hen i also has all a ibu es om Bunde all condi ions om C. I s o mal
de ini ion is he ollowing:
De ini ion 3. Le K=hG, M, B, Iibe a iadic con ex , A, B ⊆Mand C ⊆ B.
The implica ion (X→Y)Cholds in he con ex Ki (X, C)0⊆(Y, C)0.
Gan e and Obiedko [6] conside h ee kinds o iadic implica ions. We will
desc ibe and make use o he ollowing one which is s onge han Biede mann’s
exp ession and has ano he no a ion: XC
−→ Y, whe e X, Y ⊆Mand C ⊆ B. Such
implica ion is called condi ional a ibu e implica ion (CAI ) and is ead as “X
implies Yunde all condi ions in Co any subse o i ”.
De ini ion 4 (Condi ional a ibu e implica ion). Le K=hG, M, B, Iibe
a iadic con ex , X, Y ⊆Mand C ⊆ B. The implica ion XC
−→ Yholds in he
con ex Kwhen (X, {c})0⊆(Y, {c})0 o all c∈ C.
No ice ha CAI s p ese e he dyadic implica ions ha hold o each elemen-
a y condi ion in C. The ollowing p oposi ion ela es bo h no ions o implica ions
and also shows ha Biede mann’s de ini ion is weake han he CAI de ini ion.
P oposi ion 1 ([6]). Le K=hG, M, B, Iibe a iadic con ex , X, Y ⊆Mand
C ⊆ B. Then XC
−→ Yholds in Ki (X→Y)Nalso holds in K o all N ⊆ C.
The ollowing example illus a es he abo e p oposi ion.
Example 1. Le Kbe he iadic o mal con ex gi en in Figu e 1.
i) The CAI Nae
−→ Pholds in Ksince he ollowing implica ions a e sa is ied:
(N→P)a,(N→P)e,(N→P)ae.
ii) The Biede mann’s implica ion (N→P)abe is sa is ied bu he CAI Nabe
−−→ P
does no hold because, o ins ance, (N→P)bis no sa is ied.
Ou objec i e in his pape is o p o ide in e ence mechanisms o a se o
CAI s.
To ha end, a sound and comple e axioma ic sys em is needed. As men ioned
ea lie , we ha e in oduced in [12] a no el logic o compu ing CAI s and easoning
abou hem. This logic is b ie ly p esen ed in he ollowing sec ion.
3 CAIL: Condi ional A ibu e Implica ion Logic
In his sec ion, we desc ibe CAIL, a logic o easoning abou CAI s in he ame-
wo k o TCA [12]. This logic is p esen ed in a classical s yle by conside ing h ee
pilla s: he language, he seman ics and he in e ence sys em.
Language: As i has been ou lined, we use he ollowing language: gi en an a -
ibu e se Ωand a se o condi ions Γ, he se o well- o med o mulas (he e-
ina e , o mulas o implica ions) is LΩ,Γ ={AC
−→ B|A, B ⊆Ω, C ⊆ Γ}.
In he sequel we use X, Y, Z, W o mean subse s o a ibu es (X, Y, Z, W ⊆Ω)
and C,C1,C2 o subse s o condi ions (C,C1,C2⊆Γ). Fo he sake o eadabili y
o o mulas, we omi he b acke s and commas (e.g. abc deno es he se {a, b, c})
and, as usual, he union is deno ed by se jux aposi ion (e.g. XY deno es X∪Y).
Seman ics: Based on De ini ion 4, he seman ics is in oduced by means o he
no ions o in e p e a ion and model. F om a language LΩ,Γ , an in e p e a ion is
a iadic con ex K=hG, M, B, Iisuch ha M=Ωand B=Γ. A model o a
o mula XC
−→ Y∈ LΩ,Γ is an in e p e a ion ha sa is ies XC
−→ Yin K. In his
case, we w i e K|=XC
−→ Y.
As usual, o Σ⊆ LΩ,Γ , an in e p e a ion Kis a model o Σ(b ie ly, K|=Σ)
i K|=XC
−→ Y o each XC
−→ Y∈Σ. Simila ly, Σ|=XC
−→ Ys a es ha XC
−→ Y
is a seman ic consequence o Σ, i.e. e e y model o Σis also a model o XC
−→ Y.
Syn ac ic in e ence: The syn ac ic de i a ion in CAIL is deno ed by he symbol
`Cand co e s wo axiom schemes and ou in e ence ules.
De ini ion 5. The CAIL axioma ic sys em consis s o he ollowing ules:
[Non-cons ain ] `C∅∅
−→ Ω.
[Inclusion] `CXY Γ
−→ X.
[Augmen a ion] XC
−→ Y`CXZ C
−→ Y Z.
[T ansi i i y] {XC1
−→ Y, Y C2
−→ Z} `CXC1∩C2
−−−−→ Z.
[Condi ional Decomposi ion] XC1C2
−−−→ Y`CXC1
−→ Y.
[Condi ional Composi ion] {XC1
−→ Y, Z C2
−→ W} `CXZ C1C2
−−−→ Y∩W.
The de i a ion no ion is in oduced as usual: Fo a gi en se Σ⊆ LΩ,Γ and ϕ∈
LΩ,Γ , we s a e ha ϕis de i ed (o in e ed) om Σby using he CAIL axioma ic
sys em, deno ed by Σ`Cϕ, i he e exis s a chain o o mulas ϕ1, . . . , ϕn∈ LΩ,Γ
such ha ϕn=ϕand, o all 1 ≤i≤n,ϕiis ei he an axiom, an implica ion in Σ
o is ob ained by applying he CAIL in e ence ules o o mulas in {ϕj|1≤j < i}.
Soundness and comple eness: In [12], we p o e ha e e y model o Σis a model
o XC
−→ Yi such implica ion can be de i ed syn ac ically om Σusing he
CAIL axioma ic sys em, i.e.
Σ|=XC
−→ Yi and only i Σ`CXC
−→ Y
4 CAISL: Simpli ica ion Logic o CAI s
Once he p elimina y esul s ha e been in oduced, we now p esen a new ax-
ioma ic sys em which is mo e sui able o au oma ed easoning. We will use he
same language and seman ics p o ided in he p e ious sec ion bu gi e a no el
equi alen axioma ic sys em based on simpli ica ion pa adigm [4]. Fo his ax-
ioma ic sys em, he symbol `Sdeno es he syn ac ic de i a ion.
De ini ion 6. The CAISL axioma ic sys em has wo axiom schemes:
[Non-cons ain ] `S∅∅
−→ Ω.
[Re lexi i y] `SXΓ
−→ X.
and ou in e ence ules:
[Decomposi ion] {XC1C2
−−−→ Y Z} `SXC1
−→ Y.
[Composi ion] {XC1
−→ Y, Z C2
−→ W} `SXZ C1∩C2
−−−−→ Y W.
[Condi ional Composi ion] {XC1
−→ Y, Z C2
−→ W} `SXZ C1C2
−−−→ Y∩W.
[Simpli ica ion] I X∩Y=∅,
{XC1
−→ Y, XZ C2
−→ W} `SXZ YC1∩C2
−−−−→ W Y.

The wo axiom schemes in CAISL ha e he ollowing in e p e a ions espec-
i ely: (1) all a ibu es hold o all objec s unde a oid condi ion, and (2) X
always implies i sel unde all condi ions.
The key s a emen is ha bo h axioma ic sys ems a e equi alen as he ollow-
ing heo em p o es. Howe e , as we will show below, CAISL is mo e app op ia e
o de eloping au oma ed me hods o eason abou implica ions.
Theo em 1 (Equi alence be ween CAIL and CAISL). Fo any Σ⊆ LΩ,Γ
and XC
−→ Y∈ LΩ,Γ , one has
Σ`SXC
−→ Yi and only i Σ`CXC
−→ Y
P oo . To p o e he equi alence be ween bo h logics, we will show ha he in e -
ence ules o CAISL can be de i ed om hose in CAIL and ice e sa.
i) In e ence ules de i ed om CAIL
[Re lexi i y]:
1. XΓ
−→ X. . . . . . . . . . . . . Inclusion.
[Decomposi ion]:
1. XC1C2
−−−→ Y Z . . . . . . .Hypo hesis.
2. Y Z Γ
−→ Y. . . . . . . . . . . Inclusion.
3. XC1C2
−−−→ Y..........1,2 T ans.
4. XC1
−→ Y. . . . .3 Cond. Decomp.
[Composi ion]:
1. XC1
−→ Y. . . . . . . . . . Hypo hesis.
2. ZC2
−→ W. . . . . . . . . . Hypo hesis.
3. XZ C1
−→ Y Z . . . . . . . . . . .1 Augm.
4. Y Z C2
−→ Y W . . . . . . . . . . 2 Augm.
5. XZ C1∩C2
−−−−→ Y W . . . . . 3,4 T ans.
[Simpli ica ion]:
1. XC1
−→ Y. . . . . . . . . . Hypo hesis.
2. XZ C2
−→ W. . . . . . . . Hypo hesis.
3. XZ YΓ
−→ X. . . . . . . Inclusion.
4. WΓ
−→ W Y. . . . . . . . Inclusion.
5. XZ C2
−→ W Y. . . . . 2,4 T ans.
6. XZ YC1
−→ Y......3,1 T ans.
7. XZ YC1
−→ XY Z . . . . 6 Augm.
8. XY Z C2
−→ W Y . . . . . . . 5 Augm.
9. XZ YC1∩C2
−−−−→ W Y 7,8 T ans.
10. XZ YC1∩C2
−−−−→ W Y. 9 De-
comp.
ii) In e ence ules de i ed om CAISL
[Inclusion]:
1. XY Γ
−→ XY . . . . . . . Re lexi i y.
2. XY Γ
−→ Y. . . . . . . . . . 1 Decomp.
[Augmen a ion]:
1. XC
−→ Y. . . . . . . . . . . Hypo hesis.
2. ZΓ
−→ Z. . . . . . . . . . . . .Re lexi i y.
3. XZ C
−→ Y Z .........1,2 Comp.
[T ansi i i y]:
1. XC1
−→ Y. . . . . . . . . . . Hypo hesis.
2. YC2
−→ Z. . . . . . . . . . . Hypo hesis.
3. XC1
−→ Y X. . . . . . . 1 Decomp.
4. YC2
−→ Z Y. . . . . . . . .2 Decomp.
5. XΓ
−→ X. . . . . . . . . . . . Re lexi i y.
6. XΓ
−→ ∅ . . . . . . . . . . . . . 5 Decomp.
7. XY C2
−→ Z Y......4,6 Comp.
8. Y XΓ
−→ Y X. . . .Re lexi i y.
9. XC1∩C2
−−−−→ Z Y. . . . . 3,7 Simp.
10. XC1∩C2
−−−−→ Y Z ......1,9 Comp.
11. XC1∩C2
−−−−→ Z. . . . . . . 10 Decomp.
u
Since he wo axioma ic sys ems a e equi alen , in he sequel we will omi he
subsc ip in he syn ac ic de i a ion symbol using simply `.
5 CAISL Equi alences
In his sec ion, we in oduce se e al esul s which cons i u e he basis o he
au oma ed easoning me hod ha will be in oduced in he nex sec ion. These
esul s illus a e how we can use CAISL as a amewo k o syn ac ically ans o m
and simpli y a se o CAI s while en i ely p ese ing hei seman ics. This is he
common ea u e o he amily o Simpli ica ion Logics.
The no ion o equi alence is in oduced as usual: wo se s o CAI s, Σ1and
Σ2, a e equi alen , deno ed by Σ1≡Σ2, when hei models a e he same. Equi -
alen ly, Σ1≡Σ2i Σ1`ϕ o all ϕ∈Σ2, and Σ2`ϕ o all ϕ∈Σ1.
Lemma 1. The ollowing equi alences hold:
{XC1
−→ Y, X C2
−→ W}≡{XC1∩C2
−−−−→ Y W, X C1
C2
−−−→ Y, X C2
C1
−−−→ W}(1)
{XC1
−→ Y, XV C2
−→ W}≡{XC1
−→ Y, XV C2
C1
−−−→ W, X(V Y)C1∩C2
−−−−→ W Y}(2)
P oo . Fo Equi alence (1), i s , we p o e ha XC1∩C2
−−−−→ Y W,XC1
C2
−−−→ Y, and
XC2
C1
−−−→ Wcan be in e ed om {XC1
−→ Y, X C2
−→ W}:
–By applying Composi ion o XC1
−→ Yand XC2
−→ W, we ge XC1∩C2
−−−−→ Y W.
–XC1
C2
−−−→ Yand XC2
C1
−−−→ Wa e ob ained by Decomposi ion.
On he o he hand, we p o e ha XC1
−→ Yand XC2
−→ Wcan be in e ed om
{XC1∩C2
−−−−→ Y W, X C1
C2
−−−→ Y, X C2
C1
−−−→ W}by applying Condi ional Composi ion.
Fo Equi alence (2), om {XC1
−→ Y, XV C2
−→ W}, we in e XV C2
C1
−−−→ Wby
applying Decomposi ion o VC2
−→ W. In addi ion, we in e XV YC1∩C2
−−−−→ W Y
by applying Simpli ica ion o XC1
−→ Yand XV C2
−→ W.
Finally, {XC1
−→ Y, XV C2
C1
−−−→ W, XV YC1∩C2
−−−−→ W Y} ` XV C2
−→ Wis
p o ed. By applying Re lexi i y and Decomposi ion, we ge XV C1∩C2
−−−−→ XV Y
and, by T ansi i i y wi h XV YC1∩C2
−−−−→ W Y, one has XV C1∩C2
−−−−→ W Y. Now,
by applying Composi ion o XC1
−→ Yand XV C1∩C2
−−−−→ W Y, we in e XV C1∩C2
−−−−→
WY and, by Decomposi ion, XV C1∩C2
−−−−→ W. A las , by applying Condi ional
Composi ion o XV C1∩C2
−−−−→ Wand XV C2
C1
−−−→ W, we ob ain XV C2
−→ W.u
The ollowing heo em highligh s a common cha ac e is ic o Simpli ica ion
Logics, which shows ha in e ence ules can be ead as equi alences ha allow
edundancy emo al.
Theo em 2. The ollowing equi alences hold:
Axiom Eq.: {X∅
−→ Y}≡{XC
−→ ∅} ≡ ∅
Decomposi ion Eq.: {XC
−→ Y}≡{XC
−→ Y X}
Composi ion Eq.: {XC
−→ Y, X C
−→ W}≡{XC
−→ Y W}
Condi ional Composi ion Eq.: {XC1
−→ Y, X C2
−→ Y} ≡ {XC1C2
−−−→ Y}
Simpli ica ion Eq.: I X∩Y=∅, hen
{XC1C2
−−−→ Y, XV C2
−→ W}≡{XC1C2
−−−→ Y, XV YC2
−→ W Y}
P oo . The i s equi alence is s aigh o wa d because bo h implica ions a e ax-
ioms. Fo he es o equi alences, he le o igh in e ence is di ec ly ob ained
by applying he homonymous in e ence ule. Thus, we p o e he igh o le
in e ence:
i) XC
−→ XY is in e ed by Composi ion o XC
−→ Y Xand XC
−→ Xob ained
by e lexi i y. Then, by applying Decomposi ion, one has XC
−→ Y.
ii) XC
−→ Yand XC
−→ Wa e in e ed by applying Decomposi ion o XC
−→ Y W.
iii) XC1
−→ Yand XC2
−→ Ya e in e ed om XC1C2
−−−→ Yby applying Decomposi-
ion.
i ) I is a consequence o Axiom Equi alence and Equi alence (2) in Lemma 1.
u
This sec ion has been de o ed o equi alences in CAISL o a CAI s se in o de
o emo e edundancy o , dually, o ex end he se . The e ec depends on he
di ec ion we apply he equi alence. In nex sec ion, we a e going o use o he
equi alences whe e he emp y se plays a main ole. The Deduc ion Theo em
p esen ed below gi es o he emp y se such a ole. This heo em es ablishes he
necessa y and su icien condi ion o ensu e he de i abili y o a CAI om a se
o CAI s.
6 Au oma ed easoning
This sec ion shows he me i s o CAISL o he de elopmen o au oma ed me h-
ods. Speci ically, we p esen a me hod ha checks whe he a CAI is de i ed om
a se o CAI s. The nex heo em is he co e o ou app oach in he design o he
au oma ed p o e .
Theo em 3 (Deduc ion). Fo any Σ⊆ LΩ,Γ and XC
−→ Y∈ LΩ,Γ , one has
Σ`XC
−→ Yi and only i Σ∪ {∅ C
−→ X}`∅ C
−→ Y
P oo . S aigh o wa dly, we ha e Σ`XC
−→ Yimplies Σ∪ {∅ C
−→ X} ` ∅ C
−→ Y.
Con e sely, assuming Σ∪ {∅ C
−→ X}`∅ C
−→ Y, we ha e o p o e ha K|=Σ
implies K|=XC
−→ Y o each model K.
Conside K=hG, M, B, Iias a model o Σ. In o de o p o e (X, {c})0⊆
(Y, {c})0 o all c∈Cin K, we build he con ex K1=hG1, M, B, I1iwhe e
G1= (X, {c})0and I1=I∩(G1×M×B).
Since K|=Σ, we ha e K1|=Σ∪ {∅ {c}
−−→ X}and he e o e, by hypo hesis,
K1|={∅ {c}
−−→ Y}. Tha is, (Y, {c})0⊇(∅,{c})0=G1= (X, {c})0.
I we go back o he o iginal iadic con ex K, (X, {c})0 emains unchanged
whe eas (Y, {c})0could g ow up. The e o e, in K, one has (X, {c})0⊆(Y, {c})0 o
all c∈C.u
Func ion CAISL-P o e (Σ,XC
−→ Y)
inpu : A se o implica ions Σ, and a CAI XC
−→ Y
ou pu : A boolean answe
begin
∆X:= X× C
∆Y:= (Y× C) (X× C)
epea
lag:= alse
o each UC1
−→ V∈Σwi h C1∩ C 6=∅do
∆C:= {c∈ C1∩ C | U× {c} ⊆ ∆X}
i ∆C6=∅ hen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equi alence (4)
∆X:= ∆X∪(V×∆C)
∆Y:= ∆Y (V×∆C)
Σ:= Σ {UC1
−→ V}
C1:= C1 ∆C
i C16=∅ hen Σ:= Σ∪ {UC1
−→ V}
lag:= ue
∆C:= {c∈ C1∩ C | V× {c} ⊆ ∆X}
i ∆C6=∅ hen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equi alence (5)
i ∆C=C1 hen Σ:= Σ {UC1
−→ V}
else Σ:=(Σ {UC1
−→ V})∪ {UC1
∆C
−−−−→ V}
un il (∆Y=∅)o ( lag= alse)
e u n he boolean alue (∆Y=∅)
Theo em 3 guides he design o he au oma ed p o e . To check ha he
o mula XC
−→ Yis in e ed om he se Σwe apply he amily o simpli ica ion
equi alences i e a i ely - while i is possible - o he se Σ∪ {∅ C
−→ X}looking o
∅C
−→ Y.
The ollowing p oposi ion e isi s Theo em 2 by ins an ia ing he pa icula
case o ha ing he emp y p emise.
P oposi ion 2. The ollowing equi alences hold:
{∅ C1
−→ X, U C2
−→ V}≡{∅ C1
−→ X, U XC1∩C2
−−−−→ V X, U C2
C1
−−−→ V}(3)
{∅ C1
−→ X, U C2
−→ V}≡{∅ C1∩C2
−−−−→ XV, ∅C1
C2
−−−→ X, U C2
C1
−−−→ V}, when U⊆X(4)
{∅ C1
−→ X, U C2
−→ V}≡{∅ C1
−→ X, U C2
C1
−−−→ V}, when V⊆X(5)
P oo . Equi alence (3) is a pa icula case o Equi alence (2). In pa icula , when
U⊆X, Equi alence (4) is ob ained om (3) by applying Condi ional Composi ion