Teoremlərin avtomatik sübutu

Vikipediya, azad ensiklopediya
Naviqasiyaya keçin Axtarışa keçin

Teoremlərin avtomatik sübutu (ing. Automated Theorem Proving, ATP, həmçinin Automated deduction) — isbat, proqram vasitəsi ilə 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 həllolunmazlığı 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[redaktə | mənbəni redaktə et]

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[1].

İstinadlar[redaktə | mənbəni redaktə et]

  1. 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[redaktə | mənbəni redaktə et]