Teoremlerinin Otomatik Kanıtı ( DAT ) aktivitesidir yazılım gösteren bir önermeyi kullanıcı yardımı olmadan kendisine sunulan edilir.
Otomatik teorem kanıtlayıcıları, kurulması zor olan ilginç varsayımları çözdü, bunlardan bazıları matematikçilerden uzun süredir kaçtı; bu durum, örneğin, 1996 yılında EQP yazılımıyla gösterilen Robbins (in) varsayımıdır . Bununla birlikte, bu başarılar düzensizdir ve gösterilecek teoremlerin çok özel bir formunu varsayar; örneğin, Robbins varsayımı durumunda, bu bir eşitlik teoremidir, yani ifadesi esas olarak gösterilecek kimlikleri içeren bir teoremdir .
Otomatik göstericilerle ilgili daha basit bir sorun, kendilerine sunulan gösterilerin geçerli olmasını sağlayan gösteri doğrulayıcılarının sorunudur.
Gösteri asistanlar (veya geçirmez asistanlar) çözeltisine giden adımları vermek için bir insanın müdahalesini gerektirir. Otomasyonun derecesine bağlı olarak, kanıt asistanı, kullanıcının resmi nesneler olarak kendisine sağladığı gösterilerin doğrulayıcısına veya önemli adımları otomatik olarak yaratan kişiye indirgenebilir.
Model kontrolünü (İngilizce model kontrolü ) kullanan ifadelerin doğruluğunun karma sistem doğrulaması da vardır . Belirli bir teoremi kanıtlamak için özel olarak yazılmış programlar da vardır.
Belirli bir ispat sisteminde belirli bir ifade için bir ispatın minimum uzunluğunun değerlendirilmesi problemi , ispatların karmaşıklığı içinde incelenir .
Otomatik teorem göstericiler ticari olarak esas olarak entegre devrelerin tasarımında ve doğrulanmasında kullanılır. Yana Pentium işlemci FDIV hata sorunu daha dikkatli olmuştur etmek tasarımında mikroişlemci hesaplama birimi yüzen . İçinde Şubat 2011 , AMD, Intel ve diğerleri, işlemcilerinde bölme ve diğer işlemlerin doğru şekilde uygulandığını doğrulamak için otomatik teorem kanıtlayıcılar kullanır.