¿Qué tipo de problemas matemáticos pueden ser resueltos por los probadores de teoremas automatizados?

¿Puedo probar las siguientes afirmaciones usando los comprobadores de teoremas automatizados disponibles?

. $(a+b)^2=a^2+b^2+2ab$
Si , entonces . $11 \mid 2a-3b$ $11 \mid 7a-5b$
Si , entonces $ax^2+bx+c=0$ . $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$
Si es par, entonces es par. $a$ $4a$

¡y así!

Estoy haciendo esta pregunta porque acabo de encontrar la aplicación de los probadores de teoremas automatizados en probar teoremas en lógica.

automated-theorem-proving Math-fort
fuente

Ciertamente, puede probar todo esto (excepto quizás 3, que es incorrecto como está escrito) utilizando todos los asistentes de prueba estándar, aunque probablemente no sea automático.

Yuval Filmus

@YuvalFilmus. ¡Gracias! Entonces, ¿qué tipo de problemas se pueden resolver automáticamente?

Math-fort

Puede simplificar las expresiones automáticamente, aunque este es un servicio proporcionado por Computer Algebra Systems. No creo que los asistentes de pruebas modernos puedan probar automáticamente nada sustancial, aunque es mejor preguntar a los expertos.

Yuval Filmus

@YuvalFilmus Creo que lo que usted dice a menudo es cierto, en el sentido de que solo cuando un método de prueba automatizado da resultados interesantes, estamos dispuestos a llamarlo parte de un CAS ...

Discrete lizard

"(a + b) ^ 2 == a ^ 2 + b ^ 2 + 2ab" en WolframAlpha

Nat

Respuestas:

La mayoría de sus declaraciones son álgebra elemental, por lo que pueden probarse automáticamente mediante un sistema de álgebra computacional (CAS), como Maple o Mathematica.

(En caso de que esté interesado en las matemáticas detrás de CAS, puedo recomendar el libro Modern Computer Algebra de Joachim von zur Gathen y Jürgen Gerhard, un hermoso libro, considerado la 'biblia' del campo)

La demostración automática de teoremas tiende a ser principalmente un caso de búsqueda heurística en una estructura que representa pruebas, si la prueba no es uno de los pocos casos para los que existe un algoritmo que puede resolverlo de manera concluyente. Dado que estas declaraciones no son muy complicadas, es probable que un probador automatizado pueda 'encontrar' una prueba.

Sin embargo, creo que es interesante decir un poco más sobre las declaraciones para las que existen buenos algoritmos:

La declaración 3 es (un caso muy simple de) sobre las raíces de un (sistema de) ecuaciones polinómicas y puede resolverse encontrando una base de Gröbner con el algoritmo de Buchberger. La base de Gröbner y el algoritmo de Buchberger para encontrar uno son herramientas muy buenas para probar el teorema automatizado. Por ejemplo, ¡incluso podemos probar automáticamente teoremas elementales en geometría transformando automáticamente el problema para encontrar la raíz de una ecuación polinómica de una manera inteligente!

Otra clase interesante de teoremas son los enunciados que se pueden expresar en aritmética de Presburger sin cuantificador (en particular, este aritmético no tiene multiplicación, por lo que esto no se aplica a sus enunciados), ya que existe un algoritmo para resolver todos esos enunciados, aunque el algoritmo es un poco lento

Lagarto discreto
fuente