Automatiskt bevis ( Eng. Automated Theorem Proving, ATP , såväl som Automated deduction ) är ett bevis som implementeras programmatiskt . Den är baserad på den matematiska logikens apparatur . Idéerna från artificiell intelligensteorin används . Bevisprocessen är baserad på propositionell logik och predikatlogik .
På grund av oavgörbarheten hos till och med ganska enkla teorier, har endast halvautomatiska bevis av människa-maskin praktisk tillämpning. Dessutom, efter full automatisering, kallas beviset redan beräkning . Det enda som kan vara helt automatiskt är att kontrollera bevisen för mer komplicerade teorier (om den är förberedd för detta).
För närvarande används automatisk teoremprovning inom industrin främst vid utveckling och verifiering av integrerade kretsar och mjukvara. Efter att uppdelningsfelet i Pentium-processorer upptäcktes är de komplexa flyttalsenheterna i moderna mikroprocessorer designade med extrem omsorg. Nya processorer från AMD , Intel och andra använder automatiska teorem för att kontrollera att division och andra operationer är korrekta.
Microsoft Corporation använder Z3 automatiska teoremprover för att verifiera koden för operativsystemet Windows 7 och andra mjukvaruprodukter [1] .