برهان النظريات الآلي
الهدف من إثبات النظريات الآلي هو توليد البراهين تلقائيًا بلغة رسمية، معطوفًا على ذلك حدسية (النظرية المستهدفة) وقاعدة معرفة من الحقائق المعروفة. تتمتع هذه التقنية بأهمية كبيرة في مجالات التحقق من صحة وأنظمة البرمجيات والأنظمة المادية، بالإضافة إلى حقول أخرى.