Demostración automática de teoremas

Estas técnicas son especialmente viables como herramienta para demostrar teoremas de geometría plana.A pesar de estos límites teóricos, los demostradores prácticos del teorema pueden solucionar muchos problemas difíciles con estas lógicas.Para poder hacer esto, se requiere generalmente que cada paso individual de la demostración pueda ser verificado por una función recurrente primitiva o programa, y por lo tanto el problema es siempre decidible.Los demostradores interactivos se utilizan para numerosas tareas, en algunos casos sistemas completamente automáticos han logrado demostrar una cantidad de teoremas interesantes y difíciles, incluyendo algunos que han eludido a los matemáticos humanos durante mucho tiempo.Otro ejemplo es la demostración que en el juego de Unir Cuatro gana el primer jugador.Más precisamente en una teoría de los enteros, la inducción matemática no puede ser capturada por una lista finita de axiomas, aunque si es posible lograrlo mediante un esquema infinito de axiomas (por cada fórmula en el lenguaje se puede agregar un axioma que exprese que la inducción funciona para esa fórmula).Sin embargo, una teoría de primer orden que admite conjuntos como objetos básicos, es decir, ZFC, puede expresar la inducción sin mayores inconvenientes. Por lo tanto no debe ser confundida con una teoría de primer orden de las metamatemáticas, ya que los cuantificadores han sido eliminados, si bien es posible emular a los cuantificadores universales reescribiéndolos como variables libres.