Tipos de demostradores de teoremas automatizados

20

Estoy aprendiendo la prueba de teorema automatizado / solucionadores SMT / asistentes de prueba por mi cuenta y publico una serie de preguntas sobre el proceso, comenzando aquí .

¿Cuáles son los probadores de teoremas automatizados relevantes? Encontré una revisión de los probadores de teoremas

¿Sigue siendo actual?

¿Cuáles están todavía muy activas, es decir, cuáles se usan actualmente más allá del grupo que lo creó?

Encuentra la siguiente pregunta de la serie aquí .

Guy Coder
fuente

Respuestas:

15

La categorización en esa lista ciertamente sigue vigente.

Quizás haya surgido una nueva categoría, a saber, los lenguajes de programación de tipo dependiente . Estos son esencialmente demostradores de teoremas automatizados donde el objetivo principal no es probar los teoremas, sino programar. Debido a la correspondencia de Curry-Howard , estos dos conceptos están fuertemente entrelazados. El objetivo final de dichos lenguajes de programación es escribir programas que tengan garantías mucho más fuertes que los lenguajes de programación mecanografiados regulares. La gente también los usa para probar teoremas. Algunos sistemas nuevos que entran en esta categoría incluyen Agda y Epigram. Una de las características clave de tales lenguajes es que hacen un gran esfuerzo para facilitar a los programadores definir familias inductivas de tipos de datos. Un ejemplo simple es un vector, que depende de números naturales (definidos inductivamente).

En cuanto a cuáles todavía están muy activos, creo que todos lo están. Coq , Isabelle , Twelf y PVS se usan mucho en la comunidad de lenguajes de programación. Maude se usa ampliamente en sistemas de modelado. (Personalmente, he usado Coq y Maude ).

Nunca había oído hablar de algunos de ellos. En el pdf al que se vincula, hay vínculos a los demostradores de teoremas. Algunos enlaces son actuales, algunos están rotos. Gandalf ahora parece ser una especie de mago barbudo.

Los demostradores de teoremas mencionados en "Una revisión de los demostradores de teoremas" son:

  • ALF : subsumido por ALFA, Coq y Agda.
  • ALFA : parece que ya no es compatible.
  • COQ : apoyado activamente.
  • MetaPRL : parece que ya no es compatible.
  • NuPRL : apoyado activamente.
  • HOL : activamente apoyado.
  • PVS : apoyado activamente.
  • Isabelle : apoyada activamente.
  • DOCE : apoyado activamente.
  • ACL2 : apoyado activamente.
  • INKA : parece que ya no es compatible.
  • GANDALF : parece que ya no es compatible.
  • TPS : aún puede estar activo, pero solo tiene un pequeño seguimiento.
  • Nutria : puede que ya no sea compatible.
  • SETHEO : reemplazado por E-SETHEO, que parece que ya no es compatible.
  • SPASS : parece estar todavía activo.
  • EQP : parece que ya no es compatible.
  • MAUDE : muy activamente apoyado.
  • OMEGA : parece que ya no es compatible.
  • Mizar : activamente apoyado.

Indudablemente, hay muchos nuevos probadores de teoremas automatizados que no se han mencionado en esta lista.

Para completar, como lo sugiere Raphael , hay pruebas de archivo del sitio realizadas con diversas herramientas. Por ejemplo:

Dave Clarke
fuente
2
Probablemente sea útil vincular a (listas de) pruebas donde se han utilizado las herramientas respectivas, por ejemplo, Archivo de pruebas formales para Isabelle.
Raphael
@GuyCoder: Por alguna razón, se eliminaron sus adiciones. Los agregué nuevamente.
Dave Clarke
"Algunos sistemas nuevos que entran en esta categoría incluyen Agda y Epigram". Parece desaparecido. ¿Hay una nueva ubicación para Eprigram? O una alternativa cercana?
Hibou57
1
“En cuanto a cuáles todavía están muy activos, creo que todos lo están. Coq, Isabelle, Twelf y PVS ”: se sabe que PVS tiene errores de solidez. A diferencia de Isabelle y Coq, PVS no sigue la arquitectura de micro-kernel. Busque el criterio de De Bruijn para saber por qué es importante.
Hibou57
1
Junto con Agda y (¿desaparecido?) Epigram, está el lenguaje de programación ATS , que según su lista de correo, parece estar activo hasta ahora en 2014.
Hibou57