Loading article…
ACL2（A Computational Logic for Applicative Common Lisp）は、プログラミング言語、一階述語論理の拡張可能な理論、および自動定理証明器から構成されるソフトウェアシステムです。ACL2は、主にソフトウェアおよびハードウェアの検証を目的とした、帰納的論理理論における自動推論をサポートするように設計されています。ACL2の入力言語と実装はCommon Lispで記述されています。ACL2はフリーかつオープンソースのソフトウェアです。
ACL2プログラミング言語は、 Common Lispのアプリカティブ（副作用のない）派生言語です。ACL2は型付けされていません。ACL2の関数はすべて完全関数です。つまり、すべての関数は、ACL2ユニバース内の各オブジェクトを、そのユニバース内の別のオブジェクトにマッピングします。
ACL2の基本理論は、そのプログラミング言語と組み込み関数の意味論を公理化する。定義原理を満たすプログラミング言語内のユーザー定義は、理論の論理的一貫性を維持する形で理論を拡張する。
ACL2の定理証明器の中核は項書き換えに基づいており、この中核は拡張可能で、ユーザーが発見した定理を後続の予想に対するアドホックな証明手法として使用できます。
ACL2は、Boyer–Moore定理証明器NQTHMの「産業レベル」版となることを目指しています。この目標に向けて、ACL2は興味深い数学理論や計算理論をクリーンに設計するための多くの機能を備えています。また、ACL2はCommon Lispをベースとしているため、効率性にも優れています。例えば、帰納的検証の基礎となる仕様は、ネイティブにコンパイルして実行できます。
2005年、ACL2を含むBoyer-Mooreファミリーの証明器の著者らは、「安全性が重要なハードウェアおよびソフトウェアを検証するための形式手法ツールとして、最も効果的な定理証明器を先駆的に開発し、設計した」功績により、ACMソフトウェアシステム賞を受賞しました。 [ 2 ] [ 3 ]
ACL2は数多くの産業用途で利用されてきた。[ 4 ] [ 5 ] 1995年、J・ストローザー・ムーア、マット・カウフマン、トム・リンチは、ペンティアムFDIVバグの発覚を受けて、 AMD K5マイクロプロセッサの浮動小数点除算演算の正しさを証明するためにACL2を使用した。[ 6 ]
ACL2の産業ユーザーとしては、AMD、Arm、Centaur Technology、IBM、Intel、Oracle、Collins Aerospaceなどが挙げられる。