¿Cómo empezar con la demostración automatizada de teoremas?

Question

Estoy interesado en esta cuestión, pero no voy a enumerar mis conocimientos/demandas sino que voy a orientarlo a un propósito más general; así que lo primero se refiere a los requisitos previos, es decir

¿Cuántos conocimientos teóricos (lógica matemática, programación y otros) hay que tener antes de dedicarse a la demostración automática de teoremas (ATP)? ¿Hay algún campo de la lógica matemática que no sea un prerrequisito necesario pero que proporcione una visión más profunda del ATP?

Una vez cumplidos los requisitos previos, sólo hay que sumergirse:

¿Cómo se empieza con la ATP? ¿Existen libros, apuntes de clase, que expliquen los conceptos cruciales? Una vez que uno ha terminado con la idea general de ATP, ¿cómo se procede a hacer ¿a qué se debe?

Sin embargo, uno podría estar preocupado (al menos esa es mi principal preocupación) por la gran cantidad de teoremas diferentes; cómo se elige, y existe la posibilidad de que si uno elige el equivocado, se quede con un conocimiento obsoleto (incluso en términos de matemáticas puras). En otras palabras

¿Hasta qué punto hay que preocuparse por el "envejecimiento" de los teóricos? ¿Existen enfoques agnósticos del lenguaje?

Answer 1

Además de las sugerencias de @dtldarek, me gustaría llamar su atención sobre

Mizar: un proyecto que pretende formalizar todas las matemáticas. Lleva en marcha desde los años 70, por lo que no es probable que desaparezca pronto. Para aprender y participar en el proyecto sólo hay que estudiar algo de lógica/teoría de la demostración básica (estándar) y ver los axiomas de la teoría de conjuntos de Tarsky-Grothendieck (teoría de conjuntos con universos). http://en.wikipedia.org/wiki/Mizar_system

El sitio espejo japonés: http://markun.cs.shinshu-u.ac.jp/mirror/mizar/

Si consigues formalizar una nueva demostración en Mizar (incluso de un teorema bien conocido), tu resultado puede ser publicado en su revista revisada por pares.

Sin embargo, si realmente te interesa el ATP, es decir, los sistemas que descubren una prueba por sí mismos (o con muy poca ayuda humana), entonces mi experiencia y sugerencia va a Theorema un proyecto desarrollado en Austria. Para utilizar Theorema es necesario utilizar el software comercial Mathematica de Wolfram Research

http://www.wolfram.com/products/

Mathematica es uno de los (2 o 3) sistemas de álgebra computacional (CAS) más potentes de la actualidad. Le recomendaría que se familiarizara con un CAS lo antes posible, básicamente por las mismas razones por las que recomendaría a un aspirante a periodista o escritor que se familiarizara con el uso de un procesador de textos. Afortunadamente las ediciones de Mathematica para estudiantes o para el hogar no son también caro (entre 100 y 300 dólares). Tenga en cuenta que estas versiones son exactamente tan potentes como la versión comercial completa

Theorema es un complemento (gratuito) de Mathematica.

La tecnología que hay detrás de Theorema es muy avanzada (por ejemplo, se puede crear una nueva notación matemática, las pruebas se generan y se explican en inglés sencillo, etc.), pero parece (al menos a mí) que el sistema no se utiliza ampliamente fuera de su propio equipo de desarrollo. No obstante, estudiarlo y utilizarlo es fascinante y merece la pena.

http://www.risc.jku.at/research/theorema/description/

El teorema se puede solicitar desde esta página:

http://www.risc.jku.at/research/theorema/software/

Answer 2

1. Nunca desarrollé un ATP, sólo hice algunas cosas relacionadas, así que una respuesta de alguien que lo hizo será infinitamente mejor. Aun así, creo que podría ayudar un poco.

2. Depende en gran medida de lo que quieras hacer con él (el teorema prover).

3. Para desarrollar algo totalmente nuevo que realmente funcione se necesitaría todo un equipo de personas con experiencia durante unos cuantos años (comparar quién hizo qué en Coq ). Este tipo de software es muy difícil de escribir y requiere mucha habilidad de programación. Aun así, no es un caso perdido: jugar a desarrollar una herramienta de este tipo puede ser un ejercicio válido, aunque sea duro.

4. No puedo ayudarte con ningún libro (aunque Google parece escupir muchas cosas relacionadas), porque yo lo aprendí por ensayo y error. Por otro lado puedo decir que aprender a usar el existente (si aún no conoces alguno) puede ser una buena idea. Para ello recomiendo Coq -- no es exactamente lo que quieres (asistente de pruebas en lugar de prover de teoremas), pero tiene una comunidad agradable y grande y (desde mi punto de vista) mucha gente lo usa/conoce, yo diría que es una especie de estándar.

5. No puedo ayudarte con el envejecimiento de los demostradores de teoremas -- no soy lo suficientemente viejo :-) Sin embargo, puedo decir cómo lidiar con el envejecimiento de los lenguajes de programación (y los demostradores de teoremas son muy parecidos a los intérpretes de lenguajes de programación especializados), cada vez hay una nueva característica que te gustaría tener, así que si alguna de las herramientas disponibles la soporta, adelante, si no - desarrolla (¿amplía una aplicación existente?) la tuya propia (o convence a alguien para que la desarrolle por ti).

Buena suerte en su empeño ;-)

Answer 3

Construí un probador de teoremas de primer orden en la universidad. Era sólo un juguete comparado con los demostradores serios, pero es un buen punto de partida. Para volver sobre mis pasos deberías:

• Confíe en su capacidad de programación
• Comprender los fundamentos de la lógica de primer orden
• Comprender el algoritmo de resolución
• Tendrá que escribir un parser para que su ATP sea utilizable (el análisis sintáctico es un gran tema, pero los combinadores de análisis sintáctico son un lugar fácil para empezar)

No subestimes el tiempo ni el esfuerzo. Pero entenderás mejor las pruebas y los fundamentos de las matemáticas.

Si no recuerdo mal, este serie de conferencias fue enormemente útil

En los años transcurridos he encontrado, Manual de lógica práctica y razonamiento automatizado y este ciclo de conferencias del autor para ser una buena referencia.

No me preocuparía por el envejecimiento de un probador de teoremas. Gran parte de los conocimientos son transferibles.

Si está interesado en la demostración de teoremas de orden superior, Agda es un buen lugar para empezar.

Answer 4

Puede que quieras jugar con

metamato

y

eprover

un poco.

El proyecto Metamath también quiere formalizar todas las matemáticas.

Este último puede responder a esta pregunta con X = socrates :

fof(all_men_are_mortal, axiom, 
    ![X]: (man(X) => mortal(X))
).

fof(socrates_is_a_man, axiom, 
    man(socrates)
).

% ----------------------------------

fof(who_is_mortal,question,
    ?[X]:mortal(X)
).

?[X]: est $\exists X$ y ![X]: est $\forall X$

También debe saber

• La competición de sistemas CADE ATP - El campeonato mundial de demostración automatizada de teoremas
• La biblioteca de problemas TPTP para la demostración automatizada de teoremas
• La biblioteca de soluciones TSTP para la demostración automatizada de teoremas

Answer 5

"¿Hasta qué punto hay que preocuparse por el "envejecimiento" de los teóricos? ¿Existen enfoques agnósticos del lenguaje?"

Por lo que veo no mucho. O al menos en ciertos casos. Digo esto por una hablar que Michael Beeson dio en Japón. Las notas de Beeson dicen:

"Esta estrategia consiste en utilizar todas las subfórmulas de la meta, o de los axiomas, o de algunos otros teoremas o sistemas de axiomas en la misma lógica, como resonadores. Esta estrategia sorprendentemente sencilla no fue descubierta en 1970, 1980, 1900 o 2003, sino en 2008. Es esta sencilla técnica la que permite que la deducción automatizada hoy en día alcanzar los niveles de poder deductivo de Meredith y Lukasiewicz. En particular, esta fue la técnica utilizada para derivar Church a partir del axioma único de Meredith en tres horas, sólo utilizando las subfórmulas del axioma único como resonadores. Las mejoras mencionadas vinieron de usar las subfórmulas de otros sistemas de axiomas conocidos como resonadores también. Cabe destacar que el cambio desde 1992 no se explica por ordenadores más rápidos o mayor memoria. Esto podría haberse hecho en 1992 si alguien hubiera pensado entonces en la estrategia de las subfórmulas. Michael Beeson Lógica y ordenadores".

En realidad, la primera frase de Beeson aquí no es correcto pero afortunadamente eso no es realmente relevante.

Además, Wos sigue utilizando OTTER, a pesar de que el autor de OTTER pasó a desarrollar también Prover9, y algunas personas afirman que Prover9 es mejor que OTTER.