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:
- El teorema a demostrar se traduce en términos algebraicos: tanto las hipótesis como la tesis se expresan como condiciones del tipo
y 
respectivamente. - La veracidad del teorema es entonces equivalente a que
esté en el ideal generado por 
(lo que equivale a que la anulación de en un punto implique la anulación de en ese punto). - 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
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.
