Bài viết sưu tầm

B1 : Phát biểu lại giả thiết và kết luận của vấn đề dưới dạng chuẩn như sau: GT₁, GT₂, ...,GTn ® KL₁, KL₂, .., KLm

Trong đó : GTi và KLj là các biểu thức logic dạng chuẩn (chỉ chứa các phép toán : Ù , Ú , Ø )

B2 : Giả sử ØKL₁, ØKL₂,...ØKL_m là đúng, lúc đó ta có các biểu thức logic đúng sau:

{ GT₁, GT₂, ..., GTn , Ø KL₁, Ø KL₂, ..., Ø KLm }

B3 : Sau đó đưa về dạng chuẩn hội (tích các tổng)

Ví dụ:

                                    p®q Ù t º Øp Ú (q Ù t) º(Øp Ú q) Ù (ØpÚ t)

B4 : Xây dựng một mệnh đề mới bằng cách áp dụng đồng nhất đúng:

                                    (Øp Ú q) Ù (p Ú r) Þ q Ú r

Nghĩa là:      nếu (ØpÚ q) Ù (ØpÚ r): True thì có thêm biểu thức r Ú t: true và đưa vào tập giả thiết.

lặp lại quá trình trên cho đến khi sinh ra 2 mệnh đề có chân trị đối nhau (có sự mâu thuẫn) và bài toán lúc đó kết luận là được chứng minh, hoặc không tạo thêm mệnh đề mới nào gây mâu thuẫn và lúc này kết luận không chứng minh được.