Là quá trình xuất phát từ sự kiện cần chứng minh và thay vào đó là những sự kiện ở vế trái của 1 luật có vế phải là sự kiện cần chứng minh. Quá trình này được thực hiện cho đến khi đưa về các sự kiện là tập sự kiện con của tập sự kiện giả thiết.

(nghĩa là: để đưa ra kết luận b, ta thử tìm tất cả các luật có dạng: a₁ ù ....ù a_n Þ b, để có b, phải đưa ra các kết luận a₁,...,a_n. Quá trình xác định a_i cũng tương tự như đối với b, nếu đến một lúc nào đó phát hiện được rằng có một a_i nào đó không dẫn xuất được từ các giả thiết thì quay lui sang các luật sản xuất khác sinh ra b có dạng b₁ù....ùb_m Þ b. ngược lại, nếu mọi a_i đều dẫn xuất được giả thiết thì quá trình dẫn xuất ra b là đúng)

- giải thuật

gọi T là tập các sự kiện cần chứng minh tại thời điểm đang xét (khởi tạo T= G, G là tập kết luận).

S(p) ={r_iÎR / right(r_i) = p} ( là tập các luật trong R sao cho vế phải chứa p)

Procedure suydienlui (g);

Begin

T:= {g};

If Tì F then write (‘g đã được chứng minh ‘)

Else

Begin

p:=get(T);

If S(p) = {} then write (‘g không chứng minh được ‘)

Else

For r_iÎ S(p) do

Begin

T:= T \ right(r_i);

T:= T + left(r_i);

For lÎT \ F do suydienlui(l);

End;

End;