thuật giải bao gồm các bước sau:

B1: Phát biểu lại giả thiết và kết luận của vấn đề theo dạng chuẩn sau :

GT₁, GT₂, ..., GTn ® KL₁, KL₂, ..., KLm

Trong đó các GTi và KLi là các biểu thứclogic dạng chuẩn (chỉ chứa 3 phép toán cơ bản : ù , ú , Ø )

B2: Nếu GTi có phép ú thì tách thành hai dòng con.

Nếu ở Kli có phép ù thì tách thành hai dòng con.

Ví dụ: p ù (Ø p ú q) ® q thì tách thành 2 dòng:

p ù Ø p ® q

và p ù q ® q

Hoặc nếu có p ù q ® q ú r thì tách thành 2 dòng:

P ù q ® q

và p ù q ® r

B3: Một dòng được chứng minh nếu:

1) tồn tại chung một mệnh đề ở cả hai phía.

Ví dụ :

p ù q ® q ú r: True

2) Tồn tại 2 mệnh đề phủ định lẫn nhau (p và Øp)

Ví dụ: p ù Ø p ® q: true

B4 :

a) Nếu một dòng không còn phép nối ù hoặc ú ở cả hai vế và ở 2 vế không có chung một biến mệnh đề thì dòng đó không được chứng minh.

b) Một vấn đề được chứng minh nếu tất cả dòng dẫn xuất từ dạng chuẩn ban đầu đều được chứng minh.