¿Por qué algunos motores de inferencia necesitan asistencia humana mientras que otros no?

^{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í .}

¿Por qué los probadores de teoremas automatizados, es decir , los solucionadores de ACL2 y SMT no necesitan asistencia humana, mientras que los asistentes de pruebas, es decir, Isabelle y Coq , sí?

^{Encuentra la siguiente pregunta de la serie aquí .}

La validez de las fórmulas de orden superior en general no es decidible y los espacios de búsqueda son enormes , por lo que todo lo que puede hacer es tratar de encontrar una prueba, suponiendo que exista, enumerando hábilmente el espacio de prueba (piense en un mazo , acertadamente nombrado) Pero eso es duro. Los humanos pueden jugar el oráculo, proporcionando los lemas clave para guiar la prueba.

Los probadores automáticos, por otro lado, generalmente tratan solo con lógicas decidibles (subconjuntos de), por ejemplo, lógica proposicional o subclases de lógica de primer orden, por lo que pueden durar mucho tiempo, pero sabes que eventualmente tendrán éxito.

Tenga en cuenta que existen enfoques para permitir a los asistentes de pruebas encontrar esos lemmata importantes, por ejemplo, IsaPlanner . La herramienta adivina lemmata (inductiva) mediante enumeración y pruebas aleatorias y luego intenta probarlas. Al repetir el proceso, se pueden encontrar automáticamente muchos lemas de, por ejemplo, las definiciones típicas de tipos de datos.

ABC pequeño

• validez : una fórmula es válida, contiene lo que asigne a las variables libres.
• $\forall$$\exists$
• capacidad de decisión : una propiedad (booleana) es (Turing) decidible si hay un algoritmo que responde "sí" o "no" (correctamente) después de un período de tiempo finito.
• lógica proposicional - también lógica de orden cero ; No se permite la cuantificación.
• $\forall x. P(x)$$\forall f. f(4) > 0$
• lógica de orden superior : puede cuantificar sobre (y "construir") objetos complejos arbitrariamente, por ejemplo, funciones de orden superior (funciones que toman funciones).

Diría que la distinción clásica de "prueba de teorema automatizada" (ATP) frente a "prueba de teorema interactiva" (ITP) necesita ser reconsiderada. Si toma un sistema ITP conocido como Isabelle / HOL hoy (Isabelle2013 desde febrero de 2013), integra una gran cantidad de herramientas adicionales de la cartera ATP:

• Herramientas de prueba automatizadas genéricas a bordo: herramientas Isabelle de la vieja escuela como fasty blast(por L. Paulson) y nuevos probadores automatizados como metis(por J. Hurd).

• ATP externos para la lógica de primer orden que se invocan a través de Sledgehammer: E prover, SPASS, Vampire. La prueba que se encuentra se analiza para determinar qué lemas han contribuido a ella, reduciendo 10000 a 10 y alimentando el resultado metis.

• SMT externos con reconstrucción de prueba parcial, especialmente para Z3 (por S. Boehme).

• Herramientas para encontrar ejemplos contrarios de declaraciones no comprobadas: Nitpick / Kodkodi (J. Blanchette) y Quickcheck (L. Bulwahn).

¿Todas esas cosas automatizadas hacen que Isabelle sea un comprobador de teoremas automatizado?

En última instancia, creo que la distinción entre "ATP" y "ITP" es solo una especie de "etiqueta" que dice cómo desea posicionar o "vender" su sistema: los ATP afirman ser "herramientas de botón", pero en práctica tendrá que interactuar (indirectamente), proporcionando parámetros o sugerencias, o reformulando su problema. Eso podría ser realmente un desafío, debido a los largos tiempos de ejecución que son comunes en la comunidad ATP.

En contraste, un sistema ITP está hecho para que las personas que esperan en el lugar, con acceso medio decente a los estados de prueba internos, vean lo que falta para terminar una prueba. Un sistema ITP que envuelva las herramientas ATP a la manera de Isabelle podría resultar más atractivo para más usuarios y más aplicaciones, que ITP o ATP solo.