Ktl-icon-tai-lieu

Phân giải

Được đăng lên bởi phandaobn
Số trang: 80 trang   |   Lượt xem: 1724 lần   |   Lượt tải: 1 lần
IV. Phân giải

ntsơn

Tính hằng sai
• Mục tiêu :
Số diễn dịch của 1 công thức LLVT là vô hạn.
Làm sao biết được một công thức là hằng
đúng, hằng sai, khả đúng, khả sai ?.
Dựa vào định nghĩa ?
• Giải pháp ?

ntsơn

Tính hằng sai
Thuật toán
kiểm tra
hằng sai

yes

Thuật toán
kiểm tra
hằng đúng

yes

no

Công thức LLVT

no

Có cần thiết phải có 2 thuật toán ?

ntsơn

Tính hằng sai
• Chỉ cần 1 thuật toán :

Công thức F hằng sai ?

Công thức F hằng đúng ?

F

Thuật toán
kiểm tra
hằng sai

yes
no

¬F

ntsơn

Tính hằng sai
• Chỉ cần 1 thuật toán hằng sai :
F + yes
⎯⎯⎯→ F hằng sai.
¬F + yes
⎯⎯⎯→ F hằng đúng.
F + no và ¬F + no ⎯⎯→ F khả đúng, khả sai.

ntsơn

Tính hằng sai
• Lý do chọn hằng sai :

Hệ thống F

Hệ thống F

╞?═ H

Hằng sai ?

¬H
ntsơn

Tính hằng sai
• Mục tiêu :
Biết được công thức là hằng sai.
• Giải pháp :
* Biến đổi công thức (vẫn còn tính hằng sai).
* Co nhỏ không gian diễn dịch.

ntsơn

Tính hằng sai
Diễn dịch I

Công thức LLVT

Diễn dịch M

Diễn dịch L

Diễn dịch J
Diễn dịch M

•••

Diễn dịch N

Diễn dịchI K
Diễn dịch P

•••

Hằn
g
Yes sai
/No

Diễ
n
d
ịch
I

•••
ch
dị

N

Co nhỏ

ễn
DiDiễn dịch M

Diễn d

ịch L

Diễn dịch P

•••

Hằn
g
Yes sai
/No

(Không gian Herbrand)

ntsơn

Tính hằng sai

Công thức LLVT

Diễn dịch I
Diễn dịch M

Biến đổi

Diễn dịch L

Diễn dịch J
Diễn dịch M

•••

Diễn dịch N

Diễn dịchI K
Dạng chuẩn Skolem

Diễn dịch P

Hằng sai
Yes/No

•••

•••

ntsơn

Tính hằng sai
• Lưu ý :
Chỉ công thức đóng mới được đánh giá đúng
sai trong một diễn dịch.
Do đó, các công thức được đề cập từ đây trở đi
mặc nhiên là công thức đóng.

ntsơn

Dạng chuẩn Skolem
• Công thức F được chuyển về dạng :
1. Chuẩn Prenex.
2. Chuẩn giao.
3. Lần lượt xóa các lượng từ ∃”-”.
Với mỗi ∃x, thay tất cả các hiện hữu của x bằng
hàm fx. Hàm fx có thông số là các biến của các
lương từ ∀, với chỉ những lượng từ ∀ đứng
trước ∃x.
4. Tập SF có phần tử là các thành phần giao.
ntsơn

Dạng chuẩn Skolem
Thí dụ :
F = ∀x ∀y ∃z ∀t ∃s ∀v (p(x, y, z, t) ∧ q(s, v))
Xóa lượng từ ∃z, thay z bằng hàm fz(x, y)
∀x ∀y ∀t ∃s ∀v (p(x, y, fz(x, y), t) ∧ q(s, v))
Xóa lượng từ ∃s, thay s bằng hàm fs(x, y)
∀x ∀y ∀t ∀v (p(x, y, fz(x, y), t) ∧ q(fs(x, y, t), v))
Chuyển thành dạng tập hợp
SF = {p(x, y, fz(x, y), t), q(fs(x, y, t), v)}
dạng chuẩn Skolem

ntsơn

Dạng chuẩn Skolem
Thí dụ :
F = ∃x ∀y ∃z ∀t p(a, x, y, z, f(t))
Xóa lượng từ ∃x, thay x bằng hằng b
∀y ∃z ∀t p(a, b, y, z, f(t))
Xóa lượng từ ∃z, thay z bằng hàm fz(y)
∀y ∀t p(a, b, y, fz(y), f(t))
Chuyển thành dạng tập hợp...
ntsơn
IV. Phân gii
Phân giải - Trang 2
Để xem tài liệu đầy đủ. Xin vui lòng
Phân giải - Người đăng: phandaobn
5 Tài liệu rất hay! Được đăng lên bởi - 1 giờ trước Đúng là cái mình đang tìm. Rất hay và bổ ích. Cảm ơn bạn!
80 Vietnamese
Phân giải 9 10 443