Az automatikus bizonyítás ( ang. Automated Theorem Proving, ATP , valamint az Automated Deduction ) egy programozottan megvalósított bizonyítás . A matematikai logika apparátusán alapul . A mesterséges intelligencia elmélet ötleteit használják fel . A bizonyítási folyamat kijelentéslogikán és predikátumlogikán alapul .
A meglehetősen egyszerű elméletek eldönthetetlensége miatt csak a félautomata ember-gép bizonyításnak van gyakorlati alkalmazása. Ráadásul a teljes automatizálás után a bizonyítást már számításnak nevezik . Az egyetlen dolog, ami teljesen automatikus lehet, az a bonyolultabb elméletek bizonyításának ellenőrzése (ha erre felkészült).
Jelenleg az iparban az automatikus tételbizonyítást főként integrált áramkörök és szoftverek fejlesztése és ellenőrzése során alkalmazzák. A Pentium processzorok felosztási hibájának felfedezése után a modern mikroprocesszorok összetett lebegőpontos egységeit rendkívüli gondossággal tervezték. Az AMD , az Intel és mások új processzorai automatikus tételt használnak az osztás és egyéb műveletek helyességének ellenőrzésére.
A Microsoft Corporation a Z3 automatikus tételbizonyítót használja a Windows 7 operációs rendszer és más szoftvertermékek kódjának ellenőrzésére [1] .