Otomatikleştirilmiş muhakeme

Otomatikleştirilmiş muhakeme, otomatik akıl yürütmenin farklı yönlerinin izah edilmesine odaklanmış bir bilgisayar bilimi ve matematiksel mantık alanıdır. Otomatik akıl yürütme çalışması, bilgisayarların neredeyse tamamen otomatik olarak bilgisayar programları üretmesine yardımcı olur. Otomatik akıl yürütme, yapay zekanın bir alt alanı olarak düşünülmesine rağmen, teorik bilgisayar bilimi ve hatta felsefe ile de bağlantıları vardır.

Otomatik akıl yürütmenin en gelişmiş alt alanları, otomatik teorem ispatlama ve otomatik ispatın denetlenmesidir.Benzetme indüksiyonu ile mantık yürütmede kapsamlı çalışmalar yapılmıştır.

Otomatik akıl yürütme araçları ve teknikleri olarak klasik mantıksal hesaplamalar, bulanık mantık, Bayes çıkarımı, maksimal entropi gibi konular listelenebilir.

Uygulamaları

Otomatik akıl yürütme, otomatik teorem kanıtlayıcıları oluşturmak için sıklıkla kullanılmıştır. Bununla birlikte, çoğu zaman, teorem kanıtlarının etkili olabilmesi için bazı insan rehberliğine ihtiyaç duyar ve bu yüzden daha genel olarak kanıt yardımcıları olarak nitelendirilir. Bazı durumlarda, bu kanıtlayıcılar bir teoremin kanıtlanması için yeni yaklaşımlar geliştirebilirler.Mantık Kuramcısı(Logic Theorist) bunun güzel bir örneğidir.Bu program sayesinde, Principia Mathematica'daki Whitehead ve Russell tarafından sağlanan kanıttan daha etkili olan ve daha az adım gerektiren kanıt üretmek mümkün olmuştur.Mantık, matematik ve bilgisayar bilimleri, mantık programlama, yazılım ve donanım doğrulama, devre tasarımı ve daha birçok konuda giderek artan sayıda problemi çözmek için otomatik akıl yürütme programları uygulanmaktadır.