MÁY TÍNH CÓ KHẢ NĂNG CHỨNG MINH ĐỊNH LÝ KHÔNG?
Trong khi học môn toán học, mọi người ai cũng từng gặp phả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 điển hình nhất.
Từ xưa đến nay, mọi người luôn tìm những phương pháp chứng minh định lý tự động hy vọng có một ngày con người sẽ nhập vào máy tính một định lý toán học để chứng minh vận dụng hệ thống chứng minh định lý trong máy tính, thì định lý sẽ được chứng minh một cách nhanh chóng.
Chứng minh định lý tự động cũng được gọi là ''chứng minh máy móc''.
Sở dĩ máy tính có thể chứng minh định lý là vì các chuyên gia đã ký hiệu và công thức hoá các quy tắc và công thức toán học, lưu trữ vào máy tính, tiếp sau đó lập ra một trình tự hoạt động cho nó. Trình tự này có thể bắt trước theo phương thức suy luận của con người. Sau khi bạn nhập vào máy tính tiền đề, kết luận và những hình thức ký hiệu, quy định, trình tự này liên tục kiểm tra trong công thức, quy tắc và tiền đề từ đó tiến hành tìm kiếm và suy luận đến khi đạt được kết quả tương đồng với kết luận. Mức độ của năng lực chứng minh định lý của máy tính chủ yếu quyết định ở sự tốt hay không tốt của trình tự chứng minh và số lượng quý tắc và công thức đã nhập vào máy. Trình tự càng được thiết kế tốt, thì quy tắc và công thức lưu trữ càng nhiều, năng lực chứng minh định lý của máy tính càng mạnh. Đương nhiên, quy tắc và công thức lưu trữ đã nhiều lên thì hiệu suất trình tự sức bị ảnh hưởng.
Dưới đây, xin hãy xem một ví dụ đơn giản.
xem xét hình 1, máy tính đã lưu trữ công thức liên quan đến hình 1.
Công thức 1: đối với hình thang do bốn đỉnh X,Y,U,V tạo thành trong đó đỉnh X là đỉnh bên trái đáy nhỏ, Y là đỉnh bên phải của đáy nhỏ, U là đỉnh phải đáy lớn, V là đỉnh trái đáy lớn, VY là đường chéo. Nếu là một hình thang thì đoạn thẳng XY song song với đoạn thẳng UV.
Công thức 2: Nếu XY song song với UV thì góc XYU và góc UVY bằng nhau. Cho một hình thang như hình 2, đoạn thẳng BD là đường chéo của hình thang, cần chứng minh hai góc đối đỉnh trong ABD và BDC bằng nhau, tức là cần chứng minh: nếu ABCD là hình thang, thì góc ABD và góc BDC bằng nhau.
Tiền đề nhập vào trong máy tính là: hình thang do 4 điểm A, B, C, D tạo thành, trong đó A là đỉnh trên bên trái, B là đỉnh trên bên phải, C là đỉnh dưới bên trái, D là đỉnh dưới bên phải, BD là đường chéo, ABCD là hình thang. Kết luận là: góc ABD và góc BDC bằng nhau.
Chương trình dựa vào tiền đề tìm thấy công thức 1, những tham số X, Y, U, V trong công thức 1 lần lượt thay thế cho A, B, C, D, thu được một ví dụ thực tế của công thức 1: nếu ABCD là một hình thang, thì đoạn thẳng AB song song với đoạn thẳng CD. Lại do tiền đề ''ABCD là một hình thang'', vì thế có được kết luận trung gian, tức kết luận của ví dụ thực tế của công thức 1: đoạn thẳng AB song song với đoạn thẳng CD. Lại do kết luận trung gian mà tìm thấy công thức 2, các tham số X, Y, U, V trong công thức 2 lần lượt thay thế cho A, B, C, D, thu được một ví dụ thực tế của công thức 2: nếu đoạn thẳng AB song song với đoạn thẳng CD, thì góc ABD bằng góc BDC. Lúc này, kết luân trung gian ''đoạn thẳng AB song song với đoạn thẳng CD'' giống với tiền đề của ví dụ thực tế của công thức 2, vì thế có được kết luận, tức kết luận của ví dụ thực tế của công thức 2: góc ABD và góc BDC bằng nhau. Đây chính là kết luận cần tìm, vì thế định lý được chứng minh.
Ở đây chúng ta chỉ miêu tả một cách không có hình thức quá trình chứng minh định lý của máy tính, trên thực tế, máy tính chứng minh định lý hoàn toàn là ký hiệu hoá và hình thức hoá.
Từ thập niên 50 của thế kỷ 20, máy tính chứng minh định lý đi từ giai đoạn ý tưởng đến giai đoạn thí nghiệm, và đã thu được rất nhiều kết quả đáng mừng. Năm 1956, Niuweier và một số người khác, đã nhập quá trình tư duy các quy tắc, các sách lược, các kỹ xảo, các bước giản hoá trong khi não người suy luận vào máy tính, chứng minh 38 định lý trong số 52 định lý của chương 2 cuốn ''nguyên lý toán học'' của Luosuohuaitehai, Năm 1963, qua sửa đổi bổ xung đã chứng minh được toàn bộ 52 định lý. Năm 1958, chương trình do một người Mỹ gốc Hoa là Vương Khiết viết ra đơn giản và có hiệu quả hơn chương trình của Niuweier, chỉ trong 5 phút là đã chứng minh được toàn bộ 52 định lý. Năm 1965, Lỗ Tân Tôn đưa ra nguyên lý quy kết, đơn giản hơn so với các hình thức khác và có lợi cho việc thúc đẩy sự phát triển việc thực hiện chứng minh định lý trên máy tính.
Các nhà khoa học Trung Quốc đã thu được những kết quả khiến mọi người phải khâm phục trong việc nghiên cứu chứng minh định lý trên máy tính, nhận được sự trọng thị và đánh giá cao của giới khoa học quốc tế. Trong đó, kết quả nghiên cứu của giáo sư Ngô Văn Tuấn là nổi tiếng nhất. Giữa năm 1976 và 1977, Ngô Văn Tuấn tìm thấy phương pháp chứng minh cơ giới hoá của định lý hình học, và đã chứng minh được hơn 100 định lý trên máy tính, Sau này, ông đã mở rộng phạm chứng minh định lý bằng máy tính sang các lĩnh vực khác như hình học mô phỏng, hình học tròn, hình học cầu và hình học phi ơclit. . .
Từ đó có thể thấy, con người có thể sử dụng khả năng chứng minh định lý của máy tính. Mục đích của nghiên cứu khả năng chứng minh của máy tính là làm cho máy tính trực tiếp tham gia vào hoạt động tư duy của con người, thay thế cho một phần sức lao động trí óc của con người, nâng cao năng lực và hiệu quả sáng tạo khoa học của con người. Về phương diện này, còn có rất nhiều công việc nghiên cứu cần phải làm.
