ACL2

ACL2

パラダイム	機能的、メタ
デザイン：	ロバート・S・ボイヤー、J・ストロザー・ムーア、マット・カウフマン
開発者	マット・カウフマンとJ・ストロザー・ムーア
初登場	1990年[1]（限定配布）、1996年 （一般配布）
安定リリース	8.6 / 2024年10月 ( 2024-10 )
タイピングの規律	動的
OS	クロスプラットフォーム
ライセンス	BSDA の
Webサイト	www.cs.utexas.edu/users/moore/acl2
影響を受けた
Common Lisp、Nqthm

ACL2 ( A Computational Logic for Applicative Common Lisp ) は、プログラミング言語、一階述語論理の拡張可能な理論、および自動定理証明器で構成されるソフトウェアシステムです。ACL2 は、主にソフトウェアとハ​​ードウェアの検証のために、帰納的論理理論の自動推論をサポートするように設計されています。ACL2 の入力言語と実装はCommon Lispで記述されています。ACL2 は無料のオープン ソース ソフトウェアです。

ACL2 プログラミング言語は、 Common Lisp の応用型(副作用のない) 版です。ACL2 は型付けされていません。すべての ACL2関数は完全です 。つまり、すべての関数は ACL2ユニバースの各オブジェクトをそのユニバース内の別のオブジェクトにマッピングします。

ACL2 の基本理論は、プログラミング言語とその組み込み関数のセマンティクスを公理化します。定義原理を満たすプログラミング言語のユーザー定義は、理論の論理的一貫性を維持する方法で理論を拡張します。

ACL2 の定理証明器のコアは項の書き換えに基づいており、このコアは、ユーザーが発見した定理を後続の推測のアドホック証明手法として使用できるという点で拡張可能です。

ACL2 は、ボイヤー・ムーア定理証明器NQTHMの「産業用」バージョンとなることを目指しています。この目標に向けて、ACL2 には、興味深い数学理論や計算理論のクリーンなエンジニアリングをサポートする多くの機能があります。また、ACL2 は Common Lisp 上に構築されていることから効率性も得られます。たとえば、帰納的検証の基礎となる同じ仕様をネイティブにコンパイルして実行できます。

2005年、ACL2を含むBoyer-Mooreファミリーの証明器の作者は、「安全性が重要なハードウェアとソフトウェアを検証するための形式手法ツールとして、最も効果的な定理証明器を開拓し、設計した」としてACMソフトウェアシステム賞を受賞した。 ^{[2] [3]}

ACL2は数多くの産業用途に利用されてきた。^{[4] [5]} 1995年、J Strother Moore、Matt Kaufmann 、Tom Lynchは、 Pentium FDIVバグを受けて、AMD K5マイクロプロセッサの浮動小数点除算演算の正しさをACL2を使用して証明した。^[6]

ACL2 の産業ユーザーには、AMD、Arm、Centaur Technology、IBM、Intel、Oracle、Collins Aerospace などがあります。

• 証明補助者のリスト

• ACL2 ウェブサイト
• ACL2s - ACL2 Sedan - Peter Dillinger と Pete Manolios によって開発された Eclipse ベースのインターフェースで、ACL2 を使用して推測を指定し、定理を証明するための自動化とサポートをユーザーに提供する強力な機能が含まれています。