Luận án Học khái niệm cho các hệ thống thông tin dựa trên logic mô tả

ng tr¼nh [14]. Điểm kh¡c ở đây là c¡c k¸t qu£
được chúng tôi ph¡t triºn tr¶n lớp c¡c logic mô t£ lớn hơn đã đề cªp trong Mục 1.2.2
cõa Chương 1.
Định nghĩa 2.6. Mët TBox T (tương ùng, ABox A) trong LΣy;Φy được gọi là b§t
 0
bi¸n đối với LΣy;Φy -mô phỏng hai chi·u n¸u với mọi di¹n dịch I và I trong LΣ;Φ tồn
 0
t¤i mët LΣy;Φy -mô phỏng hai chi·u giúa I và I sao cho I là mô h¼nh cõa T (tương
 0
ùng, A) khi và ch¿ khi I là mô h¼nh cõa T (tương ùng, A). 
 y
H» qu£ 2.1. N¸u U 2 Φ th¼ t§t c£ c¡c TBox trong LΣy;Φy đều b§t bi¸n đối với
LΣy;Φy -mô phỏng hai chi·u. 
 y 0
Chùng minh. Gi£ sû U 2 Φ , T là mët TBox trong LΣy;Φy , I và I là c¡c di¹n dịch
 0
trong ngôn ngú LΣ;Φ, Z là mët LΣy;Φy -mô phỏng hai chi·u giúa I và I . Chúng ta c¦n
chùng minh n¸u I là mô h¼nh cõa T th¼ I0 cũng là mô h¼nh cõa T và ngưñc l¤i. Gi£
sû I là mô h¼nh cõa T , ta c¦n ch¿ ra r¬ng I0 cũng là mô h¼nh cõa T . Chi·u ngược l¤i
được chùng minh tương tự.
 X²t C v D là mët ti¶n đề thuªt ngú b§t kỳ cõa TBox T và x0 2 ∆I0 . Theo điều
ki»n (2.17), tồn t¤i x 2 ∆I sao cho Z(x; x0) thỏa m¢n. V¼ I là mô h¼nh cõa T n¶n ta
có x 2 (:C t D)I . Theo kh¯ng định (2.19) cõa Bê đề 2.2 ta suy ra x0 2 (:C t D)I0 .
 0
Do vªy, I cũng là mô h¼nh cõa T . 
 48
 Mët di¹n dịch I trong LΣ;Φ được gọi là k¸t nèi đối tượng đưñc đối với LΣy;Φy n¸u
 I y I
với mọi đối tượng x 2 ∆ tồn t¤i c¡ thº a 2 ΣI , c¡c đối tượng x0; x1; : : : ; xk 2 ∆
 I
và c¡c vai trá đối tượng cơ b£n R1;R2;:::;Rk cõa LΣy;Φy với k ≥ 0 sao cho x0 = a ,
 I
xk = x và Ri (xi−1; xi) thỏa m¢n với mọi 1 ≤ i ≤ k [14].
 0
Định lý 2.2. Cho T là mët TBox trong LΣy;Φy , I và I là c¡c di¹n dịch trong LΣ;Φ
thỏa điều ki»n k¸t nèi đối tượng được đối với LΣy;Φy sao cho tồn t¤i mët LΣy;Φy -mô
phỏng hai chi·u giúa I và I0. Lúc đó I là mô h¼nh cõa T khi và ch¿ khi I0 là mô h¼nh
cõa T . 
 0
Chùng minh. Gọi T là mët TBox trong LΣy;Φy . Gi£ sû I và I là c¡c di¹n dịch k¸t nèi
 0
đối tượng được trong LΣy;Φy , Z là mët LΣy;Φy -mô phỏng hai chi·u giúa I và I . Chúng
ta c¦n chùng minh n¸u I là mô h¼nh cõa T th¼ I0 cũng là mô h¼nh cõa T và ngược
l¤i. Gi£ sû I là mô h¼nh cõa T , ta c¦n ch¿ ra I0 là mô h¼nh cõa T . Chi·u ngược l¤i
được chùng minh tương tự.
 X²t C v D là mët ti¶n đề b§t kỳ cõa TBox T . Để chùng minh I0 cũng là mô h¼nh
cõa T , chúng ta c¦n ch¿ ra r¬ng CI0 ⊆ DI0 . Nghĩa là, với mọi x0 2 CI0 th¼ x0 2 DI0 .
 0 y
V¼ I là mët di¹n dịch k¸t nèi đối tưñng được trong LΣy;Φy n¶n tồn t¤i c¡ thº a 2 ΣI ,
 0 0 0 I0
c¡c đối tưñng x0; x1; : : : ; xk 2 ∆ và c¡c vai trá đối tượng cơ b£n R1;R2;:::;Rk cõa
 0 I0 0 0 I0 0 0
LΣy;Φy với k ≥ 0 sao cho x0 = a , xk = x và Ri (xi−1; xi) thỏa m¢n với mọi 1 ≤ i ≤ k.
 0 I I0
 V¼ Z là mët LΣy;Φy -mô phỏng hai chi·u giúa I và I n¶n ta có Z(a ; a ) thỏa
 I 0
m¢n (theo điều ki»n (2.1)). Đặt x0 = a . Với méi 1 ≤ i ≤ k, ta có Z(xi−1; xi−1) và
 I0 0 0 I 0 I
Ri (xi−1; xi) thỏa m¢n n¶n tồn t¤i xi 2 ∆ sao cho Z(xi; xi) và Ri (xi−1; xi) thỏa m¢n
 0 0 I0 I
(theo kh¯ng định (2.21)). Đặt x = xk, ta có Z(x; x ) thỏa m¢n. V¼ x 2 C n¶n x 2 C
(theo kh¯ng định (2.19)). Do I là mô h¼nh cõa T n¶n x 2 DI . Tø Z(x; x0) thỏa m¢n và
 I 0 I0 0
x 2 D ta suy ra x 2 D (theo kh¯ng định (2.19)). Do vªy, I là mô h¼nh cõa T . 
 y
Định lý 2.3. Cho A là mët ABox trong LΣy;Φy . N¸u O 2 Φ hoặc A ch¿ chùa c¡c
kh¯ng định d¤ng C(a) th¼ A b§t bi¸n đối với LΣy;Φy -mô phỏng hai chi·u. 
Chùng minh. Gi£ thi¸t O 2 Φy hoặc A ch¿ chùa c¡c kh¯ng định d¤ng C(a). Gọi I
 0 0
và I là c¡c di¹n dịch trong LΣ;Φ, Z là mët LΣy;Φy -mô phỏng hai chi·u giúa I và I .
Chúng ta c¦n chùng minh n¸u I là mô h¼nh cõa A th¼ I0 cũng là mô h¼nh cõa A và
ngược l¤i. Gi£ sû I là mô h¼nh cõa A, chúng ta c¦n ch¿ ra I0 cũng là mô h¼nh cõa A.
Chi·u ngược l¤i được chùng minh tương tự.
 X²t ' là mët kh¯ng định b§t kỳ cõa A, chúng ta c¦n ch¿ ra I0 j= '.
 49
 - Trường hñp ' = (a = b), v¼ I j= ' n¶n ta có aI = bI . Theo điều ki»n (2.1) th¼
Z(aI ; aI0 ) và Z(bI ; bI0 ) thỏa m¢n. V¼ aI = bI n¶n theo (2.9) ta có aI0 = bI0 . Do vªy,
I0 j= '.
 - Trường hñp ' = (a 6= b) được chùng minh tương tự như trường hñp tr¶n.
 - Trường hñp ' = C(a), v¼ I j= ' n¶n ta có CI (aI ) thỏa m¢n. Theo điều ki»n (2.1)
th¼ Z(aI ; aI0 ) thỏa m¢n. V¼ Z(aI ; aI0 ) và CI (aI ) thỏa m¢n n¶n theo kh¯ng định (2.19)
th¼ CI0 (aI0 ) thỏa m¢n. Do vªy, I0 j= '.
 - Trường hñp ' = R(a; b), v¼ I j= ' n¶n ta có RI (aI ; bI ) thỏa m¢n. Theo điều
ki»n (2.1) th¼ Z(aI ; aI0 ) thỏa m¢n. V¼ Z(aI ; aI0 ) và RI (aI ; bI ) thỏa m¢n n¶n theo
kh¯ng định (2.20), tồn t¤i y0 2 ∆I0 sao cho Z(bI ; y0) và RI0 (aI0 ; y0) thỏa m¢n. Theo
gi£ thi¸t O 2 Φy, ta chọn C ≡ fbg. V¼ Z(bI ; y0) và CI (bI ) thỏa m¢n n¶n ta có CI0 (y0)
thỏa m¢n (theo kh¯ng định (2.19)). Điều này có nghĩa là y0 = bI0 và RI0 (aI0 ; bI0 )
thỏa m¢n. Do vªy, I0 j= '.
 - Trường hñp ' = :R(a; b) được chùng minh tương tự như trường hñp tr¶n. 
 H» qu£ sau đây xem x²t cơ sở tri thùc trong trường hñp RBox b¬ng réng. Lúc đó
cơ sở tri thùc ch¿ cán TBox và ABox và do đó t½nh b§t bi¸n cõa cơ sở tri thùc có thº
được suy ra trực ti¸p tø Định lý 2.2 và Định lý 2.3.
H» qu£ 2.2. Cho cơ sở tri thùc KB = hR; T ; Ai trong LΣy;Φy sao cho R = ; và gi£
thi¸t O 2 Φy hoặc A ch¿ chùa c¡c kh¯ng định có d¤ng C(a), I và I0 là c¡c di¹n dịch
k¸t nèi đối tượng được trong LΣy;Φy sao cho tồn t¤i mët LΣy;Φy -mô phỏng hai chi·u
 0 0
giúa I và I . Lúc đó I là mô h¼nh cõa KB khi và ch¿ khi I là mô h¼nh cõa KB. 
2.4. T½nh ch§t Hennessy-Milner đối với mô phỏng hai chi·u
 Mi·n cõa mët di¹n dịch trong ngôn ngú LΣ;Φ gồm có c¡c đối tượng và c¡c đối
tượng đó quan h» với nhau thông qua c¡c vai trá. Tªp c¡c đối tượng có quan h» với
mët đối tượng x¡c định có thº là húu h¤n hoặc vô h¤n. C«n cù vào tªp c¡c đối tượng
này để x¡c định t½nh ph¥n nh¡nh húu h¤n cõa mët di¹n dịch. T½nh ph¥n nh¡nh húu
h¤n cõa mët di¹n dịch trong ngôn ngú con được định nghĩa như sau [14]:
Định nghĩa 2.7. Mët di¹n dịch I trong LΣ;Φ được gọi là ph¥n nh¡nh húu h¤n (hay
 I y
húu h¤n £nh) đối với LΣy;Φy n¸u với mọi x 2 ∆ và với mọi vai trá r 2 ΣoR th¼:
 • tªp fy 2 ∆I j rI (x; y)g là húu h¤n,
 y I I
 • n¸u I 2 Φ th¼ tªp fy 2 ∆ j r (y; x)g là húu h¤n. 
 50
 T½nh ch§t Hennessy-Milner đối với mô phỏng hai chi·u trong Định lý 2.4 và H»
qu£ 2.3 sau đây được ph¡t triºn và chùng minh dựa tr¶n c¡c k¸t qu£ cõa nghi¶n
cùu [14] cho mët lớp lớn hơn c¡c logic mô t£ đã đề cªp trong Mục 1.2.2 cõa Chương 1.
Ð đây, t½nh ch§t Hennessy-Milner được ph¡t biºu tr¶n c¡c di¹n dịch ph¥n nh¡nh húu
h¤n. Định lý 2.4 tr¼nh bày điều ki»n c¦n và đủ để x¥y dựng t½nh b§t bi¸n dựa tr¶n c¡c
di¹n dịch ph¥n nh¡nh húu h¤n.
Định lý 2.4 (T½nh ch§t Hennessy-Milner). Cho Σ và Σy là c¡c bë ký tự logic mô t£
sao cho Σy ⊆ Σ, Φ và Φy là tªp c¡c đặc trưng cõa logic mô t£ sao cho Φy ⊆ Φ, I và
 0
I là c¡c di¹n dịch trong LΣ;Φ thỏa m¢n điều ki»n ph¥n nh¡nh húu h¤n đèi với LΣy;Φy ,
 y I I0 y
sao cho với mọi a 2 ΣI , a LΣy;Φy -tương đương với a . Gi£ thi¸t r¬ng U 62 Φ hoặc
 y I 0 I0
ΣI 6= ;. Lúc đó, x 2 ∆ LΣy;Φy -tương đương với x 2 ∆ khi và ch¿ khi tồn t¤i mët
 0 0
LΣy;Φy -mô phỏng hai chi·u Z giúa I và I sao cho Z(x; x ) thỏa m¢n. 
Chùng minh. Gi£ sû Σ và Σy là c¡c bë ký tự logic mô t£ sao cho Σy ⊆ Σ, Φ và Φy
là tªp c¡c đặc trưng cõa logic mô t£ sao cho Φy ⊆ Φ, I và I0 là c¡c di¹n dịch trong
 y
LΣ;Φ thỏa m¢n điều ki»n ph¥n nh¡nh húu h¤n đối với LΣy;Φy , sao cho với mọi a 2 ΣI ,
 I I0 y y
a LΣy;Φy -tương đương với a . Gi£ thi¸t r¬ng U 62 Φ hoặc ΣI 6= ;. Ta c¦n ph£i
 I 0 I0 0
chùng minh: (*) Với x 2 ∆ và x 2 ∆ , n¸u x LΣy;Φy -tương đương với x th¼ tồn t¤i
 0 0
mët LΣy;Φy -mô phỏng hai chi·u Z giúa I và I sao cho Z(x; x ) thỏa m¢n. (**) N¸u
 0 0
tồn t¤i mët LΣy;Φy -mô phỏng hai chi·u Z giúa I và I sao cho Z(x; x ) thỏa m¢n th¼
 0 I 0 I0
x LΣy;Φy -tương đương với x , trong đó x 2 ∆ và x 2 ∆ .
 Đầu ti¶n, ta chùng minh kh¯ng định (*). Gi£ sû có x 2 ∆I , x0 2 ∆I0 thỏa m¢n x
 0
LΣy;Φy -tương đương với x . Ta định nghĩa quan h» Z như sau:
 0 I I0 0
 Z = fhx; x i2 ∆ × ∆ j x LΣy;Φy -tương đương với x g;
và ch¿ ra r¬ng Z là mët mô phỏng hai chi·u giúa I và I0.
 I I0 I I0
 - X²t điều ki»n (2.1), v¼ theo gi£ thi¸t a LΣy;Φy -tương đương với a n¶n Z(a ; a )
thỏa m¢n.
 - X²t điều ki»n (2.2) và gi£ sû Z(x; x0) thỏa m¢n. Theo định nghĩa cõa quan h»
 I I0 0
Z và quan h» LΣy;Φy -tương đương, ta có A (x) thỏa m¢n khi và ch¿ khi A (x ) thỏa
 y
m¢n với mọi t¶n kh¡i ni»m A 2 ΣC .
 - X²t điều ki»n (2.3) và gi£ sû Z(x; x0) thỏa m¢n. N¸u BI (x) x¡c định và BI (x) = d.
Lúc đó ta có x 2 (B = d)I . V¼ x 2 (B = d)I và theo định nghĩa cõa quan h» Z và
 0 I0 I0 0
quan h» LΣy;Φy -tương đương n¶n x 2 (B = d) . Nói c¡ch kh¡c B (x ) = d và do đó
BI (x) = BI0 (x0). Tương tự, n¸u BI0 (x0) x¡c định th¼ BI (x) x¡c định. Tø đó suy ra
 51
BI (x) không x¡c định khi và ch¿ khi BI0 (x0) không x¡c định. Vªy ta có BI (x) = BI0 (x0)
hoặc c£ hai không x¡c định.
 - X²t đi·u ki»n (2.4) và gi£ sû Z(x; x0), rI (x; y) thỏa m¢n. Đặt S = fy0 2 ∆I0 j
rI0 (x0; y0)g, ta c¦n ch¿ ra r¬ng tồn t¤i y0 2 S sao cho Z(y; y0) thỏa m¢n. V¼ rI (x; y)
 I 0 0 I0
thỏa m¢n n¶n x 2 (9r:>) . V¼ x LΣy;Φy -tương đương với x n¶n x 2 (9r:>) . Tø
x0 2 (9r:>)I0 ta suy ra S 6= ;. Mặt kh¡c, I0 là mët di¹n dịch ph¥n nh¡nh húu h¤n đối
 0 0 0
với LΣy;Φy n¶n S là mët tªp húu h¤n. Gọi y1; y2; : : : ; yn là c¡c ph¦n tû cõa S, ta có
 0
n ≥ 1. Gi£ sû Z(y; yi) không thỏa m¢n với mọi 1 ≤ i ≤ n. Điều này suy ra y không
 0
LΣy;Φy -tương đương với yi với mọi 1 ≤ i ≤ n. Nghĩa là, với méi 1 ≤ i ≤ n, tồn t¤i kh¡i
 I 0 I0 I
ni»m Ci sao cho y 2 Ci và yi 62 Ci . Đặt C ≡ 9r:(C1 u C2 u · · · u Cn), ta có x 2 C và
 0 I0 0
x 62 C . Điều này m¥u thu©n với gi£ thi¸t x LΣy;Φy -tương đương với x . Do vªy, tồn
 0 0
t¤i yi 2 S sao cho Z(y; yi) thỏa m¢n.
 - Điều ki»n (2.5) được chùng minh tương tự như điều ki»n (2.4).
 - X²t điều ki»n (2.6) và gi£ sû Z(x; x0) thỏa m¢n. B¬ng c¡ch thay kh¡i ni»m A
trong điều ki»n (2.2) bởi kh¡i ni»m 9σ:fdg, ta suy ra được x 2 (9σ:fdg)I khi và ch¿
khi x0 2 (9σ:fdg)I0 . V¼ vªy, σI (x; d) , σI0 (x0; d).
 - Điều ki»n (2.7) và (2.8) trong trường hñp I 2 Φy được chùng minh tương tự như
điều ki»n (2.4) và (2.5) b¬ng c¡ch thay vai trá r bởi vai trá r−.
 - X²t điều ki»n (2.9) trong trường hñp O 2 Φy và gi£ sû Z(x; x0) thỏa m¢n. Đặt
 0 I 0 I0
C ≡ fag. V¼ x LΣy;Φy -tương đương với x n¶n x 2 C khi và ch¿ khi x 2 C . Do đó,
ta có x = aI khi và ch¿ khi x0 = aI0 .
 - X²t điều ki»n (2.10) trong trường hñp N 2 Φy và gi£ sû Z(x; x0) thỏa m¢n.
Đặt S = fy 2 ∆I j rI (x; y)g và S0 = fy0 2 ∆I0 j rI0 (x0; y0)g. V¼ I và I0 là c¡c di¹n
 0
dịch ph¥n nh¡nh húu h¤n đối với LΣy;Φy n¶n S và S là húu h¤n. N¸u S = ;, ta có
 I 0 0 I0 0 I0
x2 = (9r:>) và do x LΣy;Φy -tương đương với x n¶n ta có x 2= (9r:>) . V¼ x 2= (9r:>)
 0 0
n¶n ta có S = ;. Tø đó suy ra #S = 0 = #S . N¸u S 6= ;, gọi y1; y2; : : : ; yn là c¡c
 I I
ph¦n tû cõa S với n ≥ 1. Rã ràng x 2 (≥ n r:>) và x 2 (≤ n r:>) . Do x LΣy;Φy -tương
đương với x0 n¶n ta có x0 2 (≥ n r:>)I0 và x0 2 (≤ n r:>)I0 . V¼ x0 2 (≥ n r:>)I0 n¶n
#S0 ≥ n và v¼ x0 2 (≤ n r:>)I0 n¶n #S0 ≤ n. Tø đó suy ra #S = n = #S0. Nói c¡ch
kh¡c #fy 2 ∆I j rI (x; y)g = #fy0 2 ∆I0 j rI0 (x0; y0)g.
 - Điều ki»n (2.11) trong trường hñp fN ; Ig ⊆ Φy được chùng minh tương tự như
điều ki»n (2.10) b¬ng c¡ch thay vai trá r bởi vai trá r−.
 - X²t điều ki»n (2.12) trong trường hñp F 2 Φy và gi£ sû Z(x; x0) thỏa m¢n. Đặt
 52
 I I I I
C ≡ (≤ 1 r). N¸u x 2 C th¼ #fy 2 ∆ j r (x; y)g ≤ 1. V¼ x 2 C và x LΣ;Φ-tương
đương với x0 n¶n x0 2 CI0 và do đó #fy0 2 ∆I0 j rI0 (x0; y0)g ≤ 1. Tương tự, n¸u x2 = CI
th¼ x0 2= CI0 , do đó #fy 2 ∆I j rI (x; y)g > 1 và #fy0 2 ∆I0 j rI0 (x0; y0)g > 1. Vªy ta
có [#fy 2 ∆I j rI (x; y)g ≤ 1] , [#fy0 2 ∆I0 j rI0 (x0; y0)g ≤ 1].
 - Điều ki»n (2.13) trong trường hñp fF; Ig ⊆ Φy được chùng minh tương tự như
điều ki»n (2.12) b¬ng c¡ch thay vai trá r bởi vai trá r−.
 - X²t điều ki»n (2.14) trong trường hñp Q 2 Φy và gi£ sû Z(x; x0) thỏa m¢n. Đặt
S = fy 2 ∆I j rI (x; y)g và S0 = fy0 2 ∆I0 j rI0 (x0; y0)g. V¼ I và I0 là c¡c di¹n dịch
 0
ph¥n nh¡nh húu h¤n đối với LΣy;Φy n¶n S và S là húu h¤n. Gi£ sû không tồn t¤i
mët song ¡nh h : S ! S0 nào sao cho h ⊆ Z. Tø gi£ thi¸t này ta suy ra tồn t¤i mët
 00 0 0 0 0 0
y 2 S [S sao cho với y1; y2; : : : ; yk 2 S và y1; y2; : : : ; yk0 2 S kh¡c nhau tøng đôi mët
 00 0 00 00 00 0 00 0
LΣy;Φy -tương đương với y , ta có k 6= k . Đặt I = I n¸u y 2 S và I = I n¸u y 2 S .
 0 0 0 0 0 0
Đặt fz1; z2; : : : ; zhg = S n fy1; y2; : : : ; ykg và fz1; z2; : : : ; zh0 g = S n fy1; y2; : : : ; yk0 g. Với
 00 I00 I 0
méi 1 ≤ i ≤ h tồn t¤i Ci sao cho y 2 Ci và zi 2= Ci . Tương tự, với méi 1 ≤ i ≤ h tồn
 00 I00 0 I0
t¤i Di sao cho y 2 Di và zi 2= Di . Đặt C ≡ (C1 uC2 u· · ·uCh uD1 uD2 u· · ·uDh0 ).
 I I
Chúng ta có fy1; y2; : : : ; ykg ⊆ C và fz1; z2; : : : ; zhg \ C = ;. Tương tự như th¸,
 0 0 0 I0 0 0 0 I0 0 I
fy1; y2; : : : ; yk0 g ⊆ C và fz1; z2; : : : ; zh0 g \ C = ;. N¸u k > k th¼ x 2 (≥k r:C) và
x0 2= (≥k r:C)I0 . N¸u k < k0 th¼ x2 = (≥k0 r:C)I và x0 2 (≥k0 r:C)I0 . Điều này tr¡i với
 0
gi£ thi¸t x LΣy;Φy -tương đương với x . Do vªy, điều ki»n (2.14) thỏa m¢n.
 - Điều ki»n (2.15) trong trường hñp fQ; Ig ⊆ Φy được chùng minh tương tự như
điều ki»n (2.14) b¬ng c¡ch thay vai trá r bởi vai trá r−.
 - X²t điều ki»n (2.16) trong trường hñp U 2 Φy. V¼ I và I0 là c¡c di¹n dịch
 y 0
ph¥n nh¡nh húu h¤n đối với LΣy;Φy và U 2 ΣoR n¶n I và I là húu h¤n. Gi£ sû
 I0 0 0 0 I
∆ = fx1; x2; : : : ; xng với n ≥ 1. L§y mët đối tượng b§t kỳ x 2 ∆ , gi£ sû r¬ng x
 0
không LΣy;Φy -tương đương với xi với mọi 1 ≤ i ≤ n. Lúc đó, với méi 1 ≤ i ≤ n tồn t¤i
 0 I0 I y
mët kh¡i ni»m Ci sao cho xi 2 Ci và x2 = Ci . Đặt C ≡ (C1 t C2 t · · · t Cn) và a 2 ΣI
là mët t¶n c¡ thº, ta có aI0 2 (8U:C)I0 và aI 2= (8U:C)I . Điều này tr¡i với gi£ thi¸t
 I I0 0 I0 0
a LΣy;Φy -tương đương với a . Do đó, tồn t¤i xi 2 ∆ sao cho Z(x; xi) thỏa m¢n.
 - Điều ki»n (2.17) trong trường hñp U 2 Φy được chùng minh tương tự như
điều ki»n (2.16).
 - X²t điều ki»n (2.18) trong trường hñp Self 2 Φy và gi£ sû Z(x; x0) thỏa m¢n. V¼
 0 I 0 I0
x LΣy;Φy -tương đương với x n¶n x 2 (9r:Self) khi và ch¿ khi x 2 (9r:Self) . Do vªy,
rI (x; x) thỏa m¢n khi và ch¿ khi rI0 (x0; x0) thỏa m¢n.
 0
 Chùng minh kh¯ng định (**). Gi£ sû I và I là c¡c di¹n dịch trong LΣ;Φ thỏa điều
 53
ki»n ph¥n nh¡nh húu h¤n đối với LΣy;Φy , Z là mët LΣy;Φy -mô phỏng hai chi·u giúa I
và I0 sao cho Z(x; x0) thỏa m¢n. Theo kh¯ng định (2.19), với mọi kh¡i ni»m C cõa
 I I0 0
LΣy;Φy , C (x) thỏa m¢n khi và ch¿ khi C (x ) thỏa m¢n. Do đó, x LΣy;Φy -tương đương
 0
với x . 
H» qu£ 2.3. Cho Σ và Σy là c¡c bë ký tự logic mô t£ sao cho Σy ⊆ Σ, Φ và Φy là
tªp c¡c đặc trưng cõa logic mô t£ sao cho Φy ⊆ Φ, I và I0 là c¡c di¹n dịch trong
 y
LΣ;Φ thỏa điều ki»n ph¥n nh¡nh húu h¤n đối với LΣy;Φy . Gi£ thi¸t r¬ng ΣI 6= ; và với
 y I I0 0 I I0
mọi a 2 ΣI , a LΣy;Φy -tương đương với a . Lúc đó, quan h» fhx; x i 2 ∆ × ∆ j x
 0 0
LΣy;Φy -tương đương với x g là mët LΣy;Φy -mô phỏng hai chi·u giúa I và I . 
2.5. Tự mô phỏng hai chi·u
 Mët trong nhúng mục đích cõa luªn ¡n là sû dụng mô phỏng hai chi·u để thực
hi»n vi»c ph¥n ho¤ch mi·n cõa mët di¹n dịch. Để làm được điều này chúng ta c¦n
ph£i x¥y dựng được mô phỏng hai chi·u tr¶n cùng mët di¹n dịch, được gọi là tự mô
phỏng hai chi·u. Tø k¸t qu£ cõa c¡c nghi¶n cùu [14], [44] chúng tôi ph¡t triºn c¡c định
nghĩa, định lý sau đ¥y tr¶n lớp ngôn ngú đã đề cªp trong Mục 1.2.2 cõa Chương 1.
Định nghĩa 2.8 (Tự mô phỏng hai chi·u). Cho I là mët di¹n dịch trong LΣ;Φ. Mët
LΣy;Φy -tự mô phỏng hai chi·u cõa I là mët LΣy;Φy -mô phỏng hai chi·u giúa I và ch½nh
nó. Mët LΣy;Φy -tự mô phỏng hai chi·u Z cõa I được gọi là lớn nh§t n¸u với mọi
 0 0
LΣy;Φy -tự mô phỏng hai chi·u Z cõa I th¼ Z ⊆ Z. 
 Cho I là mët di¹n dịch trong LΣ;Φ, chúng ta ký hi»u LΣy;Φy -tự mô phỏng hai chi·u
 I
lớn nh§t cõa I là ∼Σy;Φy;I , và ký hi»u quan h» hai ngôi ≡Σy;Φy;I tr¶n ∆ là quan h»
 0 0
thỏa m¢n t½nh ch§t x ≡Σy;Φy;I x khi và ch¿ khi x LΣy;Φy -tương đương với x .
 Định lý 2.5 sau đây nói l¶n r¬ng tự mô phỏng hai chi·u lớn nh§t tr¶n mët di¹n
dịch là tồn t¤i và nó là mët quan h» tương đương. V¼ là nó mët quan h» tương đương
n¶n chúng ta có thº sû dụng nó để mô h¼nh hóa t½nh không ph¥n bi»t đưñc cõa c¡c
đối tưñng. Do đó, tự mô phỏng hai chi·u lớn nh§t đóng mët vai trá quan trọng trong
qu¡ tr¼nh ph¥n ho¤ch mi·n cõa mët di¹n dịch.
Định lý 2.5. Cho Σ và Σy là c¡c bë ký tự cõa logic mô t£ sao cho Σy ⊆ Σ, Φ và Φy
 y
là tªp c¡c đặc trưng cõa logic mô t£ sao cho Φ ⊆ Φ, I là mët di¹n dịch trong LΣ;Φ.
Lúc đó:
 1. LΣy;Φy -tự mô phỏng hai chi·u lớn nh§t cõa I tồn t¤i và nó là mët quan h»
 tương đương,
 54
 2. n¸u I là mët ph¥n nh¡nh húu h¤n đối với LΣy;Φy th¼ quan h» ≡Σy;Φy;I là mët
 LΣy;Φy -tự mô phỏng hai chi·u lớn nh§t cõa I (nghĩa là, quan h» ≡Σy;Φy;I và
 ∼Σy;Φy;I trùng khớp nhau). 
Chùng minh.
 - Kh¯ng định thù nh§t được suy ra trực ti¸p tø kh¯ng định thù nh§t cõa Bê đề 2.1.
 y y
 - X²t kh¯ng định thù hai, n¸u U 2= Φ hoặc Σ 6= ; th¼ theo Định lý 2.4, ≡Σy;Φy;I
 y y
là mët LΣy;Φy -tự mô phỏng hai chi·u cõa I. Trường hñp U 2 Φ và ΣI = ; là c¦n thi¸t
cho Định lý 2.4 để chùng minh điều ki»n (2.16) và (2.17). Thªt vªy, trong trường hñp
 y y 0
U 2 Φ và ΣI = ;, c¡c điều ki»n này rã ràng thỏa m¢n khi I = I. Như vªy ≡Σy;Φy;I
là mët LΣy;Φy -tự mô phỏng hai chi·u cõa I.
 B¥y giờ chúng ta chùng minh ≡Σy;Φy;I là mët LΣy;Φy -tự mô phỏng hai chi·u lớn
nh§t cõa I. Gi£ sû Z là mët LΣy;Φy -tự mô phỏng hai chi·u b§t kỳ cõa I. Với mọi
 I 0 I 0 0
x 2 ∆ và x 2 ∆ , ta c¦n ch¿ ra n¸u Z(x; x ) thỏa m¢n th¼ x ≡Σy;Φy;I x . V¼ Z là mët
 0
LΣy;Φy -tự mô phỏng hai chi·u cõa I và Z(x; x ) thỏa m¢n n¶n theo kh¯ng định (2.19)
 I I 0
với mọi kh¡i ni»m C cõa LΣy;Φy , C (x) thỏa m¢n khi và ch¿ khi C (x ) thỏa m¢n và do
 0
đó x ≡Σy;Φy;I x . Do đó, ta có Z ⊆ ≡Σy;Φy;I . Vªy ≡Σy;Φy;I là mët LΣy;Φy -tự mô phỏng
hai chi·u lớn nh§t cõa I. 
 Chúng ta nói r¬ng tªp Y bị ph¥n chia bởi tªp X n¸u Y n X 6= ; và Y \ X 6= ;.
Như vªy, tªp Y không bị ph¥n chia bởi tªp X n¸u hoặc Y ⊆ X hoặc Y \ X = ;. Ph¥n
ho¤ch Y = fY1;Y2;:::;Yng được gọi là nh§t qu¡n với tªp X n¸u với mọi 1 ≤ i ≤ n, Yi
không bị ph¥n chia bởi X.
 Định lý 2.6 sau đây nói l¶n kh£ n«ng ph¥n ho¤ch mi·n cõa di¹n dịch dựa tr¶n mô
phỏng hai chi·u lớn nh§t sao cho nó nh§t qu¡n với mët tªp c¡c đối tượng cho trước.
Khi mët ph¥n ho¤ch nh§t qu¡n với mët tªp c¡c đối tượng cho trước, chúng ta có thº
biºu di¹n tªp đó thông qua hñp cõa mët sè lớp tương đương trong ph¥n ho¤ch đó. Tø
đó cho ph²p chúng ta x¥y dựng thuªt to¡n học mët kh¡i ni»m trong h» thèng thông
tin thông qua mô phỏng hai chi·u lớn nh§t.
Định lý 2.6. Cho Σ và Σy là c¡c bë ký tự cõa logic mô t£ sao cho Σy ⊆ Σ, Φ và Φy là
tªp c¡c đặc trưng cõa logic mô t£ sao cho Φy ⊆ Φ, I là mët di¹n dịch húu h¤n trong
 I I
LΣ;Φ và X ⊆ ∆ . Gọi Y là ph¥n ho¤ch cõa ∆ thông qua quan h» ∼Σy;Φy;I . Lúc đó:
 I
 1. n¸u tồn t¤i kh¡i ni»m C cõa LΣy;Φy sao cho C = X th¼ ph¥n ho¤ch Y nh§t qu¡n
 với tªp X,
 55
 2. n¸u ph¥n ho¤ch Y nh§t qu¡n với tªp X th¼ tồn t¤i kh¡i ni»m C cõa LΣy;Φy sao
 I
 cho C = X. 
Chùng minh. V¼ I là mët di¹n dịch húu h¤n trong LΣ;Φ n¶n I thỏa m¢n điều ki»n
ph¥n nh¡nh húu h¤n đối với LΣy;Φy . Theo kh¯ng định (2) cõa Định lý 2.5, ta có ∼Σy;Φy;I
trùng khớp với ≡Σy;Φy;I .
 I
 - X²t kh¯ng định (1) và gi£ sû C = X với C là mët kh¡i ni»m cõa LΣy;Φy . Gọi
 I
Y = fY1;Y2;:::;Yng là mët ph¥n ho¤ch cõa ∆ được ph¥n ho¤ch thông qua quan
 0 0
h» ∼Σy;Φy;I . Với 1 ≤ i ≤ n, l§y x và x là hai ph¦n tû b§t kỳ cõa Yi, ta có x và x thuëc
v· mët lớp tương đương đưñc ph¥n ho¤ch bởi ∼Σy;Φy;I . Do ∼Σy;Φy;I trùng với ≡Σy;Φy;I
 0 I 0 I
n¶n x LΣy;Φy -tương đương với x và do đó x 2 C khi và ch¿ khi x 2 C . Nghĩa là
fx; x0g không bị ph¥n chia bởi CI . Do vªy, CI ph£i là hñp cõa mët sè lớp tương đương
được ph¥n ho¤ch bởi ∼Σy;Φy;I . Tø đó suy ra ph¥n ho¤ch Y nh§t qu¡n với X.
 - X²t kh¯ng định (2) và gi£ sû Y là mët ph¥n ho¤ch cõa ∆I được ph¥n ho¤ch
thông qua