在計算機科學中，特別是在知識表示和推理以及金屬邏輯中，自動推理領域致力于理解推理的不同方面。對自動推理的研究有助于產生計算機程序，使計算機能夠完全或幾乎完全自動推理。盡管自動推理被認為是人工智能的一個子領域，但它也與理論計算機科學和哲學有聯系。自動推理最發達的子領域是自動定理證明（以及自動化程度較低但更務實的交互式定理證明子領域）和自動證明檢查（被視為固定假設下的保證正確推理）。

在使用歸納法和演繹法進行類比推理方面也做了大量的工作。其他重要的課題包括不確定性下的推理和非單調性推理。不確定性領域的一個重要部分是論證，在這個領域中，在更標準的自動演繹的基礎上，還應用了最小化和一致性的約束。JohnPollock的OSCAR系統是一個自動論證系統的例子，它比僅僅是一個自動定理檢驗器更具體。自動推理的工具和技術包括經典邏輯和計算法、模糊邏輯、貝葉斯推理、xxx熵推理和許多不太正式的特別技術。早年形式邏輯的發展在自動推理領域發揮了很大的作用，它本身也導致了人工智能的發展。形式證明是一種證明，其中每一個邏輯推理都被檢查到數學的基本公理。所有的中間邏輯步驟都被提供，沒有例外。