Prolog

面白そうな質問を見つけた。
question:1142415206

Prolog。名前しか聞いたことがない。
そういえば昔、情報処理試験に出てきてたな。

Prolog（プロローグ、プロログ）は非手続き型プログラミング言語の一つ。論理型言語に分類される。名称はProgramming in Logic の略。 1972年ごろにフランスのカルメラウアーとコワルスキーによって考案された。プログラムは一階述語論理に基づいてデータ間の関係を示す命題として記述され、処理系がそれらにパターンマッチング（ユニフィケーション）を施しながら、与えられた命題が成立するか再帰的手続きによって探索する。 人工知能におけるトップ・ダウン式の問題解決と相性が良いために、人工知能研究とエキスパートシステムの実現のための主要言語として広く採用された。

Prologのもととなる演繹手法は導出と呼ばれ、自動定理証明の研究においてProlog開発以前よりよく知られていた。Prologは、導出において節を以下に述べる頭部が一つの命題からのみなるホーン節に限定したものととらえる事が出来る。　

自動定理証明がキーワードかな。
google:自動定理証明