Mộ số thuật giải liên quan đến mệnh đề một trong những vấn đề khá quan trọng của logic mệnh đề là chứng minh đúng đắng phép suy diễn . Đây cũng là bài toán chứng minh thường gặp trong toán học | END END CONST SO_LUAT 3 BEGIN WHILE x z AND y z DO BEGIN FOR i 1 TO SO_LUAT DO IF DK L THEN ThiHanh L END END. Đoạn chương trình chính cũng thi hành bằng cách lần lượt xét qua 3 lệnh IF như chương trình đầu tiên. Tuy nhiên ở đây biểu thức điều kiện được thay thế bằng hàm DK và các hành động ứng với điều kiện đã được thay thế bằng thủ tục ThiHanh. Tính chất mềm hơn của chương trình này thể hiện ở chỗ nếu muốn bổ sung tri thức ta chỉ phải điều chỉnh lại các hàm DK và ThiHanh mà không cần phải sửa lại chương trình chính. Bây giờ hãy giả sử rằng ta đã có hàm và thủ tục đặc biệt sau FUNCTION GiaTriBool DK String BOOLEAN PROCEDURE ThucHien ThaoTac String hàm GiaTriBool nhận vào một chuỗi điều kiện nó sẽ phân tích chuỗi tính toán rồi trả ra giá trị BOOLEAN của biểu thức này. Ví dụ GiaTriBoolean 6 7 sẽ trả ra FALSE Thủ tục ThucHien cũng nhận vào một chuỗi nó cũng sẽ phân tích chuỗi rồi tiến hành thực hiện những hành động được miêu tả trong chuỗi này. Với hàm và thủ tục này chương trình của chúng ta sẽ như sau CONST SO_LUAT 3 TYPE Luat RECORD DK String ThiHanh String 50 Sưu tầm bởi END DSLuat ARRAY OF Luat 9 VAR CacLuat DSLuat PROCEDURE KhoiDong BEGIN CacLuat 1 .DK x Vx CacLuat 2 .DK y 0 CacLuat 3 .DK y 0 9 CacLuat 1 .ThaoTac x 0 CacLuat 2 .ThaoTac y Vy CacLuat 3 .ThaoTac k min Vx-x y x x k y y-k END BEGIN WHILE x z AND y z DO BEGIN FOR i 1 TO SO_LUAT DO IF GiaTriBoolean CacLuat i .DK THEN ThucHien CacLuat i .ThaoTac END END. Chúng ta tạm cho rằng trong quá trình chương trình thi hành ta có thể dễ dàng thay đổi số phần tử mảng CacLuat các ngôn ngữ lập trình sau này như Visual C Delphi đều cho phép điều này . Với chương trình này khi muốn sửa đổi tri thức bạn chỉ cần thay đổi giá trị mảng Luat là xong. Tuy nhiên người dùng vẫn gặp khó khăn khi muốn bổ sung hoặc hiệu chỉnh tri thức. Họ cần phải nhập các chuỗi đại loại như x 0 hoặc k min Vx-x y .Các chuỗi này tuy có ý nghĩa đối với chương trình nhưng vẫn còn khá xa lạ đối với người dùng bình thường.
