Sistema interactivo de prueba de matemáticas

Question

Estoy buscando una herramienta (GUI preferida pero la CLI funcionaría) que me permite ingresar expresiones matemáticas y luego realizar manipulaciones de ellas, pero me restringe solo a operaciones matemáticamente válidas. Además, la herramienta debe poder guardar una sesión y luego demostrar que el conjunto dado de operaciones guardadas es válido.

Nota: No soy buscando un sistema para generarpruebas, solo que comprobar que los pasos que especificar manualmente son válidos.

He usado ACL2 para operaciones similares y lo hace bien en algunos casos, pero es muy difícil de usar para todo lo demás.

This little project is my motivation. Es un tipo de plantilla D que permite resolver ecuaciones. Dada esta ecuación:

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

Cualquier uno de los símbolos se puede configurar como desconocido y la evaluación de que la expresión tendrá como resultado un una asignación a esa variable. Funciona construyendo árboles de expresiones en el tipo y luego usando reglas de reescritura para convertirlo en algo que se puede eventuar para el tipo desconocido.

Lo que necesito es una forma de validar la regla de reescritura. Se pueden validar comprobando la afirmación de que dada cierta relación es verdadera, otra es también.

Answer 1

ACL2 es notorio: solíamos decir que era un sistema experto, por lo que solo podían usarlo expertos que tuvieran que aprender de Warren Hunt, J Moore o Bob Boyer. Lo que debe hacer en ACL2 es realmente entender cómo funciona el sistema de prueba; entonces puede "insinuarlo" en direcciones que reducen el espacio de búsqueda.

Existen varios otros sistemas que pueden ayudar con este tipo de cosas, sin embargo, dependiendo de lo que intente hacer.

Si desea trabajar con matemática continua o teoría de números, el ideal es Mathematica. El problema es que puedes comprar un auto usado por la misma cantidad de dinero (a menos que califiques para una licencia académica, un trato mucho mejor).

Algo similar, y gratis, es Open Maxima, que es una extensión de Macsyma. Esa página también apunta a varios otros como Axiom, con los que no tengo experiencia.

Para las operaciones de lógica matemática, hay PVS de SRI. Tienen otras cosas interesantes como la comprobación de modelos en el mismo marco.

Answer 2

Además de los enlaces de Charlie Martin, es posible que también desee consultar Maple. Mi experiencia con este tipo de software tiene alrededor de 5 años, pero recuerdo que en ese momento Maple era mucho más intuitivo que Mathematica.

Answer 3

Hay investigaciones en curso en esta área, se llama "Teorema que demuestra en álgebra de la computadora".

Las personas están tratando de combinar la facilidad de uso y el poder de los sistemas de álgebra computacional como Mathematica, Maple, ... con el rigor lógico de los sistemas de prueba. Los problemas son:

• Los sistemas de álgebra computarizada no son rigurosos. Tienden a olvidar condiciones secundarias como que un divisor no debe ser 0.

• Los sistemas de prueba son difíciles y tediosos de usar (como usted ha descubierto).

Answer 4

Un sistema viejo y sin mantenimiento es 'óntica':

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

Answer 5

Varios asistentes a prueba de estadounidenses ya se mencionaron (por lo general con la sintaxis LISP), asi que aquí hay una lista Europa centradas para complementar que:

• Coq

• Isabelle

• HOL4

• HOL-Light

• Mizar

Todos ellos son notorios para las interfaces de TTY, pero Coq e Isabelle proporcionan un buen soporte para la prueba Generales/Emacs interfaz. Además, Coq viene con CoqIDE, que se basa en OCaml/GTK y el widget de texto incorporado. La versión reciente de Isabelle incluye el IDE Isabelle/jEdit Prover, que se basa en jEdit y se complementa con el marcado semántico proporcionado por el probador en tiempo real a medida que el usuario escribe.

Answer 6

El lean prover es interactivo a través de un JS gui.