›
›

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

Download
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  
yes  
no  
Thuật toán  
kiểm tra  
hằng sai  
Công thức LLVT  
Thuật toán  
kiểm tra  
hằng đúng  
yes  
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
yes  
no  
Thuật toán  
kiểm tra  
hằng sai  
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  
• 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  
• 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, t)  
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  
SF = {p(a, b, y, fz(y), f(t)} dạng chuẩn Skolem  
ntsơn  
Dạng chuẩn Skolem  
Thí dụ :  
F = x y (p(a, x, f(y)) → y z u q(y, z, u))  
F = x y (p(a, x, f(y))  y z u q(y, z, u))  
F = x y (p(a, x, f(y))  t z u q(t, z, u))  
F = x y t z u (p(a, x, f(y)) q(t, z, u))  
y z (p(a, b, f(y)) q(g(y), z, h(y, z)))  
SF = {p(a, b, f(y)) q(g(y), z, h(y, z))}.  
ntsơn  
Dạng chuẩn Skolem  
Nhận xét :  
• Các hàm được đặt tên fx để không trùng tên với  
các hàm đã có của công thức.  
• Nếu trước x khô ng có lương từ phổ dụng thì  
thay bằng hàm không thông số. Hàm không  
thông số là một hằng.  
• Từ kết quả của bước 4 có thể tạo lại kết quả  
của bước 3.  
ntsơn  
Dạng chuẩn Skolem  
Nhận xét :  
• Công thức ở dạng chuẩn Prenex vẫn còn  
tương đương với công thức ban đầu.  
• Kết quả của bước chuyển về dạng chuẩn giao  
vẫn còn tương đương với công thức ban đầu.  
• Kết quả của bước xóa lượng từ không phải là  
công thức, dĩ nhiên là không tương đương với  
công thức ban đầu.  
ntsơn  
Dạng chuẩn Skolem  
• Ý nghĩa của việc thay biến x của lượng từ x.  
- Thay x bằng hằng.  
“có x có tính chất p” là công thức x p(x)  
“lấy c có tính chất p” là công thức p(c) với mục  
đích là làm đơn giản công thức.  
ntsơn  
Dạng chuẩn Skolem  
• Ý nghĩa của việc thay biến x của lượng từ x.  
- Thay x bằng hàm.  
“Everyone has a mother” (mỗi người đều có  
mẹ) là công thức x y mother(x, y).  
Nếu thay y bằng hằng thì công thức x  
mother(x, c) mang ý nghĩa khác. Phần tử y phụ  
thuộc vào x nên phải thay bằng hàm theo x.  
ntsơn  
Mệnh đề  
• Mỗi phần tử của dạng chuẩn Skolem được gọi  
là 1 mệnh đề.  
• Do đó mệnh đề được định nghĩa là hội các  
lưỡng nguyên.  
• Mệnh đề đơn vị là mệnh đề có 1 lưỡng nguyên.  
• Mệnh đề rỗng là công thức hằng sai.  
• Nhắc lại :  
F ⊥ = F (⊥ là công thức hằng sai), F.  
F Ť = F (Ť là công thức hằng đúng), F.  
ntsơn  
Tính hằng sai  
Định lý :  
Công thức F hằng sai nếu và chỉ nếu dạng  
chuẩn Skolem SF hằng sai.  
Nhận xét :  
Từ định lý trên có thể nói : công thức F và dạng  
chuẩn Skolem SF là tương đương theo nghĩa  
hằng sai, nghĩa là dạng chuẩn Skolem duy trì  
được tính hằng sai.  
ntsơn  
Tính hằng sai  
Ghi chú :  
Tính hằng sai chỉ được định nghĩa cho khái  
niệm công thức.  
Dạng chuẩn Skolem được gọi là hằng sai dựa  
vào công thức ở cuối bước 3 trong quá trì nh  
biến đổi về dạng chuẩn Skolem.  
ntsơn  
Nguyên tắc phân giải  
• Một hệ thống hằng sai nếu “sản sinh” được  
mệnh đề hằng sai.  
• Qui tắc truyền  
(P → Q), (Q → R) ╞═ (P → R),  
thay P bằng T :  
(T Q), (Q R) ╞═ (T R).  
ntsơn  
Nguyên tắc phân giải  
• (T Q), (Q R) ╞═ (T R).  
Có thể được hiểu là :  
* Mệnh đề (T R) được sinh ra từ 2 mệnh đề  
(T Q) và (Q R).  
* Phương thức sinh ra là bỏ đi 2 lưỡng nguyên  
đổi dấu của mỗi mệnh đề, hội những phần còn  
lại của 2 mệnh đề.  
* Mệnh đề được sinh ra là hệ quả luận lý của 2  
mệnh đề sinh ra nó.  
ntsơn  
Tải về để xem bản đầy đủ
ppt 72 trang myanh 18920 Free
Download
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng môn Luận lý toán học - Chương 3: Luận lý vị từ - Phần IV: Phân giải - Nguyễn Thanh Sơn", để tải tài liệu gốc về máy hãy click vào nút Download ở trên

File đính kèm:

  • pptbai_giang_mon_luan_ly_toan_hoc_chuong_3_luan_ly_vi_tu_phan_i.ppt