Automatisk bevis ( Eng. Automated Theorem Proving, ATP , samt Automated deduction ) er et bevis implementeret programmatisk . Den er baseret på matematisk logiks apparat . Idéerne om kunstig intelligensteori bruges . Bevisprocessen er baseret på propositionel logik og prædikatlogik .
På grund af uafgøreligheden af selv ret simple teorier, er det kun semi -automatisk menneske-maskine-bevis, der har praktisk anvendelse. Derudover kaldes beviset efter fuld automatisering allerede beregning . Det eneste, der kan være helt automatisk, er at kontrollere beviset for mere komplicerede teorier (hvis det er forberedt på dette).
På nuværende tidspunkt bruges automatisk teorembeviselse i industrien hovedsageligt i udvikling og verifikation af integrerede kredsløb og software. Efter at divisionsfejlen i Pentium-processorer blev opdaget , er de komplekse flydende komma-enheder i moderne mikroprocessorer designet med ekstrem omhu. Nye processorer fra AMD , Intel og andre bruger automatisk teorem, der beviser for at kontrollere, at division og andre operationer er korrekte.
Microsoft Corporation bruger Z3 automatisk sætningsbeviser til at verificere koden for Windows 7-operativsystemet og andre softwareprodukter [1] .