Hệ thống chứng minh toán học tương tác

Question

Tôi đang tìm một công cụ (GUI được ưu tiên nhưng CLI sẽ hoạt động) cho phép tôi nhập các biểu thức toán và sau đó thực hiện các thao tác của chúng nhưng hạn chế tôi chỉ hoạt động toán học hợp lệ. Ngoài ra, công cụ phải có khả năng lưu một phiên và sau đó chứng minh rằng tập hợp các hoạt động đã lưu là hợp lệ.

Lưu ý: Tôi Không tìm kiếm một hệ thống để tạo chứng minh, chỉ có kiểm tra xem các bước tôi tự xác định là hợp lệ.

Tôi đã sử dụng ACL2 cho các hoạt động tương tự và nó hoạt động tốt trong một số trường hợp nhưng rất khó sử dụng cho mọi thứ khác.

This little project is my motivation. Đây là loại mẫu D cho phép giải phương trình. Với phương trình này:

(A * B) = C + D/F; 

Bất kỳ biểu tượng nào có thể được đặt là chưa biết và đánh giá biểu thức đó sẽ dẫn đến gán cho biến đó. Nó hoạt động bằng cách xây dựng các cây biểu thức thành loại và sau đó sử dụng các quy tắc viết lại để chuyển đổi nó thành một cái gì đó có thể được sắp xếp cho loại không xác định.

Điều tôi cần là một số cách để xác thực quy tắc ghi lại. Chúng có thể được xác nhận bằng cách kiểm tra xác nhận cho một số quan hệ là đúng, một số khác cũng có.

Answer 1

ACL2 nổi tiếng - chúng tôi thường nói đó là một hệ thống chuyên gia, vì vậy chỉ có thể được sử dụng bởi các chuyên gia, những người đã học hỏi từ Warren Hunt, J Moore, hoặc Bob Boyer. Điều bạn cần làm trong ACL2 thực sự thực sự hiểu cách hệ thống chứng minh hoạt động; sau đó bạn có thể "gợi ý" nó theo hướng làm giảm không gian tìm kiếm.

Có một số hệ thống khác có thể trợ giúp với loại điều này, tuy nhiên, tùy thuộc vào những gì bạn đang cố gắng làm.

Nếu bạn muốn làm việc với lý thuyết toán học hoặc số liên tục, lý tưởng là Mathematica. Vấn đề là bạn có thể mua một chiếc xe đã sử dụng với số tiền tương tự (trừ khi bạn có thể đủ điều kiện để được cấp giấy phép học tập, một thỏa thuận tốt hơn nhiều.)

Điều gì đó tương tự và miễn phí là Open Maxima, là phần mở rộng của Macsyma. Trang đó cũng chỉ vào một số trang khác như Axiom, mà tôi không có kinh nghiệm.

Đối với các phép toán logic toán học, có PVS từ SRI. Họ đã có một số công cụ thú vị khác như kiểm tra mô hình trong cùng một khuôn khổ.

Answer 2

Ngoài những liên kết của Charlie Martin, bạn cũng có thể muốn xem Maple. Kinh nghiệm của tôi với phần mềm như vậy là khoảng 5 tuổi, nhưng tôi nhớ lại vào thời điểm tìm kiếm Maple trực quan hơn nhiều so với Mathematica.

Answer 3

Có nghiên cứu đang diễn ra trong lĩnh vực này, nó được gọi là "Định lý chứng minh trong đại số máy tính".

Mọi người đang cố gắng hợp nhất tính dễ sử dụng và sức mạnh của các hệ thống đại số máy tính như Mathematica, Maple, ... với độ cứng hợp lý của hệ thống chứng minh. Các sự cố là:

• Hệ thống đại số máy tính không nghiêm ngặt. Họ có xu hướng quên các điều kiện phụ như là số chia không được bằng 0.

• Hệ thống chứng minh khó sử dụng (như bạn đã khám phá).

Answer 4

Một hệ thống cũ và bỏ dở là 'Ontic':

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html

Answer 5

Vài trợ chứng minh Mỹ đã được đề cập đã (thường là với cú pháp LISP), vì vậy đây là một danh sách châu Âu làm trung tâm để bổ sung cho rằng:

• Coq

• Isabelle

• HOL4

• HOL-Light

• Mizar

Tất cả đều là những tiếng xấu cho các giao diện TTY, nhưng Coq và Isabelle cung cấp hỗ trợ tốt cho các Proof General/Emacs giao diện. Hơn nữa, Coq đi kèm với CoqIDE, được dựa trên OCaml/GTK một tiện ích văn bản trên tàu. Isabelle gần đây bao gồm IDE của Isabelle/jEdit Prover, dựa trên jEdit và được tăng cường bằng cách đánh dấu ngữ nghĩa được cung cấp bởi người chuyên nghiệp trong thời gian thực như kiểu người dùng.

Answer 6

lean prover tương tác thông qua JS gui.