Loading article…
計算論理とは、計算を実行したり、計算について推論したりするために論理を用いることである。それは、数理論理学が数学と、哲学論理学が哲学と持つ関係と同様に、コンピュータ科学や工学と密接な関係にある。「コンピュータ科学における論理学」の別称とも言える。
計算論理は、論理プログラミングとも関連付けられるようになりました。これは、1970年代初頭の論理プログラミングに関する初期の研究の多くが、エジンバラ大学の計算論理学科で行われたためです。1990年代初頭には、EU基礎研究プロジェクト「Compulog」および関連する卓越ネットワークにおける論理プログラミングの拡張に関する研究を説明するために、この用語が再利用されました。基礎研究プロジェクトCompulog-IIのコーディネーターであったKrzysztof Aptは、2000年にACM Transactions on Computational Logicを創刊し、初代編集長に就任した際に、この用語を再利用し、一般化しました。
「計算論理」という用語は、2000年にACM Transactions on Computational Logicが創刊されたことで広く知られるようになりました。 [ 1 ]しかし、この用語はそれよりずっと前の1970年にJA Robinsonによって導入されました。 [ 2 ]この表現は、2番目の段落で使用されており、脚注では「計算論理」は「機械が効率的に推論を行う方法を扱う人工知能の分野にとって、『定理証明』よりも明らかに優れた表現である」と主張しています。
1972年、エジンバラ大学のメタ数学ユニットは、人工知能学部の「計算論理学科」と改名されました。[ 3 ]この用語は、 1970年代初頭に同学科で働いていたロバート・S・ボイヤーとJ・ストローザー・ムーアによって、プログラム検証と自動推論に関する彼らの研究を説明するために使用されました。彼らはまた、Computational Logic Inc.を設立しました。