suy diễn lùi (lập luận lùi - backward chaining hoặc backward reason)

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.

- 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 = "rỗng" 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;

Ví dụ

1) cho tập sự kiện F={p, r}, và tập luật R:

r₁) p =>q

r₂) q và r =>s

chứng minh s