Automaattinen todistus ( eng. Automated Theorem Proving, ATP , sekä Automated Deduction ) on ohjelmallisesti toteutettu todistus . Se perustuu matemaattisen logiikan laitteistoon . Tekoälyteorian ideoita käytetään . Todistusprosessi perustuu propositionaaliseen logiikkaan ja predikaattilogiikkaan .
Jopa melko yksinkertaisten teorioiden päättämättömyydestä johtuen vain puoliautomaattisella ihminen- konetodistuksella on käytännön sovellus. Lisäksi täyden automatisoinnin jälkeen todistusta kutsutaan jo laskennaksi . Ainoa asia, joka voi olla täysin automaattista, on monimutkaisempien teorioiden todisteiden tarkistaminen (jos se on valmis tähän).
Tällä hetkellä teollisuudessa automaattista lausetodistusta käytetään pääasiassa integroitujen piirien ja ohjelmistojen kehittämisessä ja verifioinnissa. Sen jälkeen kun Pentium-prosessorien jakovirhe havaittiin , nykyaikaisten mikroprosessorien monimutkaiset liukulukuyksiköt on suunniteltu erittäin huolellisesti. Uudet AMD :n , Intelin ja muiden prosessorit käyttävät automaattista lausetta, joka todistaa, että jako- ja muut toiminnot ovat oikein.
Microsoft Corporation käyttää Z3-lauseiden automaattista todistajaa Windows 7 -käyttöjärjestelmän ja muiden ohjelmistotuotteiden koodin tarkistamiseen [1] .