asistente de pruebas en lenguaje natural

Question

Me preguntaba si se ha intentado crear un asistente de pruebas que escriba en él, en inglés,

Me refiero a que escribes tu prueba de la forma habitual en TeX (quizás usando un "inglés más sencillo") y luego, en lugar de enviarla a una revista para que la verifiquen, utilizas el asistente de pruebas para que la verifiquen por ti.

Hay lenguajes de programación como inform7 en el que se programa en inglés. Creo que lo que se necesita es un conjunto de macros para convertir el texto en, digamos, algo que Coq pueda verificar. ¿Existe algo así?

¿Cree que si esto ocurre los matemáticos ocasionales lo usarán? o ¿hay problemas más profundos para que la gente no los use ahora?

Answer 1

El comprobador de pruebas CalcCheck recibe información a través de $\TeX{}$ en forma de fórmulas y acompañadas de consejos/justificaciones en inglés.

Dado el archivo de entrada, el sistema indicará que la prueba es válida en todos los pasos o indicará qué pasos están mal justificados.

Hasta donde yo sé, en la actualidad reconoce la mayoría de los teoremas de la lógica de primer orden y de la teoría de conjuntos -basado en el gran texto ``A Logical Approach to Discrete Math''.

Si no recuerdo mal, el back-end está en Haskell.

• El sitio principal del sistema está en http://calccheck.mcmaster.ca/ .
• Manual: http://calccheck.mcmaster.ca/CalcCheckDoc/

Por último, este sistema se ha utilizado en cursos de lógica de primer año para ayudar a los estudiantes a escribir pruebas. Es útil tener un sistema que compruebe las pruebas de uno cuando se tiene alguna duda.

---

Editar Lo anterior fue en 2013, ahora a partir de 2017, ahora soporta

• creación de teorías lógicas mediante módulos con nombre al estilo del lenguaje Agda
• entrada unicode directamente a través de enlaces de tipo látex
• "Completar el código de los nombres y definiciones de los teoremas
• mensajes de error coloreados y algo útiles.

Además, ahora ya no es necesario instalar el sistema como una aplicación, sino que se puede utilizar directamente a través de un navegador.

Se ha utilizado con éxito en lugar de los exámenes de papel y lápiz a nivel universitario con más de 200 estudiantes solo en el trimestre de otoño de 2017.

Por desgracia, no es de código abierto.

Answer 2

Ahora existe un programa llamado Coqatoo que convierte las pruebas de Coq en pruebas de lenguaje natural. Puede ser factible escribir un traductor que convierta estas pruebas en inglés de nuevo en Coq, pero no sé si se ha hecho ya.

También existen probadores de lenguaje natural que convierten un texto en inglés en una representación semántica formal de su significado. Por ejemplo, el Razonador ACE puede demostrar afirmaciones que están escritas en Inglés controlado por Attempto .

Answer 3

Creo que el grupo RISC (Research Institute for Symbolic Computation) del castillo de Hagenberg, en Austria, lleva muchos años trabajando en este tipo de cosas.

Véase: www.theorema.org

Basándose en los comentarios del candidato, parece que no están buscando un "probador de teoremas" automatizado, sino un "verificador de pruebas" automatizado. Si es así, ya hay un hilo sobre esto en:

¿Cómo funcionan los verificadores de pruebas?