Automatický důkaz ( angl. Automated Theorem Proving, ATP , stejně jako Automated deduction ) je důkaz implementovaný programově . Je založen na aparátu matematické logiky . Jsou použity myšlenky teorie umělé inteligence . Proces důkazu je založen na výrokové logice a predikátové logice .
Vzhledem k nerozhodnutelnosti i docela jednoduchých teorií má praktické použití pouze poloautomatický důkaz člověk-stroj. Navíc po plné automatizaci se důkaz již nazývá výpočet . Jediné, co může být zcela automatické, je kontrola důkazů složitějších teorií (pokud je na to připravena).
V současné době se automatické dokazování teorémů v průmyslu využívá především při vývoji a ověřování integrovaných obvodů a softwaru. Poté, co byla objevena chyba dělení v procesorech Pentium , jsou komplexní jednotky moderních mikroprocesorů s pohyblivou řádovou čárkou navrhovány s extrémní péčí. Nové procesory od AMD , Intelu a dalších používají automatické dokazování teorémů ke kontrole správnosti dělení a dalších operací.
Společnost Microsoft Corporation používá automatický dokaz věty Z3 k ověření kódu operačního systému Windows 7 a dalších softwarových produktů [1] .