Teoremlərin avtomatik sübutu (ing. Automated Theorem Proving, ATP, həmçinin Automated deduction) — isbat, proqram vasitəsilə həyata keçirilmişdir. Riyazi məntiqin aparatına əsaslanır. Süni intellekt nəzəriyyəsinin fikirlərindən istifadə olunur. İsbat prosesi təkliflərin məntiqi və predikatların məntiqinə əsaslanır.
Hətta olduqca sadə nəzəriyyələrin səbəbindən yalnız yarı avtomatik insan maşın sübutları praktik tətbiq olunur. Üstəlik, tam avtomatlaşdırıldıqdan sonra sübut hesablama adlanır. Yalnız daha mürəkkəb nəzəriyyələrin sübutunu yoxlamaq üçün tam avtomatik ola bilər (bu üçün hazırlayırsınızsa).
İstifadəsi
Hal-hazırda, sənayedəki teoremlərin avtomatik sübutu, əsasən inteqrasiya edilmiş sxemlərin və proqramların işlənməsi və yoxlanılmasında istifadə olunur. Pentium prosessorlarında bölmə xətası aşkar edildikdən sonra müasir mikroprosessorların üzən nöqtə əməliyyatlarının mürəkkəb modulları çox diqqətlə hazırlanır. AMD, Intel və digər şirkətlərin yeni prosessorları bölünmə və digər əməliyyatların düzgün aparıldığını yoxlamaq üçün teoremlərin avtomatik sübutundan istifadə edirlər.
Microsoft Windows 7 əməliyyat sisteminin kodunu və digər proqram məhsullarını yoxlamaq üçün Z3 teoreminin avtomatik sübutundan istifadə edir.
İstinadlar
- Gwen Salaün, Bernhard Schätz. Formal Methods for Industrial Critical Systems: 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings. Springer. 2011. 5. ISBN 9783642244308.
Xarici keçidlər
- Беклемишев, Лев Дмитриевич. . postnauka.ru. 20.05.2014.