Khi học môn toán, mọi người đều đã đụng tới vấn đề “chứng minh định lí”. Chứng minh định lí có thể nói là một quá trình suy luận lôgic điển hình.

Do vậy có thể thấy rằng người ta có thể làm cho máy tính có khả năng chứng minh. Mục đích của việc nghiên cứu chứng minh định lí bằng máy tính là để máy tính trực tiếp can dự vào quá trình hoạt động tư duy của con người, nâng cao khả năng và hiệu quả sáng tạo khoa học của loài người. ý nghĩa thật là to lớn và sâu xa. Về mặt này còn có nhiều việc phải làm nữa.

Từ khóa: Suy luận lôgic; Chứng minh định lí; Chứng minh cơ giới.