Demostración automática

Demostración automática

De Wikipedia, la enciclopedia libre

Las técnicas de demostración automática de teoremas consisten en aplicar métodos computacionales para demostrar teoremas. Es decir, demostración de teoremas con un ordenador. Estas técnicas son especialmente viables como herramienta para demostrar teoremas de geometría plana.

En líneas generales, el procedimiento es el siguiente:

  1. El teorema a demostrar se traduce en términos algebraicos: tanto las hipótesis como la tesis se expresan como condiciones del tipo P_i(x_1,\ldots,x_n)=0, i=1,\ldots,k y Q(x_1,\ldots,x_n)=0 respectivamente.
  2. La veracidad del teorema es entonces equivalente a que Q\, esté en el ideal generado por P_1,\ldots,P_k (lo que equivale a que la anulación de P_1,\ldots,P_k en un punto implique la anulación de Q\, en ese punto).
  3. El problema de pertenencia de un polinomio a un ideal es un problema clásico en álgebra computacional; una técnica habitual de resolución de este problema es el cálculo de una base de Gröbner adecuada.

Este método de demostración tiene el inconveniente de que la complejidad computacional del problema de pertenencia es elevada.

[editar] Ejemplo

Icono de esbozo
 El contenido de esta página es un esbozo sobre matemática. Ampliándolo ayudarás a mejorar Wikipedia.
Puedes ayudarte con las wikipedias en otras lenguas.
El contenido de esta página (o parte de ella) fue extraído de wikipedia y puede redistribuirse libremente bajo la licencia de documentación libre GNU