Dovada automată ( Ing. Automated Theorem Proving, ATP , precum și Automated Deduction ) este o dovadă implementată programatic . Se bazează pe aparatul logicii matematice . Sunt folosite ideile teoriei inteligenței artificiale . Procesul de demonstrare se bazează pe logica propozițională și logica predicatelor .
Datorită indecidibilității chiar și a unor teorii destul de simple, doar proba semi -automată om-mașină are aplicație practică. În plus, după automatizarea completă, dovada se numește deja calcul . Singurul lucru care poate fi complet automat este verificarea dovezii unor teorii mai complicate (dacă este pregătită pentru asta).
În prezent, demonstrarea automată a teoremei în industrie este utilizată în principal în dezvoltarea și verificarea circuitelor integrate și a software-ului. După ce a fost descoperită eroarea de diviziune a procesoarelor Pentium , unitățile complexe cu virgulă mobilă ale microprocesoarelor moderne sunt proiectate cu grijă extremă. Noile procesoare de la AMD , Intel și altele folosesc teorema automată pentru a verifica dacă diviziunea și alte operațiuni sunt corecte.
Microsoft Corporation folosește demonstratorul automat de teoreme Z3 pentru a verifica codul sistemului de operare Windows 7 și al altor produse software [1] .