ナクトム

Nqthmはボイヤー・ムーア定理証明器とも呼ばれる定理証明器である。ACL2の前身である。^[1]

このシステムは、テキサス大学オースティン校のコンピュータサイエンスの教授であるロバート・S・ボイヤーとJ・ストロザー・ムーアによって開発されました。彼らは1971年にスコットランドのエジンバラでこのシステムの開発を始めました。彼らの目標は、完全に自動化されたロジックベースの定理証明器を作ることでした。彼らは作業ロジックとして Pure LISPの変種を使用しました。

定義は完全に再帰的な関数として形成され、システムは書き換えと、書き換えや記号評価と呼ばれるものが失敗したときに使用される 帰納的ヒューリスティックを広範に使用します。

このシステムは Lisp 上に構築されており、Common Lisp 実装上に ブートストラップした後のマシンの状態である「グラウンド ゼロ」と呼ばれる状態に関する非常に基本的な知識を持っていました。

これは簡単な算術定理の証明の例です。関数TIMESはBOOT-STRAP（「サテライト」と呼ばれる） の一部であり、次のように定義されます。

 ( DEFN TIMES ( X Y ) ( IF ( ZEROP X ) 0 ( PLUS Y ( TIMES ( SUB1 X ) Y ))))   
    
      
           

定理の定式化は Lisp のような構文でも与えられます。

 (証明補題倍数の可換性(書き換え) (等しい(倍x z ) (倍z x )))  
         

定理が正しいと証明された場合、それはシステムの知識ベースに追加され、将来の証明のための書き換え規則として使用できます。

証明自体は、準自然言語形式で示されています。著者は、数学的証明の手順を埋め込むために、典型的な数学的フレーズをランダムに選択しており、これにより、証明が実際に非常に読みやすくなります。Lisp構造を、ある程度読みやすい数学的言語に変換できる LaTeX用のマクロがあります。

時間の交換性の証明は続きます:

この予想に*1という名前を付けます。
 我々は帰納法に頼る。この予想の項から2つの帰納法が示唆される。
 どちらも欠陥がある。我々は、
 予想における非原始再帰関数の最大数。
 これらは同じくらい起こりうるので、私たちは恣意的に選びます。
 次のスキーム:
       (そして (ゼロ X) (p XZ) を意味します)
          ((AND (NOT (ZEROP X)) (p (SUB1 X) Z) を意味します)
                   (p XZ)))。
 線形演算、補題COUNT-NUMBERP、ZEROPの定義は、
 基準値（COUNT X）は、十分な根拠のある関係に従って減少することがわかります。
 LESSPは各誘導ステップで使用されます。上記の誘導スキーム
 次の2つの新しい推測が生まれます。
 ケース2. (ゼロXを意味する)
                  (等しい (XZ 倍) (ZX 倍)))。

そして、いくつかの帰納的証明を経て、最終的に次のように結論づける。

ケース 1. (IMPLEIES (AND (NOT (ZEROP Z))
                      (等しい 0 (倍 (SUB1 Z) 0)))
                 (0 (Z 0 倍)) に等しい)。
これにより、ZEROP、TIMES、PLUS、EQUAL の定義が次のように拡張され、簡素化されます。
     T.
これで *1.1 の証明は終了し、*1 の証明も終了します。
QED
[ 0.0 1.2 0.5 ]
時間の交換性

このシステムでは多くの証明が行われ、確認されているが、特に

• (1971) リスト連結
• (1973) 挿入ソート
• （1974）二進加算器
• (1976) スタックマシン用の式コンパイラ
• (1978) 素因数分解の一意性
• (1983) RSA暗号化アルゴリズムの可逆性
• (1984) Pure Lisp の停止問題の解決不可能性
• （1985）FM8501マイクロプロセッサ（ウォーレン・ハント）^[2]
• (1986) ゲーデルの不完全性定理 (シャンカール)
• (1988) CLI スタック (ビル・ベヴィエ、ウォーレン・ハント、マット・カウフマン、J・ムーア、ビル・ヤング)
• (1990) ガウスの二乗の相互法則 (デイビッド・ラッシノフ)
• (1992) ビザンチン将軍と時計の同期 (Bevier と Young)
• (1992) Nqthm言語のサブセット用のコンパイラ (Arthur Flatau)
• (1993) バイフェーズマーク非同期通信プロトコル
• (1993) Motorola MC68020 と Berkeley C 文字列ライブラリ (Yuan Yu)
• (1994)パリ・ハリントン・ラムゼー定理(ケネス・クネン)
• (1996) NFSA と DFSA の同等性 (Debora Weber-Wulff)

PC-Nqthm (Proof-checker Nqthm) と呼ばれるより強力なバージョンがMatt Kaufmannによって開発されました。これにより、システムが自動的に使用する証明ツールがユーザーに提供されるため、証明にさらに多くのガイダンスを提供できます。システムには帰納的証明の無限の連鎖をたどる非生産的な傾向があるため、これは非常に役立ちます。

• 計算論理ハンドブック、RS Boyer および J S. Moore、Academic Press (第 2 版)、1997 年。
• Boyer-Mooreの定理証明器とその対話型機能拡張、M. KaufmannおよびRS Boyerとの共著、Computers and Mathematics with Applications、29(2)、1995年、27～62頁。

2005年にロバート・S・ボイヤー、マット・カウフマン、J・ストロザー・ムーアはNqthm定理証明器の開発でACMソフトウェアシステム賞を受賞した。 ^[3]

• 自動推論システム Nqthm
• ボイヤー・ムーア定理証明器 (NQTHM)
• このシステムはサポートされなくなりましたが、[1]ではまだ利用可能です。
• GitHubで実行可能なバージョン: [2]