T f" '
ĐẠI HỌC Qưóc Gỉ A HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
ĐỖ TH AN H THỦY
NGHIÊN CỨU MỘT SỐ KHÍA CẠNH
LÝ THUYẾT CỦA LẬP TRÌNH LỎGIC
VÀ LẬP TRÌNH LOGIC MODAL
Chuyên ngành: Công nghệ thông tin
Mã số: 1.0U0
LUẬN VẦN THẠC s ĩ
• ■
Người hướng dẫn khoa học: (
PGS.TS. Hồ Thuần
oạ: học QUOC Gi- ' . I lộĩ I
: 'RUNG ĨẢ M t h o n g tin thì, ir r; í
r V - l o ) h >
Hà Nội - 2005
Mục lục
■ ■
Lời cảm ơn 1
Mục lục 2
Mở đầu 4
Chương 1. Tổng quan về lập trình logic 6
1.1. Giới thiệu về lập trình logic
6
1.2. Lập trình logic - các nội dung đang được nghiên cứu 7
1.3. Lập trình logic trone tương lai 10
Chương 2. Các nguyên lý cơ sờ 11
2.1. C hương trinh logic 11
2.1.1. Câu logic 11
2.1.2. Câu chương trình 12


50
4.2.1. Logic modal cấp một 50
4.2.2. Ngôn ngừ MProlog 51
4.2.3. Mô hình và khung làm việc (Model & frame) 53
4.2.4. Điểm bất động 59
4.2.5. Thuật giải SLD
.
60
4.3. Ví dụ áp dụng 61
4.4. Kết luận về lập trình logic modal 64
Kết luận 65
Phụ lục 66
Tài liệu tham khảo 75
3
M ở đầu
Lịch sử ỉập trình logic được bắt đầu từ logic ký hiệu (symbolic logic). Sau
đó, logic vị từ cấp một ra dời trên cơ sờ loeic ký hiệu và là một nhánh nghiên cứu
của logic ký hiệu. Logic vị từ cấp một đã trở thành nền tảng của lập trình logic và
có những bước phát triển mạnh trong thế kỷ 20.
Theo Salah al-Fadhli [13] cỏ thể chia lịch sử cùa lập trình logic thành ba giai
đoạn: Giai đoạn thứ nhất là việc tìm ra ngôn ngừ ký hiệu cùa logic. Người có ảnh
hưởng lớn nhất trong giai đoạn này là Aristotle, ông là người đầu tiên đưa ra
phương pháp suy diễn thành công “tam đoạn luận”. Sau này, các học trò của
Aristotle đã phát triển phương pháp suy diễn này thành các luật suy diễn. Giai đoạn
thứ hai là giai đoạn phát triển thực sự của logic ký hiệu và giai đoạn thứ ba là giai
đoạn đưa logic ký hiệu vào lập trình logic.
Điểm bắt đầu cùa lập trình logic là thuật giải tuyến tính của Robinson (trong
những năm 1960) và các nghiên cứu cùa các tác già Kowalski, Colmerauer (trong
những năm 1970) [3). Thuật giải cùa Robinson dùng để suy diễn trong chứng minh

Chi tiết nội dung trình bày như sau:
Chương 1 : Giới thiệu về lập trình logic, khái quát về hướng nghiên cứu này
ở trong và ngoài nước, các hướng mở rộng của lập trình logic.
Chưong 2: Hệ thống các nguyên iý cơ sở trong lập trinh logic. Đó ỉà lý
thuyết các mô hình; lý thuyết điểm bất động; thuật giải SLD (Linear resolution with
Selection function for Definite clause).
Chương 3: Trình bày về ngôn ngữ Prolog trong mối quan hệ với lập trinh
logic.
Chương 4: Giới thiệu về lập trinh logic modal (dạng thức) (modal logic
programming) - một mở rộng của lập trình logic cổ điển với việc thêm vào các toán
tử modal (modal operator).
Phần kết luận trình bày các nội dung mà đề tài đã làm được và đưa ra
hướng phát triển trong tương lai của đề tài.
Phần phụ lục trình bày các toán tử và một số chương trinh Prolog minh họa
đà được kiểm thừ.
5
Chương 1. Tổng quan về lập trình logic
1.1. Giới thiệu về lập trình logic
Lập trình logic đã được nghiên cứu từ những năm đầu cùa thập kỷ 70 thế kỷ
20 và được xem như có nguồn gốc tự nhiên từ việc nghiên cứu chứng minh định lý
tự động và trí tuệ nhân tạo [3]. Năm 1972, Kowalski và Colmerauer đã đưa ra ý
tường nền tảng cho rằng logic có thể được sử dụng như một ngôn ngữ lập trình.
Theo Kowalski thuật toán của lập trình gồm hai phần riêng biệt: phần logic và
phần điều khiển. Phần logic là câu lệnh (phát biểu) chi ra vấn đề cần giải quyết;
phần điều khiển là câu lệnh chi ra phải giải quvết vấn đề như thế nào.
Trong lập trình truyền thống, người lập trình phải định nghĩa các thao tác cần
thực hiện để giải bài toán. Nghĩa ỉà, phải chi ra cho máy tính biết cách thức giải
quyết vấn đề như thế nào. đó là cách tiếp cận thủ tục (procedural). Các giả thiết
thường là ẩn (không được viết trong chương trình).
Đối với lập trình logic, người la xây dựng chương trình bàng cách mô tả lĩnh

Để giải bài toán đó, về lý thuyết có hai cách tiếp cận là mô hình Herbrand
nhò nhất và điêm bất động nhò nhất của ánh xạ T từ tập các thể hiện Herbrand vào
tập các thể hiện Herbrand. Cà hai cách trên đều có chung một mục đích là tìm ra mô
hình Herbrand nhỏ nhất của p và nếu G có thể được suy diễn từ p thì G phải thuộc
mô hình Herbrand nhỏ nhất của p.
Tuy nhiên, các phương pháp để đạt được mục đích chung đó là khác nhau.
Với cách tiếp cận xây dựng mô hình Herbrand nhò nhất vấn đề tập trung là các sự
kiện nền, các luật trong p và các phép thế biến. Trong khi đó cách tiếp cận điểm bất
động lại tập trung vào các mô hình và điểm bất động nhỏ nhất cùa ánh xạ T chính là
mô hình Herbrend nhò nhất của p.
Trong thực hành suy diễn để tìm lời giải cho bài toán trên, một thủ tục suy
diễn lùi đã được xây dựng trên cơ sở của thuật giải SLD. Thuật giải SLD tìm ra các
câu trả lời đúng cho bài toán dựa trên các câu đích và các biến. Các câu trả lời đúng
ở đây cũng phải thuộc mô hình Herbrand nhỏ nhất của p.
1.2. Lập trình logic - các nội dung đang được nghiên cứu
Trên thế giới, lập trình logic đã và đang thu hút nhiều nghiên cứu của các
nhà khoa học bởi tính hiệu quả và phạm vi áp dụng rộng lớn của nó.
Lập trình logic cổ điển (classical logic programming) đã mang lại nhiều
thành tựu quan trọng và khảng định vị trí độc lập cùa lập trình logic trong ngành
khoa học máy tính.
Trong lập trình logic cổ điển, một chươns trình logic được định nghĩa là tập
hữu hạn các câu Horn (câu có dạng: A<- Bị, Bn; n > 0. Trong đó, A, Bj, j = 1, 2,
n là các công thức nguyên tố. A có thể ià rỗng). Dể chứng minh một câu G có
được suy diễn từ chương trình p hay không về lý thuyết cần phải chứng minh G có
là hệ quả logic của p hay không, và trone thực hành điều đó được thực hiện bằng
phép hợp nhất và phép thế. Đó là những nguyên tấc cơ bản của lập trình logic cổ
điển. Dựa trên nguyên tắc này, việc xây dựng mô tơ suy diễn đã bớt phức tạp và
hiệu quả hơn (thuật giải SLD là đúng đắn và đầy đù). Bời lẽ, nếu câu chương trình
có phần đầu không chứa đúng một nguyên tố như câu Hom thì vấn đề sẽ trờ nên
phức tạp.

được mà dựa trên trực giác là một yếu tố quan trọng trong việc quyết định khi nào
và cách thức sử dụng ràng buộc.
Với một chương trình logic, khi tỉm lời giải cho câu hòi, hệ thống áp dụng
chiến lược quay lui trên cây SLD để đảm bảo vét cạn tất cả các nhánh có thể. Việc
duyệt cây có thể được thi hành song song (thường được gọi là OR-parallelism) và
mọi cố gắng duvệt cây tìm lời giải cho một đích con phải dừng lại ngay khi nó hợp
nhất được với đầu cùa một câu bất kỳ. Đó là ý tưởng của toán tử ủy thác (commit
operator). Phép toán này chia thân câu chương trình thành hai phần: phần có gác
(guarded part) và phần thân (bodv part). Có thể xem toán tử ủy thác như một nhát
cắt. Khi một đích con đã có lời giải (ờ một nhánh nào đó của cây), nhát cẳt sẽ cắt bỏ
(không tiếp tục duyệt) tất cả các nhánh khác của cây có gốc là đích con đó. Đó là
những ý tưởng cơ bàn cho một lóp ngôn ngữ lập trình dựa trên lập trình logic và
được gọi là ngôn ngữ lập trình logic tương tranh (concurrent logic programming
language). Một câu chương trình ở đây là một câu có gác (guarded clause). Câu
chương trình có dạng H <- G|, Gm I B], Bn. Trong đó, n , m >0; G|, Gm là
các gác; I là ký hiệu phân tách phần gác và phần thân câu và được gọi là toán tử ủy
thác (commit operator). Chương trình là một tập hữu hạn các câu có gác. Mỗi câu
chương trình phải chứa chính xác một toán tử ủy thác. Toán tử này chia vế phải của
câu chương trình thành hai phần, được giải quyết theo một trật tự nhất định. Phần
gác được thi hành trước, sau đó là phần thân. Do đó, các literal trong các phần này
có thể được thi hành một cách song song. Vậy nên, một đích không thể có nhiều
hơn một lời giải và đó cũng là nhược điểm chính của lớp ngôn ngữ lập trình này.
Lập trình logic tương tranh thích hợp với các hệ thống song song và phân tán.
Như vậy, có thể thấy các hướng mở rộng dù theo cách tiếp cận nào cũng đều
tập trung vào việc mở rộng phần tử cơ bản xây dựng chương trình logic đó là câu
Hom. Mồi cách mở rộng đều có cơ sở, phạm vi áp dụng và khiếm khuyết riêng
nhưng tất cả đã góp phần quan trọng vào việc đưa lập trình logic đến gần với các
úma dụng thực tể hơn.
9
Hiện tại, trên thế giới các nghiên cứu tập trung nhiều vào lập trình logic ràng

Vx, Vxs (Lị V . v L J
Trong đó: Moi Lj là một lite ra l và X|, xs là các biến xuất hiện irong L|
V V Lm. Literal đã được định nghĩa trong [3].
Ví dụ: công thức Vx Vy (p(x, y) V -q (x ))
Là một câu vì X, y là các biến xuất hiện trong (p(x, y j V -iq(x ))
Ví dụ: công thức \/x Vy (p(x, y) V -q (x ) V r(z) V r(a) )
với a là một hằng , là một câu.
Ví dụ: công thức Vx Vy (p(x, y) V -q {x ) V r(z))
ichông là một câu logic vì các biển X, y xuất hiện trong
(p(x, y ) V - q ( x ) V r(z ) .

Tuy nhiên, bien z có một xuất hiện tự do trong (p(X, v) V - q (x ) V r(z).
Do các câu rất phổ biển trong lập trình logic nên để thuận tiện chúng ta ký
hiệu câu sau đây:
VX| Vxs (A| V V Ak V -iB| V V -iBn)
Trone đó: Aị, A k, B|, B n là các nguyên tổ và X(, x s là các biến xuất
hiện trong các nguyên tổ đó.
bằng:
A|, Ak <— B], Bn
Như vậy, trong ký hiệu câu, mọi biến đều được già định là có lượng từ phổ dụng,
các dấu phẩy ở vế phải ký hiệu phép hội, các dấu phẩy ờ vế trái ký hiệu phép tuyển.
Một câu chương trình là một câu có dạng:
A<—Bi, Bn (n > 0)
Trong câu chương trình chỉ có đúng một nguyên tố (là A). A được gọi là đầu
(head) và Bj, Bn được gọi ià thân {body) của câu chương trình.
Ví dụ: câu parent (X, Y, Z) <— father (X, Z), mother (Y, Z).
(với X, Y, z là các biến) là một câu chương trình.
Ý nghĩa của câu này là “nếu X là cha của z và Y là mẹ của z thì X và Y là
cha mẹ của Z”.
Dạng công thức logic cùa công thức trên được biểu diễn như sau:

min(A, B, C) <- A < B, c = A.
Là một chương trình logic.
Chương trình này sẽ tìm ra số nhỏ nhất trong 2 số A và B, kết quả đặt trong
biến c. Để chạy chương trình, ta phải nạp đoạn mã trên vào máy tính theo cú pháp
của một trình dịch nào đó hỗ trợ lập trình logic (chẳng hạn là Prolog). Sau đó, ta
đưa vào một đích. Ví dụ để tìm số nhỏ nhất trong 2 số 100 và 200 ta đưa vào đích
<- min(10Q, 200, C). Kết quả ta sẽ nhận được c ~ 100 là số nhỏ nhất trong hai số
đó.
2.2. Hệ quả logic và các mô hỉnh
Để xét tính đúng, sai của một công thức, đầu tiên ta cần phải gán ý nghĩa cho
mỗi ký hiệu trong công thức đó. Các phép liên kết logic và các lượng từ đều có ý
nghĩa cố định, nhưng các hằng, ký hiệu hàm, ký hiệu vị từ thì có ý nghĩa thay đổi
với từng miền thể hiện của chúng.
Một thể hiện đơn giản bao gồm một miền nào đó, mà trên miền này:
+ Xác định phạm vi của các biến,
+ Phép gán mỗi hằng là một phần tử của miền,
+ Phép gán mỗi ký hiệu hàm là một ánh xạ trên miền
+ Và phép gán mỗi ký hiệu vị từ là một quan hệ trên miền.
13
Do vậy, một thể hiện chi rõ ý nehĩa cho mồi kv hiệu trong công thức. Chúng
ta đặc biệt quan tâm đến các thể hiện mà ờ đó cône thức nhận giá trị logic “true”.
Thể hiện như vậy được gọi ỉà mô hình của công thức.
Định nghĩa: (Thể hiện (interpretation) [3])
Một thể hiện
ỉ
(interpretation) cùa một ngôn ngữ cấp một L hao gồm:
+ Một tập khác rỗng D, gọi là miền thế hiện.
+ Với mỗi hằng trong L, gán một phần tử trong D.
+ Với mối hàm n - ngôi trong L, gán một ánh xạ từ ữ' vào D.
+ Với mỗi vị từ n - ngôi trong L, gán một ánh xạ từ ữ' vào tập (true, false}

Gọi Ị là một thể hiện của một ngôn ngữ cấp một L, giả sử F ỉà một công thức
đóng của /. Khi đó, ỉ là mô hình cho F nếu giá trị chân lý của F đối với ỉ là đúng.
Với tập các công thức đóng s, Ị ỉà mô hình cho s nếu nó ỉà mô hình cho mọi
công thức trong s.
Ví dụ: Xét công thức Vx3yp(x,y) và thể hiện I như sau:
+ Miền D là miền các số nguyên chẵn, không âm. x,y G D
+ p là quan hệ “chia hết cho”.
Như vậy, I là mô hình cho p vì Vx3yp(x,y) luôn đúng đối với I. Phát biểu
của công thức p trong I là: “với mọi số nguyên X e D, luôn tồn tại một số nguyên y
e D để X chia hết cho y”.
Sau đây là định nghĩa về tính thôa được và tính xác đáng của công thức dựa
trên các mô hình.
Định nghĩa: (Tính thỏa được, xác đáng, không thỏa được của công thức [3])
Gọi s là tập các công thức đóng của ngôn ngữ cắp một L. Ta nói
+ s ì à thỏa được (satisfaction) nếu L có một thể hiện là mô hình cho s.
+ s là xác đáng (validity) nếu mọi thể hiện của L đều là mô hình cho s.
+ s là không thỏa được nếu nó không có mô hình.
2.2.1. Hệ quả logic
Định nghĩa: (Hệ quà logic (logical consequence) [3])
15
G là sir S là một tập các công thức đóng của một ngón ngừ cấp một L. Ta nói,
F là hệ quà logic của s nếu với mọi thể hiện Ị cùa L, 1 là mô hình của s kéo theo I là
mô hình cùa F.
Ví dụ: Cho s = {p(a), Vxp(x) -» q(x)}. F = q(a).
Gọi 1 ỉà một mô hình bất kỳ của S; a là một hằng thuộc miền thể hiện của I.
Khi đó, ta có p(a) đúng với I và Vxp(x) -» q(x) đúng với I => q(a) đúng => I cũng là
mô hình của F. Như vậy, F là hệ quà logic của s.
Như vậv, với một chương trình p và một câu đích G = <- B|, Bn(n >0),
ta cần chứng minh P u {G} là không thỏa được. Điều đỏ tương đương với việc
chứna minh 3yJ 3ym (B| A B n) (với y 1, ym là các biến xuất hiện trong B),

xem mọi mô hình Herbrand của p có là mô hình của A hay không. Neu đúng thì A
là hệ quả logic của p.
Ví dụ: Cho một chương trình p gồm các cône thức sau:
odd(s(0)).
odd(s(s(X))) <- odd(X).
Vũ trụ Herbrand của p bao gồm hằng 0 và hàm s. U|> = {0, s(0), s(s(0)),
Cơ sờ Herband của p chứa vị từ odd của các hạng thức nền trong Up.
Bp = {odd(0), odd(s(0)), odd(s(s(0))), }
Các thể hiện Herbrand của p là:
1,= {0 }.
I2={odd(s(0))}.
I3 = { odd(s(0)), odd(s(s(0)))}
ỉ4 = {odd(s"(0)) I n e {1,3, 5, 7, }}
I5 = Bp
Các thể hiện Herbrand Ịà các tập con của cơ sở Herbrand.
Il không phải là một mô hình của p vì nó không là mô hình Herbrand của
odd(s(0)). Còn I2, 13, Ỉ4, Is là các mô hình của odd(s(0)) vì ođd(s(0)) e Ij (i = 2, 3, 4,
5).
Tuy nhiên, I2 không phải là mô hình của p vì trong kết thế nền
odd(s(s(s(0)))) <- odd(s(0)), phần giả thiết odđ(s(0)) e I2 nhưng kết luận
odd(s(s(s(0)))) Ể I2 (phần kết luận sai trong I2). Tương tự, I3 cũng không là mô hình
của p.
__________________
! 0 '' I M o c Q L ! Ỏ c GIA - :
I iRvJỉv>-> ÍA M THONG i!í'] ’ >•>■ £
■ í - i c f n ì > 17
I4 là mô hình của p vì odd(s(0)) e I4 và ta xét luật odd(s(s(t))) <- odd(t) là
một kết thế nền bất kỳ cùa luật odd(s(s(X))) <- odd(X) với t G Up. Rõ ràng
ođd(s(s(t))) <- odd(t) đúng nếu odd(t) £ I4. Hơn thế nữa, nếu odd(t) e I4 thì
ođd{s(s(t))) € I4 và do đó, odd(s(s(t))) <- odd(t) đúnẹ trong I4. Tương tự I5 cũng là

chúng ta có một cách tiếp cận cho lời giải. Đó ỉà tìm ra mô hình Herbrand nhỏ nhất
Mp cùa p và xét xem G có thuộc Mp hay không. Nếu G Ể Mp thì p u {G} không
thỏa được và do đó -iG là hệ quả logic cùa p. Nếu G e M|>thì p u {G} thỏa được
và do đó G là hệ quả logic của p.
2.2.3. Xây dựng mô hình Herbrand nhỏ nhát
Có thể xem một chương trình hữu hạn là tập các sự kiện (fact) và các luật
(rule). Tiếp cận theo điểm bất động nhò nhất ta có thể xây dựng mô hình Herbrand
nhỏ nhất (một cách trực giác) như sau:
+ Tất cả các kết thế nền (ground instance) của các sự kiện phải thuộc mô
hình Herbrand. Vì nếu một thể hiện Herbranđ 1 không chứa kết thế nền của một sự
kiện A thì A không đúng trong I và như vậy ĩ không là một mô hình.
+ Xét luật A0 <r- Ai, An (n > 0) lấy bất kỳ kết thể nền nào (A0 <- Aj,
An)9 cùa luật. Nếu I chứa A|0, An0 thì nó phải chứa Ao0 để I là còn một mô hình.
Ở đây 8 là một phép thế biến bất kỳ.
Ví dụ: Xét chương trình p gồm các câu sau:
p(f(x)) <- q(x, g(x)).
q(a, g(b)).
q(b,(g(b)).
Ở đây: + a, b là các hăng, X là biến thuộc bảng chữ cái ngôn ngừ cấp một.
+ f(), g() là hàm, p(), q() là các vị từ thuộc ngôn ngữ cấp một.
Ta xây dựng mô hình Herbrand nhỏ nhất cho chương trình trên như sau:
+ Các kết thế nền cùa các sự kiện là: q(a, g(b)), q(b,(g(b)) => Mp = {q(a,
g(b)), q(b,(g(b))}.
+ Xét luật: p(f(x)) <- q(x, g(x))
-Dùng phép thế biến: 0 = {x/a}, ía cỏ: q(a, g(a)) Ể Mp nên p(f(a)) Ể Mp.
-Dùng phép thế biến: 9 = {x/b}, ta có: q(b, g(b)) e Mị» nên p(f(b)) e Mp.
Như vậy, mô hình Herbrand nhỏ nhất cho chương trình trên là: Mp = {q(a,
g(b)), q(b,(g(b)), p(f(b))}. Ở đây, nếu ta bò đi bất kỳ phần tử nào trong Mpthì nó
không còn là mô hình cho chương trình p nữa.
19

20
Sau đây là định nghĩa điểm bất động
Định nghĩa: (Điếm bất độne [1])
Cho L là một dàn đầy đủ và một ánh xạ: 77 L —> L. Ta nói a € Llà một điêm
bât động của T nếu T(a) = a
Đối với điểm bất động, ta đặc biệt quan tâm đến điểm bất động nhỏ nhất và
điểm bất động lớn nhất.
Định nghĩa: (Điểm bất động nhỏ nhất, điểm bất động lớn nhất [1])
Cho L lò một dàn đầy đủ và ảnh xạ T: L —> L. Khi đó a e L được gọi là điếm
bất động nhỏ nhắt cùa T nếu với mọi điếm bất động b của T, a < b. Ký hiệu điểm
bất động nhỏ nhất cùa T là lfp(T).
Tương tự, a e L được gọi là điếm bắt động lớn nhất cùa T nếu với mọi điểm
bắt động b của T, a >b.
Định nghĩa: (Ánh xạ đơn điệu [1])
Cho L là một dàn đầv đủ và T: L —> L là một ảnh xạ. T là ánh xạ đơn điệu
nếu:
với Vx, y € L, nếu X < V thì T(x) < T(y)
Định nghĩa: (Tập có hướng [1])
Cho L là một dàn đầy đù và X a L. X được gọi là có hirớng nếu mọi tập con
hữu hạn của X đều có một cận trên trong X.
Định nghĩa: (Ánh xạ liên tục [1])
Cho L là một dàn đầy đủ và T: L —> L là một ảnh xạ. Ta nói T là liên tục
nếu:
T(lub(X)) = lub(T(X)) với v x ç L và Xcó hướng.
Với một dàn đầy đủ L và một ánh xạ đơn điệu T: L -> L. Khi đó, T luôn có
điểm bất động nhỏ nhất và điểm bất động lớn nhất [1].
Lý thuyết về điểm bất động cùa một ánh xạ trong mổi liên hệ với chương
trình logic p có ý nghĩa quan trọng. Đó là đoi với một chicơng trình logic p tập tất
cả các thể hiện Herbrand của p làm thành một dàn đầy đủ và tồn tại một ánh xạ
liên tục liên kết với p xác định trên dàn đầy đù đó Ị1 ].

22
cùa ánh xạ Tp (đó là tập các sự kiện được suy diễn từ P). Lời giải của bài toán sẽ
thuộc tập các điểm bất động đó. Và đâv là cách tiếp cận bottom - up.
2.4. Thuật giải SLD
Như đã biết, bài toán quan trọng trone lập trinh logic là cho một chương
trình logic p, một đích G, vấn đề đặt ra là xác định tính không thỏa được của p u
{G}. Mô hình Herbrand nhỏ nhẩt và điểm bất động nhỏ nhất là cách tiếp cận lời giải
cho bài toán (về mặt xây dựng lý thuyết) theo hướng bottom - up, chủ yếu dựa trên
các mô hình.
Trong thực hành xây dựng thù tục suy diễn tìm lời giải cho bài toán trên,
người ta sử dụng một cách tiếp cận khác đó là sử dụng thuật giải SLD. Thuật giải
SLD là giải pháp đế tìm ra câu trả lời đúng đắn cho P u {G}. Đây là cách tiếp cận
theo hướng top - down, chù yếu dựa trên các câu đích và các biến.
2.4.1. Nội dung thuật giải
Thuật giải SLD được Kowalski tinh chế từ luật suy diễn trong chứng minh
định lý tự động của Robinson. SLD là viết tắt của Linear resolution with Selection
function for Definite clause (thuật giải tuyến tính với hàm chọn cho các câu hữu
hạn).
Phát biểu của thuật giăi như sau:
V~(A| A A Aj.| A Ai A Aj+1 A A A m) V(Bo < - B| A A Bn)
V~(A| A A Aj_| A B] A A Bn A Aị+I A A Am)0
Hoặc (dùng ký hiệu cùa lập trình logic):
<—(A|, Aj.|, A j, Aj+], A m) Bo <— B) A A B n
< - ( A ] A A A j.| A B i A A B n A A j+I A A A j e
Ở đây, A|, An, là các công thức nguyên tố.
Bo ■<— B| A A Bn (n > 0) là một câu chương trình trong chương trình
p.
mgu(Aj, Bo) = 0. Phép thế tổng quát nhất mgu đã được định nghĩa
trong [3].
Ta có thể mô tả thuật giải SLD như sau:

Ta đưa vào một câu đích G = <- student(Z). Áp dụng thuật giải SLD ta có:
Go : <- student(Z)
C i : student(Xũ) <- study_at(X0, Y0), university(Yo)
24
Hợp nhất student(Z) với student(Xo) mau 0| = {X0 / Z}. Giả sử hàm chọn ở
đây là luôn chọn đích con bên trái nhất.
G i : <- study_at(Z, Y 0), university(Yo).
c 2 : study_at(nam, dh_y khoa).
Hợp nhất study_at(Z, Y0) với study_at(nam. dh y khoa) mgu 02 = ịZ / nam,
Yo / dh_y_khoa}.
G2 : <- university(dh_y_khoa).
c3 : university(dh_y_khoa).
Phép thể ở đây là rồng 03 = {}.
G3 : □.
Như vậy phép thế của quá trình suy diễn là:
0|0203= {Xo/Z}{Z/nam, Yo/ dh_y_khoa} = {Xo/nam, Yo/ dh_y_khoa}.
Minh họa bằne sơ đồ như sau:
<- student(Z)
student(Xo) <- stuđy_at(X0, Y0), university(Yo)
study at(X0l Yũ), university(Yũ)
study_at(nam, dh_y_khoa)
u n i ve rs ity (d h_y_khoa )
university(dh_y_khoa)
Định nghĩa: (Dần xuất SLD (SLD-derivation) [3])
Gọi p là một chương trình, Go là một đích. Mộí dan xuất SLD (SLD-
derivation) của p u ịG} bao gồm một dãy (hữu hạn hoặc vô hạn) G = Go, G Ị,
Gn, các đích, mội dãv C/, C2, c„, các câu chương trình (đã thay đoi biến
trong đó) trong p và một dây 01, 02, 9„, các mgu sao cho Gị+I được suy dẫn từ
Gi dùng dị, /.
Mồi Cj được thay thế các biến sao cho khác các biến đã có trong Cị. Điều