自動推論
自動推論（じどうすいろん、Automated Reasoning）は計算機科学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全（あるいはほぼ完全）自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。
自動推論のなかでも最も研究が進んでいるのは、自動定理証明と自動定理検証（固定の前提条件下での推論と見なすことができる）であるが、他にもアナロジー、帰納、還元による推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証（argumentation）が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。形式的論証は人工知能の一分野である。
自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。
学術会議とワークショップ
学会と学会誌
Association for Automated Reasoning（自動推論学会）は以下の学会誌を出している。
 | この項目は、コンピュータに関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています（PJ:コンピュータ/P:コンピュータ）。 |