Bài giảng Luận lý toán học - Chương 2: Luận lý mệnh đề (Phần 3) - Nguyễn Thanh Sơn

[*] Logic and Proof - Computer Science Tripos Part IB Michaelmas Term 
 Lawrence C Paulson - Computer Laboratory University of Cambridge lcp@cl.cam.ac.uk 
ntsơn 
@Nguyễn Thanh Sơn 
Dạng NNF 
 Thí dụ : 
 F = (A → ¬B) → (B ∨ ¬A) 
 F = ¬(A → ¬B) ∨ (B ∨ ¬A) (thay →) 
 F = ¬(¬A ∨ ¬B) ∨ (B ∨ ¬A) (thay →) 
 F = (A ∧ B) ∨ (B ∨ ¬A) (khai triển ¬) 
[*] Logic and Proof - Computer Science Tripos Part IB Michaelmas Term 
 Lawrence C Paulson - Computer Laboratory University of Cambridge lcp@cl.cam.ac.uk 
ntsơn 
@Nguyễn Thanh Sơn 
Từ NNF đến CNF[*] 
•  Đẩy ∨ vào trong, dùng 
 F ∨ (G ∧ H) = (F ∨ G) ∧ (F ∨ H) 
•  Đơn giản hóa : 
–  Xóa mệnhđề chứa 2 lưỡngnguyên trái dấu. 
 eg : (F ∨ G ∨ ¬F) ∧ (H ∨ K) = H ∨ K. 
–  Xóa mệnh đề chứa mệnh đề khác. 
 eg : (H ∨ K ∨ ¬F) ∧ (H ∨ K) = H ∨ K. 
–  Thay (F ∨ G) ∧ (¬F ∨ G) bằng G. 
[*] Logic and Proof - Computer Science Tripos Part IB Michaelmas Term 
 Lawrence C Paulson - Computer Laboratory University of Cambridge lcp@cl.cam.ac.uk 
ntsơn 
@Nguyễn Thanh Sơn 
Thuật toán CNF 
•  Function CNF (F) 
Begin 
 case 
 F là nguyên từ : return F 
 F = F1 ∧ F2 : return CNF (F1) ∧ CNF (F2) 
 F = F1 ∨ F2 : return Phb (CNF (F1), CNF (F2)) 
 endcase 
End 
[*] Logic and Proof - Computer Science Tripos Part IB Michaelmas Term 
 Lawrence C Paulson - Computer Laboratory University of Cambridge lcp@cl.cam.ac.uk 
ntsơn 
@Nguyễn Thanh Sơn 
Thuật toán CNF 
•  Function PhB (F1, F2) 
Begin 
 case 
 F1 = F11∧F12 : return PhB (F11,F2) ∧ Phb (F12,F2) 
 F2 = F21∧F22 : return PhB (F1,F21) ∧ Phb (F1,F22) 
 otherwise (không có toán tử ∧) : return F1 ∨ F2 
 endcase 
End 
ntsơn 
@Nguyễn Thanh Sơn 
Thuật toán NNF 
•  Function NNF (F) 
Begin 
 case 
 F là nguyên từ : return F 
 F = ¬¬F1 : return NNF (F1) 
 F = F1 ∧ F2 : return NNF (F1) ∧ NNF (F2) 
 F = F1 ∨ F2 : return NNF (F1) ∨ NNF (F2) 
 F = ¬(F1 ∧ F2) : return NNF (¬F1) ∧ NNF (¬F2) 
 F = ¬(F1 ∨ F2) : return NNF (¬F1) ∨ NNF (¬F2) 
 endcase 
End 
ntsơn 
@Nguyễn Thanh Sơn 
Thuật toán NO_ARROW 
•  Function NO_ARROW (F) 
Begin 
 case 
 F là nguyên từ : return F 
 F = ¬F1 : return ¬(NO_ARROW (F1)) 
 F = F1 ∧ F2 : return NO_ARROW (F1) ∧ NO_ARROW (F2) 
 F = F1 ∨ F2 : return NO_ARROW (F1) ∨ NO_ARROW (F2) 
 F = F1 →F2 :return ¬NO_ARROW(F1) ∨ NO_ARROW (F2) 
 endcase 
End 
ntsơn 
@Nguyễn Thanh Sơn 
Dạng CNF 
Thí dụ : 
F = (¬A ∧ B → A ∧ (C → B) 
F1 = NO_ARROW(F) 
= ¬(¬A ∧ B) ∨ (A ∧ (¬C ∨ B)) 
F2 = NNF(F1) 
= (A ∨ ¬B) ∨ (A ∧ (¬C ∨ B)) 
F3 = CNF(F2) 
= (A ∨ ¬B ∨ A) ∧ (A ∨ ¬B ∨ ¬C ∨ B) 
F3 =CNF(NNF(NO_ARROW(F))) 
ntsơn 
@Nguyễn Thanh Sơn 
Dạng CNF 
Thí dụ : 
F = (¬A ∧ B → A ∧ (C → B) 
CNF(NNF(NO_ARROW(F))) 
= (A ∨ ¬B ∨ A) ∧ (A ∨ ¬B ∨ ¬C ∨ B) 
Tuy nhiên, (A ∨ ¬B) cũng là một dạng CNF của F. 
Kết quả của CNF(NNF(NO_ARROW(F))) không 
chắc là tối ưu cho việc giải bài toán SAT. 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause 
•  Mệnh đề Horn là mệnh đề chỉ có 1 lưỡng 
nguyên dương (positive literal). 
Thí dụ : 
 (A) 
 (A ∨ ¬B) 
 (¬C ∨ D ∨ ¬E) 
•  Dạng Horn : giao của các mệnh đề Horn. 
Thí dụ : 
 (A ∨ ¬B) ∧ (¬C ∨ D ∨ ¬E) 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause 
•  Dạng Horn là giao các cấu trúc điều kiện (có 
hậu quả là một công thức nguyên và nguyên 
nhân là giao các công thức nguyên). 
Thí dụ : 
 (A ∨ ¬B) ∧ (¬C ∨ D ∨ ¬E) 
 thường được viết dưới dạng 
 (B → A) ∧ ((C ∧ E) → D) 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause 
•  Dạng Horn được định nghĩa bằng văn phạm 
Backus Naur form : 
 F ::= ⊥ | Ť | A 
 G ::= F | F ∧ G 
 H ::= G → F 
 K ::= H | H ∧ K 
Chú thích : 
 ⊥ là công thức hằng sai 
 Ť là công thức hằng đúng 
 A là công thức nguyên 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause 
Thí dụ : 
 (A → B) ∧ (A → ⊥) ∧ ((C ∧ E) → D) 
 ((A ∧ B ∧ C ∧ E) → D) ∧ (Ť → A) 
 Có thể loại trừ 2 dạng sau : 
 ⊥ → A và (A ∧ B) → Ť vì luôn luôn đúng, 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause & SAT 
•  Function HORN (F) 
Begin 
 Đánh dấu (đd) tất cả Ť có trong F. 
 while 
 có ((A1 ∧ ... ∧ An) → A) của F sao cho các Ai 
 bị đd và A chưa bị đd, khi đó đd mọi A của F 
 endwhile 
 if ⊥ bị đd then F hằng sai else F khả đúng 
End 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause & SAT 
•  Thí dụ : 
HORN ((A → ⊥) ∧ (Ť → A)) 
Begin 
 (A → ⊥) ∧ (Ť* → A) 
 (Ť* → A) : (A* → ⊥) ∧ (Ť* → A*) 
 (A* → ⊥) : (A* → ⊥*) ∧ (Ť* → A*) 
End 
⊥ bị đánh dấu. Vậy công thức F hằng sai. 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause & SAT 
•  Thí dụ : 
F = ((A → B) ∧ (Ť → A) ∧ ((A ∧ B ∧ C) → D)) 
HORN (F) 
Begin 
 (A → B) ∧ (Ť* → A) ∧ ((A ∧ B ∧ C) → D) 
 (A* → B) ∧ (Ť* → A*) ∧ ((A* ∧ B ∧ C) → D) 
 (A* → B*) ∧ (Ť* → A*) ∧ ((A* ∧ B* ∧ C) → D) 
End 
 vậy công thức F khả đúng. 
ntsơn 
@Nguyễn Thanh Sơn 
Horn clause & SAT 
•  Thí dụ : 
HORN ((A → B) ∧ ((C ∧ E) → D) ∧ (Ť → A) ∧ 
 ((A ∧ B ∧ C ∧ E) → D)) 
Begin 
 (A → B) ∧ ((C ∧ E) → D) ∧ (Ť* → A) ∧ 
 ((A ∧ B ∧ C ∧ E) → D) 
 (A* → B*) ∧ ((C ∧ E) → D) ∧ (Ť* → A*) ∧ 
 ((A* ∧ B* ∧ C ∧ E) → D) 
End vậy công thức khả đúng. 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ quả luận lý 
•  Nếu mọi mô hình của F cũng là mô hình của H 
thì H được gọi là hệ quả luận lý của F. 
 Ký hiệu F ╞═ H. 
•  F là KB, được gọi là tiền đề và H được gọi là 
kết luận. 
•  Logical Consequence = Entailment 
 = Hệ quả luận lý (HQLL). 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ quả luận lý 
•  Để chứng minh H là hệ quả luận lý của F : 
–  Liệt kê tất cả diễn dịch. 
–  Chọn các diễn dịch là mô hình của F. 
–  Kiểm tra xem các mô hình này có còn là mô 
hình của H hay không. 
F H 
Tập các Diễn dịch Tập các Diễn dịch Tập con 
thỏa thỏa 
Hệ quả luận lý 
╞═ 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ quả luận lý 
Thí dụ : 
 {A, B} ╞═ A ∨ B 
 {A, B} ╞═ A ∧ B 
 {A, B} ╞═ A → B 
 {A, A ∨ B} ╞‌═ A → B 
 {A ∨ B, A ∧ B} ╞═ A 
 {A ∨ B, A ∧ B} ╞═ B 
 {A ∨ B, A ∧ B} ╞═ A → B 
 {B, A → B} ╞═ A ∨ B 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ quả luận lý 
•  Kiểm tra X → Y, X ╞═ Y. 
Không là mô hình của KB 1 0 0 1 
1 1 1 1 1 
╞═ Y X X → Y Y X 
0 1 1 0 
0 1 0 0 
Không là mô hình của KB 
Không là mô hình của KB 
ntsơn 
@Nguyễn Thanh Sơn 
Ký hiệu hằng đúng 
•  Ký hiệu công thức H là hằng đúng : 
 ╞═ H 
 Ký hiệu ╞═ H có nghĩa là ∅ ╞═ H. 
 Hệ thống { F1,  , Fn }╞═ H 
 ↔ { F1,  , Fn } ∪ {CTHằngđúng}╞═ H 
 ↔ F1, ∧  ∧ , Fn ∧ CTHằngđúng ╞═ H 
 Do đó khi { F1,  , Fn } = ∅ thì 
 CTHằngđúng╞═ H. 
ntsơn 
@Nguyễn Thanh Sơn 
Công thức hằng đúng 
•  Nếu F ╞═ H thì công thức (F → H) hằng đúng. 
•  Một công thức hằng đúng : 
 F ╞═ H ↔ ╞═ (F → H) 
 F ╞═ H ↔ ╞═ ¬( F ∧ ¬H) 
 ( F1,  , Fn ╞═ H ) ↔ (F2,  , Fn ╞═ F1 → H) 
 ( F ╞═ H và H ╞═ K ) → (F ╞═ K) (truyền) 
ntsơn 
@Nguyễn Thanh Sơn 
Ký hiệu ╞═ 
•  Một số tác giả ký hiệu M ╞═ F, trong đó F là 
một công thức và M là một mô hình của F. 
ntsơn 
Chương 2 
Bài tập 
Chương 2 : Luận lý mệnh đề 
ntsơn 
@Nguyễn Thanh Sơn 
Lập bảng thực trị 
Cho các công thức sau : 
1. (¬P ∨ Q) ∧ (¬(P ∧ ¬Q)) 
2. (P → Q) → (¬Q → ¬P) 
3. (P → Q) → (Q → P) 
4. P ∨ (P → Q) 
5. (P ∧ (Q → P)) → P 
6. P ∨ (Q → ¬P) 
7. (P ∨ ¬Q) ∧ (¬P ∨ Q) ∧ (¬(P → Q)) 
ntsơn 
@Nguyễn Thanh Sơn 
Tương quan giữa các toán tử 
So sánh các công thức sau : 
 1. ¬(P → (¬Q)) và (P ∧ Q) 
 2. (¬P → Q) và (P ∨ Q) 
Nhận xét gì về sự liên hệ của các toán tử ? 
ntsơn 
@Nguyễn Thanh Sơn 
Tương quan giữa các toán tử 
Viết ra các công thức sau chỉ dùng → và ¬ : 
 1. (P ∨ Q) ∧ (Q → P) 
 2. (¬P ∨ Q) ∧ (¬(P ∧ ¬Q)) 
 3. P ∨ (P → Q) 
 4. (P ∧ (Q → P)) → P 
 5. P ∨ (Q → ¬P) 
 6. (P ∨ ¬Q) ∧ (¬P ∨ Q) ∧ (¬(P → Q)) 
ntsơn 
@Nguyễn Thanh Sơn 
Dùng thủ tục số học 
Tính các công thức : 
 1. (¬P ∨ Q) ∧ (¬(P ∧ ¬Q)) 
 2. (P → Q) → (¬Q → ¬P) 
 3. (P → Q) → (Q → P) 
 4. P ∨ (P → Q) 
 5. (P ∧ (Q → P)) → P 
 6. P ∨ (Q → ¬P) 
 7. (P ∨ ¬Q) ∧ (¬P ∨ Q) ∧ (¬(P → Q)) 
ntsơn 
@Nguyễn Thanh Sơn 
Sự tương đương 
Chứng minh sự tương đương của các công thức : 
 1. (P → Q) → (P ∧ Q) = (¬P → Q) ∧ (Q → P) 
 2. P ∧ Q ∧ (¬P ∨ ¬Q) = ¬P ∧ ¬Q ∧ (P ∨ Q) 
 3. (P → Q) ∧ (P → R) = (P → (Q ∧ R)) 
 4. P ∧ (P → (P ∧ Q)) = ¬P ∨ ¬Q ∨ (P ∧ Q) 
ntsơn 
@Nguyễn Thanh Sơn 
Hằng đúng - Hằng sai 
Xác định tính hằng đúng, hằng sai của các công 
thức : 
 1. ¬(¬S) → S 
 2. ¬(S ∨ T) ∨ ¬T 
 3. (S→T)→ (¬T→ ¬S) 
 4. P ∨ (P → Q) 
 5. (P ∧ (Q → P)) → P 
 6. ¬P ∧ (¬(P → Q)) 
 7. ((A ∨ B) ∧ (¬A ∨ C)) → (B ∨ C). 
ntsơn 
@Nguyễn Thanh Sơn 
Mô hình 
Tìm một mô hình cho mỗi công thức : 
 1. ¬(¬S) → S 
 2. ¬(S ∨ T) ∨ ¬T 
 3. (S→T)→ (¬T→ ¬S) 
 4. P ∨ (P → Q) 
 5. (P ∧ (Q → P)) → P 
 6. ¬P ∧ (¬(P → Q)) 
 7. ((A ∨ B) ∧ (¬A ∨ C)) → (B ∨ C). 
ntsơn 
@Nguyễn Thanh Sơn 
Mô hình 
Diễn dịch nào : 
 I1 = {S} 
 I2 = {S, ¬T} 
 I3 = {A, ¬B, C} 
 I4 = {S, ¬T, A, ¬B, C, P, ¬Q} 
là mô hình của các công thức sau : 
1. ¬(¬S) → S 2. ¬(S∨T) ∨ ¬T 
3. P ∨ (P → Q) 4. (P → Q) → (¬Q → ¬P) 
5. ((A ∨ B) ∧ (¬A ∨ C)) → (B ∨ C). 
ntsơn 
@Nguyễn Thanh Sơn 
Dạng chuẩn CNF 
Chuyển thành dạng CNF 
1. ¬(P → Q) 2. ¬(P ∨ ¬Q) ∧ (P ∨ Q) 
3. (¬P ∧ Q) → R 4. ¬(P ∧ Q) ∧ (P ∨ Q) 
5. (P → Q) → R 6. P → ((Q ∧ R) → S) 
7. P ∨ (¬P ∧ Q ∧ R) 8. ¬(P → Q) ∨ (P ∨ Q) 
9. (¬P ∧ Q) ∨ (P ∧ ¬Q). 
ntsơn 
@Nguyễn Thanh Sơn 
Hằng đúng - Hằng sai 
Chứng minh các công thức sau đây là hằng đúng, 
hằng sai, hay khả đúng khả sai : 
 1. ¬(¬S) → S 
 2. ¬(S∨T) ∨¬T 
 3. (S→T)→(¬T→ ¬S) 
ntsơn 
@Nguyễn Thanh Sơn 
Mô hình 
Tìm một mô hình I cho công thức F. 
 F = ((A∨B) ∧ ¬B) → A 
Mở rộng I để nó cũng là mô hình của G. 
 G = ((A∧C) ∨ ¬C) → A. 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ qủa luận lý 
Chứng minh ¬K là hệ quả luận lý của hệ thống 
{F1, F2, F3, F4} : 
F1 = J → P ∨ T, 
 F2 = K ∨ Q → J, 
 F3 = T → A, 
 F4 = ¬P ∧ ¬A. 
ntsơn 
@Nguyễn Thanh Sơn 
Hệ qủa luận lý 
Công thức nào là hệ quả luận lý của hệ thống 
 {A, B, A→ C } 
 1. A∨ B. 
 2. A ∧ B. 
 3. B → C. 
 4. (A ∧ B) ∨ C. 
ntsơn 
@Nguyễn Thanh Sơn 
Hằng đúng 
Công thức nào sau đây là hằng đúng : 
1. (x → x) 
 2. ¬(x ↔ x) 
 3. (((P → Q) ∧ (¬P → Q)) → Q) 
4. (¬A → (B → A)) 
 5. ((A ∨ B) → (¬B → A)) 
6. ((¬P ∧ Q) ∧ (Q → P)) 
 7. (((X → Y) → X) → Y). 
ntsơn 
@Nguyễn Thanh Sơn 
Hết slide