Điểm bất động đối với chương trình logic diễn giải

Thông báo Khoa học và Công nghệ * Số 1-2015 114 
ĐIỂM BẤT ĐỘNG ĐỐI VỚI CHƢƠNG TRÌNH LOGIC DIỄN GIẢI 
ThS. Trần Thái Sơn 
Trung Tâm Ngoại ngữ - Tin học, Trường Đại học Xây dựng Miền Trung 
Tóm tắt: Chương trình logic diễn giải và chương trình logic dạng tuyển đều là 
những mở rộng của chương trình logic. Bài báo này trình bày ngữ nghĩa điểm 
bất động đối với chương trình logic diễn giải. Đầu tiên, nghiên cứu ngữ nghĩa 
điểm bất động đối với chương trình logic dạng tuyển dương, trên cơ sở đó xây 
dựng các phép chuyển đổi chương trình logic, chương trình Horn diễn giải và 
chương trình logic diễn giải về chương trình logic dạng tuyển không chứa ký 
hiệu phủ định. Cuối cùng, xác định ngữ nghĩa điểm bất động thông qua chương 
trình được chuyển đổi. 
Từ khóa: Abductive Logic Programs; Logic Programming; Fixpoint 
Semantics; Disjunctive Logic Programs. 
1. Ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương 
Định nghĩa 1.1 
Một chương trình logic là một tập hữu hạn các mệnh đề có dạng sau: 
p ← q1  ...  qm  qm+1  ...  qn (1.1) 
hoặc ← q1  ...  qm  qm+1  ...  qn (1.2) 
trong đó n m 0, p và qi là các nguyên tố. Trong mệnh đề (1.1), vế trái của ← được 
gọi là đầu mệnh đề và vế phải của ← được gọi là thân mệnh đề. 
Mỗi mệnh đề dạng (1.2) được gọi là một ràng buộc toàn vẹn, với ý nghĩa không 
thể tất cả q1,,qm là đúng và đồng thời tất cả qm+1,,qn là sai. Một ràng buộc toàn vẹn 
còn được gọi là một mệnh đề âm nếu nó không chứa ký hiệu phủ định (tức là m = n) 
Chương trình logic không chứa ký hiệu phủ định được gọi là chương trình Horn. 
Chương trình Horn không chứa ràng buộc toàn vẹn được gọi là chương trình 
logic xác định. 
Định nghĩa 1.2 Chương trình logic dạng tuyển dương P là tập hữu hạn các mệnh 
đề có dạng p1   pl  q1    qm (l, m 0) trong đó pi và qj là các nguyên tố. 
Thể hiện I thỏa mãn mệnh đề nền p1   pl  q1    qm nếu {q1,...,qm}  I kéo 
theo pi I với mọi i ( 1 i l ). I là mô hình cực tiểu của P nếu nó là thể hiện cực tiểu 
thỏa mãn tất cả các mệnh đề nền từ P. 
Định nghĩa 1.3 [8] Cho P là một chương trình logic dạng tuyển dương và I 
là một tập của các thể hiện. Ánh xạ TP: 
HBHB 22 2 2 được xác định như sau: 

I
I
)()(
I
IPP TT 
Trong đó ánh xạ TP: 
HB2HB 2 2 được xác định như sau: 
Thông báo Khoa học và Công nghệ * Số 1-2015 115 
Ø, Nếu {q1,...,qm}  I đối với mệnh đề âm nền  q1  ...  qm của P; 
TP(I) = { J với mỗi mệnh đề nền Ci: ii m11 ...... qqpp l  
 của P sao cho },...,{
im1
qq  I và },...,{
il1
pp  I =  
 J = I  
i
}{ j
C
p )1( ilj } 
Đặc biệt, TP() =  
Theo định nghĩa này, nếu một thể hiện I không thỏa mãn một số mệnh đề âm 
nền thì TP(I) = . Ngược lại, nếu có một mệnh đề nền không âm Ci mà không thỏa 
mãn bởi I (tức là I thỏa mãn phần thân của Ci nhưng không thỏa mãn phần đầu Ci) thì I 
được mở rộng bằng cách bổ sung mỗi phần tuyển từ các phần đầu của mọi Ci. 
Định nghĩa 1.4 [8] Thứ tự lũy thừa của toán tử TP được xác định như sau. 
TP ↑ 0 = {}, 
TP ↑ n +1 = TP ↑ (TP ↑ n), 
TP ↑  = 
  n
TP ↑ n 
trong đó n là thứ tự kế tiếp và  là thứ tự giới hạn. 
Ví dụ 2.1 Cho chương trình logic dạng tuyển dương P gồm các mệnh đề: 
 p  q  r , 
 s  r , 
 r  , 
  q  s , 
TP ↑  đạt được từ P như sau: 
 TP ↑ 1 = {{r}}, 
 TP ↑ 2 = {{r, s, p}, {r, s, q}}, 
 TP ↑ 3 = {{r, s, p}} = TP ↑  
Định lý 1.1 [8] Cho P là một chương trình logic dạng tuyển dương. Lúc đó: 
(a) TP ↑  là một điểm bất động của P. 
(b) Mỗi phần tử trong TP ↑  là một mô hình của P. 
(c) Gọi MMP là tập của tất cả các mô hình cực tiểu của P. 
 MMP = min(TP ↑ ) 
 trong đó min(I) = { I I J I sao cho J  I } 
Chứng minh: 
(a) Khi I TP ↑ , giả sử không có thể hiện J trong TP ↑  sao cho I TP({J}). Trong 
trường hợp này với bất kỳ, có n ( n ) sao cho J không được bao hàm trong TP 
↑ n. Lúc đó, I TP ↑ n+1, mâu thuẫn với thực tế I TP ↑ . Vì vậy J TP ↑ , I 
TP (TP ↑ ). Do đó I TP↑n với bất kỳ +1 n  suy ra I TP ↑ . 
(b) Với bất kỳ I TP ↑ , I thỏa mãn mỗi mệnh đề nền âm từ P, với bất kỳ mệnh đề 
nền p1  ...  pl  q1  ...  qm từ P, {q1,,qm }  I kéo theo và Ai I với mọi i ( 
Thông báo Khoa học và Công nghệ * Số 1-2015 116 
1 i l. Do đó, I là một mô hình của P. 
(c) Vì MMP  min(TP ↑ ) là hiển nhiên từ (b). Cho I là mô hình cực tiểu của P, với 
mỗi nguyên tố A trong I có một mệnh đề nền p1 ...  pl  q1  ...  qm từ P sao 
cho {q1,...,qm}  I và A = pi với mọi i ( 1 i l ). Theo định nghĩa cấu trúc điểm 
bất động, I được chứa trong TP ↑ . Vì mỗi phần tử trong TP ↑  là một mô hình 
của P, I là một phần tử cực tiểu của TP ↑ . Do đó I min(TP ↑ ). 
Theo định nghĩa, điểm bất động TP ↑  luôn luôn tồn tại đối với bất kỳ 
chương trình logic dạng tuyển dương P và được xác định duy nhất cho mỗi P. 
Điểm bất động này được gọi là điểm bất động tuyển chọn của P. Định lý 1.1 (c) mô 
tả cấu trúc điểm bất động của ngữ nghĩa mô hình cực tiểu đối với các chương trình 
logic dạng tuyển dương. 
2. Ngữ nghĩa điểm bất động đối với chương trình logic 
Phần này nghiên cứu một phép chuyển đổi để chuyển đổi chương trình logic 
sang chương trình logic dạng tuyển không chứa ký hiệu phủ định. Ngữ nghĩa điểm bất 
động được xây dựng dựa trên chương trình logic đã được chuyển đổi. 
 Định nghĩa 2.1 Cho P là một chương trình logic. PK là chương trình nhận được 
từ P như sau: 
1. Mỗi mệnh đề dạng p  q1  ...  qm  ¬qm+1  ...  ¬qn được chuyển đổi thành 
mệnh đề dạng (p  Kqm+1  ...  Kqn)  Kqm+1 ...  Kqn  q1  ...  qm (2.1) 
 trong P
K
. 
2. Mỗi ràng buộc toàn vẹn được chuyển thành Kqm+1 ...  Kqn  q1  ...  qm 
3. Mỗi nguyên tố B trong cơ sở Herbrand (HB), bổ sung vào PK mệnh đề dạng 
  KB  B (2.2) 
Trong đó, Kq (t.ư Kq) là một nguyên tố mới mà ký hiệu q là độ tin cậy (t.ư. 
không tin cậy) 
Trong phép chuyển đổi, mỗi nguyên tố ¬qi được viết lại Kqi và chuyển sang phần 
đầu của mệnh đề. Hơn nữa, vì phần đầu p trở thành true khi mỗi Kqi trong phần thân 
là true nên điều kiện Kqm+1 ... Kqn được thêm vào p. 
Ràng buộc toàn vẹn  Kq  q cho thấy rằng mỗi nguyên tố q cùng một thời 
điểm không thể là true và không tin cậy (Kq). 
Một thể hiện IK của chương trình chuyển đổi bây giờ được xác định như một tập 
con của cơ sở Herbrand mới HBK: 
HB
K
 = HB  { Kq | q HB }  { Kq | q HB }. 
 Định nghĩa 2.2 Một nguyên tố trong HBK được gọi là mục tiêu nếu nó là trong 
HB và tập các nguyên tố mục tiêu trong thể hiện IK được ký hiệu bằng obj(IK). 
Chú ý: Kq và Kq không xem như là công thức mới trong logic hình thức mà 
xem như các nguyên tố mới được đưa ra trong chương trình mới chuyển đổi. Ý nghĩa 
của Kq được cho bởi  Kq  q, trong đó Kq chấp nhận ràng buộc chính tắc sau. 
Thông báo Khoa học và Công nghệ * Số 1-2015 117 
 Định nghĩa 2.3 [8] Một thể hiện IK là chính tắc nếu nó thỏa mãn điều kiện: Đối với 
mỗi nguyên tố nền q nếu Kq IK thì q IK. Với IK là tập của các thể hiện. Ký hiệu 
objc(I
K
) = { obj(I
K
) IK IK và IK là chính tắc } 
Để sử dụng điểm bất động tuyển chọn đối với ngữ nghĩa của chương trình 
chuyển đổi, một chương trình mới giống như PK trong định nghĩa 2.1 cho phép một 
phép tuyển của các phép hội của các nguyên tố trong phần đầu một mệnh đề được xác 
định như sau. Một mệnh đề có thể được phân tách ra thành một tập của các mệnh đề có 
dạng p1   pl  q1    qm (l, m 0). 
Mệnh đề có dạng 
 m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  (2.3) 
 đặt cho k1×k2××kl chuyển đổi thành mệnh đề dạng 
 m1,,2,1 ......21 qqppp lilii  (2.4) 
với mọi i1 = 1,,k1, i2 = 1,,k2, il = 1,...,kl. 
Một chương trình gồm các mệnh đề có dạng 
 m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  cũng xem như là một 
chương trình logic dạng tuyển dương. Ánh xạ có thể được áp dụng cho các mệnh đề 
dạng m1,,2,1 ......21 qqppp lilii  Ánh xạ được sửa đổi để xử lý một phép tuyển 
của các phép hội về các nguyên tố trong phần đầu. Đối với một phép hội của các 
nguyên tố F = p1  ...  pk, ký hiệu tập các phép hội của nó là conj(F) = {p1,,pk}. 
Định nghĩa 2.4 [8] Cho P là một chương trình logic gồm các mệnh đề có dạng 
m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  và I là một thể hiện. 
Ánh xạ TP : 2
HB
HB22 được xác định như sau: 
Ø, Nếu {q1,...,qm}  I đới với mệnh đề âm nền  q1  ...  qm của P; 
TP(I) = { J đối với mỗi mệnh đề nền Ci : 
ii m11
...... qqFF l  
 từ P sao cho {
im1
,...,qq }  I và conj(Fj) I với j = 1,,li 
 J = I  
i
)( j
C
Fconj (1 j li) }. 
Định lý sau đây trình bày đặc trưng điểm bất động về ngữ nghĩa mô hình bền 
vững đối với các chương trình logic. 
Định lý 2.1 [8] Cho P là một chương trình logic, PK là chương trình chuyển đổi của P 
và STP là tập tất cả các mô hình bền vững của P. Lúc đó: 
a) STP = objc( KPT ). 
b) P không có mô hình bền vững nếu và chỉ nếu objc( KPT ) = . 
Ví dụ 2.1 Cho P là chương trình logic gồm các mệnh đề: 
p  ¬q, 
q  ¬p, 
Thông báo Khoa học và Công nghệ * Số 1-2015 118 
r  q, 
r  ¬r, 
P
K
 là chương trình chuyển đổi của P gồm các mệnh đề: 
 P
K
 = { ( p  Kq)  Kq  , 
 q  Kp)  Kp  , 
 r  q, 
 ( r  Kr)  Kr  }  {  KB  B B HB }. 
Toán tử KPT được xác định như sau: 
0K PT = { } 
1K PT = { { p, Kq, q, Kp, r, Kr}, { p, Kq, q, Kp, Kr}, 
{ p, Kq, Kp, r, Kr}, { p, Kp, Kp, Kr}, { Kq, q, Kp, r, Kr}, 
{Kq, q, Kp, Kr}, {Kq, Kp, r, Kr}, { Kq, Kp, Kr} }, 
2K PT = { {p,Kq, Kp,Kr }, { Kq, q,Kp, Kr, r } , { Kq, Kp, Kr} }, 
3K PT = 2K PT = KPT . 
Trong KPT chỉ có phần tử thứ hai { Kq, q,Kp, Kr, r } là chính tắc. 
Vì vậy, objc( KPT ) = {{ q, r}}và {q, r} là mô hình bền vững duy nhất của P. 
3. Ngữ nghĩa điểm bất động đối với chương trình Horn diễn giải 
Đối với chương trình Horn diễn giải, để áp dụng phép chuyển đổi theo định 
nghĩa 2.1, một giả thuyết về nguyên tố q được thiết lập để định giá công thức phủ định 
¬q. Tính đúng đắn của giả thuyết âm Kq được kiểm tra thông qua ràng buộc toàn 
vẹn  Kq  q. 
Trong phép chuyển đổi của chương trình Horn diễn giải, mỗi vị từ diễn giải cũng 
có thể được coi như là một giả thuyết. Khác nhau duy nhất giữa các giả thuyết từ các 
vị từ diễn giải và giả thuyết từ công thức phủ định là giả thuyết dương Kr cho mỗi vị 
từ diễn giải r (r A) luôn luôn cần thỏa mãn ràng buộc chính tắc. 
Phép chuyển đổi của chương trình Horn diễn giải được định nghĩa như sau. 
Định nghĩa 3.1 Cho là một chương trình Horn diễn giải. 
K
AP là chương trình 
nhận được từ như sau: 
1. Mỗi mệnh đề dương trong P có dạng 
p  q1  ...  qm  r1  ...  rn (m, n 0) (3.1) 
(trong đó qi là các vị từ không diễn giải (qi A) và rj là các vị từ diễn giải (rj A)) 
được chuyển đổi thành mệnh đề dạng 
(p  r1    rn)  Kr1  ...  Krn  q1  ...  qm (3.2) 
trong 
K
AP . 
2. Mỗi ràng buộc toàn vẹn trong P được chuyển đổi thành 
Thông báo Khoa học và Công nghệ * Số 1-2015 119 
Kr1 ...  Krn  q1  ...  qm 
3. Mỗi vị từ diễn giải r trong A (r A) bổ sung vào 
K
AP mệnh đề 
 Kr  r 
Ví dụ 3.1 Cho chương trình Horn diễn giải như sau: 
 P = { p  q  a } 
A = {a} 
I = {a} là mô hình bền vững của 
Nhưng KAP = { ( p  a)  Ka  q,  Ka  a } là chương trình chuyển đổi 
của và K
A
T
P
 = {}. 
Bổ đề 3.1 [8] Cho là một chương trình Horn diễn giải, O là một quan sát. Nếu 
E  A là một giải thích của O thì có một giải thích E‟ của O sao cho E‟  E và IE‟ = 
obj(I
K) đối mọi IK K
A
T
P
. 
Ví dụ 3.1 Cho chương trình Horn diễn giải như sau: 
P = { hắt_hơi(X)  người(X)  cảm_lạnh(X), 
hắt_hơi(X)  người(X)  nóng_sốt(X), 
người(Tom)  , 
  người(X)  cảm_lạnh(X)  nóng_sốt(X) } 
 A = { cảm_lạnh(X), nóng_sốt(X) } 
Chương trình Horn diễn giải được chuyển đổi thành chương trình logic dạng 
tuyển dương 
K
AP gồm các mệnh đề sau: 
(cảm_lạnh(X)  hắt_hơi(X))  Kcảm_lạnh(X)  người (X), 
 (nóng_sốt(X)  hắt_hơi(X))  Knóng_sốt(X)  người(X), 
 người(Tom)  , 
  Kcảm_lạnh(X)  Knóng_sốt(X)  người(X), 
  Kcảm_lạnh(X)  cảm_lạnh(X), 
  Knóng_sốt(X)  nóng_sốt(X) 
Cho O = hắt_hơi(Tom) là một quan sát. Lúc đó: K
A
T
P
 = { M1, M2, M3 } 
Trong đó: 
M1 = { người(Tom), cảm_lạnh(Tom), hắt_hơi(Tom), Knóng_sốt(Tom)}, 
M2 = { người(Tom), Kcảm_lạnh(Tom), nóng_sốt(Tom), hắt_hơi(Tom) }, 
M3 = { người(Tom), Kcảm_lạng(Tom), Knóng_sốt(Tom) }. 
Vậy E1 = {cảm_lạnh(Tom)} và E2 = {nóng_sốt(Tom)} là hai giải thích cho quan 
sát O sau khi trích lọc các vị từ diễn giải từ M1 và M2. 
4. Ngữ nghĩa điểm bất động đối với chương trình logic diễn giải 
Phần này trình bày một phép chuyển đổi của chương trình logic diễn giải bằng 
cách kết hợp hai phép chuyển đổi trong mục 2 và 3. Trong đó, mỗi nguyên tố âm ¬q 
đối với vị từ không diễn giải q (q A) được chuyển đổi theo cách chuyển đổi của 
Thông báo Khoa học và Công nghệ * Số 1-2015 120 
chương trình logic nó được chia ra thành Kq và Kq. Mặt khác, khi một nguyên tố âm 
¬r với r là một vị từ diễn giải (r A) xuất hiện bên trong mệnh đề chương trình thì ¬r 
được chia ra thành Kr và r. 
Định nghĩa 4.1 Cho là một chương trình logic diễn giải. 
K
AP là chương trình 
nhận được từ như sau: 
1. Mỗi mệnh đề dạng 
p  q1  ...  qm  ¬qm+1  ...  ¬qs  r1  ...  rn  ¬rn+1  ...  ¬rt (4.1) 
trong P, (trong đó s m 0, t n 0), qj là các vị từ không diễn giải (qj A) và rk là 
các vị từ diễn giải (rk A)) được chuyển đổi thành mệnh đề dạng 
(p  r1    rn  ¬Kqm+1    ¬Kqs  ¬Krn+1    ¬Krt)  ¬Kr1    ¬Krn 
 Kqm+1   Kqs  rn+1    rt ← q1  ...  qm (4.1) 
 trong 
K
AP . 
2. Mỗi ràng buộc toàn vẹn trong P được chuyển thành 
Kr1   Krn  Kqm+1    Kqs  rn+1   rt  q1    qm 
3. Mỗi nguyên tố H trong cơ sở Herbrand (HB) được bổ sung vào 
K
AP mệnh đề có 
dạng  KH  H 
Chú ý: Chương trình chuyển đổi 
K
AP trong định nghĩa này có thể rút gọn thành 
chương trình PK (tại mục 2) khi các nguyên tố diễn giải A là rỗng và có thể rút gọn 
thành chương trình 
K
AP khi P là một chương trình Horn. 
Định nghĩa 4.2 Cho IK là một tập của các thể hiện, ký hiệu minA(I
K) được xác định 
như sau: 
minA (I
K
) = {IE I
K
 JF I
K
 sao cho F  E} 
Định lý 4.1 [8] Cho là một chương trình logic diễn giải. Lúc đó: 
(a) Gọi min-BM là tập của tất cả các mô hình bền vững cực tiểu của , 
min-BM = minA(objc( K
A
T
P
)). 
(b) Cho E là một tập con của A và O là một quan sát. E là giải thích cực tiểu của O 
đối với nếu và chỉ nếu 
 IE minA(objc( ))T K
A}) {P(

 O
. 
Ví dụ 4.1 Cho chương trình logic diễn giải như sau: 
 P = { p  r  b  ¬q 
 q  a 
 r  
  ¬p } 
A = {a, b} 
Chương trình 
K
AP được chuyển đổi từ là: 
K
AP = { ( p  b  Kq)  Kb  Kq  r, 
Thông báo Khoa học và Công nghệ * Số 1-2015 121 
 ( q  a)  Ka , 
 r  , 
 Kq  , }  {  KH  H | H HB} 
Lúc đó: {r, p, b, Kq, Ka, Kp } là tập chính tắc duy nhất trong K
AP
T . 
Vì vậy, min-BM = {{ r, p, b }} 
5. Kết luận 
Bài báo tập trung nghiên cứu một khuôn khổ đồng nhất cho việc mô tả điểm bất 
động của các chương trình logic dạng tuyển dương, chương trình Horn diễn giải và 
chương trình logic diễn giải. Dựa trên toán tử điểm bất động thông qua các tập của các 
thể hiện, ngữ nghĩa mô hình bền vững của chương trình logic diễn giải có thể được mô 
tả bởi điểm bất động của chương trình dạng tuyển dương được chuyển đổi phù hợp. So 
với các cách tiếp cận khác, lý thuyết điểm bất động ở đây cung cấp một cách thức lập 
luận để đưa ra các giải thích cho các quan sát từ chương trình logic diễn giải. 
TÀI LIỆU THAM KHẢO 
[1] Võ Thị Ngọc Huệ. 2009. Nghiên cứu đặc trưng điểm bất động và các kỹ thuật định 
giá truy vấn đối với cơ sở dữ liệu suy diễn dạng tuyển, luận văn thạc sĩ khoa học Công 
nghệ thông tin, chuyên ngành Khoa học máy tính, Trường Đại Học Khoa Học Huế. 
[2] Trần Thái Sơn. 2010. Nghiên cứu ngữ nghĩa và phương pháp định giá truy vấn đối 
với chương trình logic diễn giải, luận văn thạc sĩ khoa học Công nghệ thông tin, 
chuyên ngành Khoa học máy tính, Trường Đại Học Khoa Học Huế. 
[3] Alferes. J, Pereira. L.M and Swift. T. 2003. “Abduction in Well-Founded 
Semantics and Generalized Stable Models via Tabled Dual Programs”, Under 
consideration for publication in Theory and Practice of Logic Programming, 
arXiv:cs/0312057v1 [cs.LO]. 
[4] Denecker. M and Schreye. D.De. 1997. “SLDNFA an abductive procedure for 
abductive logic programs”, Journal of Logic Programming 34(2), pp. 111-167. 
[5] Gelfond. M and Lifschitcz. V. 1988. “The Stable Semantics for Logic 
Programming”, In Logic Programming: proceeding of the 5th International Conference 
and Symposium, MIT Press, pp. 1070-1080. 
[6] Mancarella. P and Terreni. G. 2009. “The CIFF Proof Procedure for Abductive 
LogicProgramming with Constraints: Theory, Implementation and Experiments”, 
Under consideration for publication in Theory and Practice of Logic Programming, 
arXiv:0906.1182v1 [cs.AI]. 
[7] Sakama. C and Inoue. K. 1994. “On the equivalence between disjunctive and 
abductive logic Programs”, In Proceeding of the 11th International Conference on 
Logic Programming, (MIT Press, Cambridge), pp. 489 – 503. 
[8] Sakama. C and Inoue. K. 1996. “A Fixpoint characterization of Abductive Logic 
Programs”, Journal of logic Programming 27, pp. 107-136.