Bài giảng Luận lý toán học - Chương 3: Luận lý vị từ (Phần 4) - Nguyễn Thanh Sơn

 nhất
• Để có được một mgu từ tập bất đồng thì tập bất 
đồng phải có :
1. Một biến.
2. Biến  biểu thức.
ntsơn
mgu
Thí dụ :
S = {p(x, y, z), p(f(y), z, g(w)), p(f(g(a)), z, t)} 
{x, f(y)}  0 = {f(y)/x}
S0 = {p(f(y), y, z), p(f(y), z, g(w)), p(f(g(a)), z, t)} 
{y, z}  1 = 0.{z/y} = {f(z)/x, z/y}
S1 = {p(f(z), z, z), p(f(z), z, g(w)), p(f(g(a)), z, t)} 
{z, g(w)}  2 = 1.{g(w)/z}
= {f(g(w))/x, g(w)/y, g(w)/z}
S2 = {p(f(g(w)), g(w), g(w)), p(f(g(a)), g(w), t)}
ntsơn
mgu
{z, g(w)}  2 = {f(g(w))/x, g(w)/y, g(w)/z}
S2 = {p(f(g(w)), g(w), g(w)), p(f(g(a)), g(w), t)} 
{w, a}  3 = 2.{a/w}
= {f(g(a))/x, g(a)/y, g(a)/z, a/w}
S3 = {p(f(g(a)), g(a), g(a)), p(f(g(a)), g(a), t)} 
{g(a), t}  4 = 3.{g(a)/t}
= {f(g(a))/x, g(a)/y, g(a)/z, a/w, g(a)/t}
S4 = {p(f(g(a)), g(a), g(a))}
mgu(S) ={f(g(a))/x, g(a)/y, g(a)/z, a/w, g(a)/t}
ntsơn
Thừa số
• Thừa số (factor) của một mệnh đề.
D = p(x)  p(f(y))  q(x)  p(z)
p(x) và p(f(y)) có mgu  = {f(y)/x}.
D = p(f(y)  q(f(y))  p(z) là thừa số.
p(z) và p(f(y)) có mgu  = {f(y)/z}.
D = p(x)  p(f(y)  q(x) là một thừa số.
p(x) và p(z) có mgu  = {x/z}.
D = p(x)  p(f(y)  q(x) là một thừa số.
ntsơn
Phân giải nhị phân
• Phân giải nhị phân của 2 mệnh đề.
C = p(x)  q(x) D = p(a)  r(x).
LC = p(x) và
LD = p(a).
LC và LD có mgu  = {a/x}.
(C  LC)  (D  LD) = q(a)  r(a).
 pgb(C, D) = (q(a)  r(a)) là phân giải nhị phân 
của C và D.
ntsơn
Phân giải nhị phân
Thí dụ
C = p(x)  r(a) D = p(b)  p(f(y))  r(x).
pgb(C, D) = r(a)  p(f(y))  r(b), với  = {b/x}.
pgb(C, D) = r(a)  p(b)  r(f(y)),
với  = {f(y)/x}.
pgb(C, D) = p(a)  p(b)  p(f(y)), với  ={a/x}.
ntsơn
Phân giải
• Phân giải của hai mệnh đề C, D :
1. Phân giải nhị phân của C và D.
2. Phân giải nhị phân của C và 1 thừa số của D.
3. Phân giải nhị phân của 1 thừa số của C và 1 
thừa số của D.
Ký hiệu pg(C, D)
ntsơn
Phân giải
Thí dụ
C = p(x)  q(a) D = p(z)  p(f(y))  r(x).
pg(C, D) = q(a)  p(f(y))  r(x).
pg(C, D) = q(a)  p(z)  r(f(y)),
pg(C, D) = q(a)  r(f(y)).
ntsơn
Phân giải
Định lý
Phân giải là hệ quả luận lý của 2 mệnh đề được 
phân giải.
C, D ╞═ pg(C, D)
Hệ quả
Một hệ thống hằng sai nếu phân giải ra được 
mệnh đề hằng sai ().
Quá trình phân giải sẽ dừng nếu không sinh ra 
được mệnh đề mới.
ntsơn
Chứng minh
• Chứng minh H là hệ qủa luận lý của F và G :
F = x (p(x)  (w(x)  r(x)))
G = x (p(x)  q(x))
H = x (q(x)  r(x))
Chuyển F, G và H thành dạng chuẩn.
F = x ((p(x)  w(x))  (p(x)  r(x)))
G = x (p(x)  q(x))
H = x (q(x)  r(x))
ntsơn
Chứng minh
• Hệ thống mới là :
(1) (p(x)  w(x))
(2) (p(x)  r(x)))
(3) p(a)
(4) q(a)
(5) q(x)  r(x).
pg(2, 3) = r(a) (6)
pg(4, 5) = r(a) (7)
pg(6, 7) = .
ntsơn
Problem-solving[13]
• If one number is less than or equal to a second 
number, and the second number is less than or 
equal to a third, then the first number is not 
greater than the third. A number is less than or 
equal to a second number if and only if the 
second number is greater than the first or the 
first is equal to the second. Given a number, 
there is another number that it is less than or 
equal to. Therefore, every number is less than 
or equal to itself.
[13] The essence of logic John Kelly. Prentice Hall 1997
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng ký hiệu toán học.
If (x  y) and (y  z) then not (x > z).
(x  y) iff (y > x)) or (x = y).
For every x, there is a y such that x  y.
Therefore, x  x for every x.
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng logic.
Các vị từ le (), gt (>), eq (=)
x y z ((le(x, y)  le(y, z))  gt(x, z))
x y (le(x, y)  (gt(y, x)  eq(x, y)))
x y le(x, y)
╞═ x le(x, x).
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng logic.
Các vị từ le (), gt (>), eq (=)
x y z ((le(x, y)  le(y, z))  gt(x, z))
x y (le(x, y)  (gt(y, x)  eq(x, y)))
x y le(x, y)
╞═ x le(x, x).
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng logic.
{
x y z ((le(x, y)  le(y, z))  gt(x, z)),
x y (le(x, y)  (gt(y, x)  eq(x, y))),
x y ((gt(y, x)  eq(x, y)))  le(x, y),
x y le(x, y),
(x le(x, x)).
} hệ thống hằng sai.
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng logic.
{
x y z (le(x, y)  le(y, z)  gt(x, z)),
x y (le(x, y)  gt(y, x)  eq(x, y)),
x y ((gt(y, x)  eq(x, y))  le(x, y)),
x y le(x, y),
x le(x, x).
} hệ thống hằng sai.
ntsơn
Problem-solving[13]
• Biểu diễn dưới dạng logic.
{
x y z (le(x, y)  le(y, z)  gt(x, z)),
x y (le(x, y)  gt(y, x)  eq(x, y)),
x y ((gt(y,x)  le(x,y))  (eq(x,y)  le(x,y)),
x y le(x, y),
x le(x, x)
} hệ thống hằng sai.
ntsơn
Problem-solving[13]
• Biến đổi về dạng chuẩn Skolem.
{
le(x, y)  le(y, z)  gt(x, z),
le(x, y)  gt(y, x)  eq(x, y),
gt(y, x)  le(x, y),
eq(x, y)  le(x, y),
le(x, f(x)),
le(a, a)
}
ntsơn
Problem-solving[13]
• Biến đổi về dạng chuẩn Skolem.
le(x, y)  le(y, z)  gt(x, z) (1’)
le(x, y)  gt(y, x)  eq(x, y) (2)
gt(y, x)  le(x, y) (3)
eq(x, y)  le(x, y) (4)
le(x, f(x)) (5)
le(a, a) (6)
ntsơn
Problem-solving[13]
• Biến đổi về dạng chuẩn Skolem.
/* le(x, y)  le(y, z)  gt(x, z) (1’) */
le(x, x)  gt(x, x) (1) thừa số (1’)
le(x, y)  gt(y, x)  eq(x, y) (2)
gt(y, x)  le(x, y) (3)
eq(x, y)  le(x, y) (4)
le(x, f(x)) (5)
le(a, a) (6)
ntsơn
Using Resolution[13]
• Phân giải.
pg(1, 2), pg(1, 3), pg(1, 4), pg(1, 5), pg(1, 6),
pg(2, 3), pg(2, 4), pg(2, 5), pg(2, 6),
pg(3, 4), pg(3, 5), pg(3, 6),
pg(4, 5), pg(4, 6),
pg(5, 6)
ntsơn
Using Resolution[13]
• Phân giải pg(1, 2).
M1 = le(x, x)  gt(x, x) (1)
M2 = le(x, y)  gt(y, x)  eq(x, y) (2)
 = {x/y}
M1 = le(x, x)  gt(x, x)
M2 = le(x, x)  gt(x, x)  eq(x, x)
pg(1, 2) = le(x, x)  eq(x, x)
ntsơn
Problem-solving[13]
• Some students attend logic lectures diligently. 
No student attends boring logic lectures 
diligently. Sean’s lectures on logic are attended 
diligently by all students. Therefore none of 
Sean’s logic lectures are boring.
• Chọn các vị từ :
lec(x) : x là bài giảng về logic
st(x) : x là student, s : Sean,
at(x, y) : x tham dự y chăm chỉ, 
bor(x) : x tẻ nhạt, gv(x, y) : x được cho bởi y
ntsơn
Problem-solving[13]
• Chuyển về LLVT
Some students attend logic lectures diligently.
There is an x who is a student and, for every y, 
if y is a logic lecture, then x attends y diligently.
x (st(x)  y (lec(y)  at(x, y)))
Nếu dịch :
x y (st(x)  lec(y)  at(x, y))) ???
y x (st(x)  lec(y)  at(x, y))) ???
ntsơn
Problem-solving[13]
• Chuyển về LLVT
No student attends boring logic lectures 
diligently.
For every x, if x is a student, then, for every y, if 
y is a lecture which is boring, then x does not 
attend y.
x (st(x)  y (lec(y)  bor(y)  at(x, y)))
ntsơn
Problem-solving[13]
• Chuyển về LLVT
Sean’s lectures on logic are attended diligently 
by all students.
If x is a lecture given by s then every student z 
attends it.
x (lec(x)  gv(x, s)  z (st(z)  at(z, x)))
ntsơn
Problem-solving[13]
• Chuyển về LLVT
Therefore none of Sean’s logic lectures are 
boring.
Every lecture given by s is not boring.
x ((lec(x)  gv(x, s))  bor(x))
ntsơn
Problem-solving[13]
• Tổng kết
x (st(x)  y (lec(y)  at(x, y)))
x (st(x)  y (lec(y)  bor(y)  at(x, y)))
x (lec(x)  gv(x, s)  z (st(z)  at(z, x)))
╞═ x (lec(x)  gv(x, s)  bor(x))
ntsơn
Problem-solving[13]
• Biến đổi
x (st(x)  y (lec(y)  at(x, y)))
x (st(x)  y (lec(y)  bor(y)  at(x, y)))
x (lec(x)  gv(x, s)  z (st(z)  at(z, x)))
 x (lec(x)  gv(x, s)  bor(x))
chứng minh hệ thống hằng sai.
ntsơn
Problem-solving[13]
• Biến đổi
x y (st(x)  (lec(y)  at(x, y)))
x y (st(x)  lec(y)  bor(y)  at(x, y))
x z (lec(x)  gv(x, s)  st(z)  at(z, x))
x (lec(x)  gv(x, s)  bor(x))
ntsơn
Problem-solving[13]
• Biến đổi
st(a)  (lec(y)  at(a, y))
st(x)  lec(y)  bor(y)  at(x, y)
lec(x)  gv(x, s)  st(z)  at(z, x)
lec(b)  gv(x, s)  bor(b)
ntsơn
Problem-solving[13]
• Biến đổi
st(a) (1)
lec(y)  at(a, y) (2)
st(x)  lec(y)  bor(y)  at(x, y) (3)
lec(x)  gv(x, s)  st(z)  at(z, x) (4)
lec(b) (5)
gv(x, s) (6)
bor(b) (7)
ntsơn
Problem-solving[13]
• Phân giải
st(a) (1)
lec(y)  at(a, y) (2)
st(x)  lec(y)  bor(y)  at(x, y) (3)
lec(x)  gv(x, s)  st(z)  at(z, x) (4)
lec(b) (5)
gv(x, s) (6)
bor(b) (7)
ntsơn
Problem-solving[13]
• Phân giải
st(a) (1)
lec(y)  at(a, y) (2)
st(x)  lec(y)  bor(y)  at(x, y) (3)
lec(x)  gv(x, s)  st(z)  at(z, x) (4)
lec(b) (5)
gv(x, s) (6)
bor(b) (7)
Nhận xét : dư (4) và (6) !!!.
ntsơn
Bài tập
Chương 4 : Phân giải
ntsơn
Dạng chuẩn Skolem
1. Chuyển về dạng chuẩn Skolem :
F = xy ((S(x,y)  T(x,y))  x T(x,y))
H = (x (p(x)  yz q(y,z)))
G = xy (z K(x,y,z)  v (H(y,v)u H(u,v)))
K = x ( e(x,0) 
(y ( e(y, g(x))  z (e(z, g(x))  e(y, z)) )))
ntsơn
Thay thế
2. Cho 3 thay thế  = f(y)/x, z/y, g(x)/z,
 = a/x, b/y, x/t,
 = y/z, h(x)/y, f(x)/t .
Tìm hợp nối  và  .
3. Dùng thuật toán đồng nhất tìm mgu của công 
thức P :
P = q(f(x),y,u), q(u,v,h(x)), q(t,y,z).
ntsơn
Thừa số
4. Cho thay thế  =a/x, b/y, g(x,y)/z và
E = p(h(x),z), Tính E. 
5. Tìm các thừa số của T :
T = p(h(x))  r(y)  p(f(y))  q(x)  r(g(a)) 
r(y)  p(a).
6. Dùng phân giải để khảo sát tính hằng sai, khả 
đúng của công thức :
(r(x,y,z)  v(f(y),w))  v(x,y)  t(x,z)  (t(x,y) 
 v(x,y))
ntsơn
Chứng minh
7. Bằng phân giải chứng minh tập S là hằng sai
S = p(x)  q(y), p(a)  r(x), p(a)  r(x), p(x) 
 q(b), r(a)  q(y), r(x)  q(b).
8. Dùng phân giải cho biết công thức F là hằng sai 
hay khả đúng :
F =(q(c)  p(b))  (q(c)  r(c))  (q(c)  r(c)) 
 (q(c)  p(b))  (r(c)  p(b))  (r(c) 
p(b)).
ntsơn
Hết slide