La prueba automática ( Eng. Automated Theorem Deving, ATP , así como la deducción automática ) es una prueba implementada mediante programación . Se basa en el aparato de la lógica matemática . Se utilizan las ideas de la teoría de la inteligencia artificial . El proceso de demostración se basa en la lógica proposicional y la lógica de predicados .
Debido a la indecidibilidad de incluso teorías bastante simples, solo la prueba semiautomática hombre-máquina tiene aplicación práctica. Además, después de la automatización completa, la prueba ya se llama cálculo . Lo único que puede ser completamente automático es comprobar la demostración de teorías más complicadas (si está preparado para ello).
En la actualidad, la demostración automática de teoremas en la industria se utiliza principalmente en el desarrollo y verificación de circuitos integrados y software. Después de que se descubrió el error de división en los procesadores Pentium , las complejas unidades de punto flotante de los microprocesadores modernos se diseñaron con extremo cuidado. Los nuevos procesadores de AMD , Intel y otros utilizan la demostración automática de teoremas para verificar que la división y otras operaciones sean correctas.
Microsoft Corporation utiliza el probador automático de teoremas Z3 para verificar el código del sistema operativo Windows 7 y otros productos de software [1] .