アイサプランナー

IsaPlanner ^{[1] は、対話型}証明支援ツールIsabelleの証明プランナーです。もともとは Lucas Dixon [2] がエディンバラ大学の博士論文の一部として開発し、^現在はエディンバラ大学情報学部の数学的推論グループのメンバーによって保守されています。IsaPlanner は、エディンバラで書かれた一連の証明プランナーの最新版です。以前のプランナーには Clam と LambdaClam があります。

IsaPlanner を使用すると、ユーザーはコンビネータ言語を使用して推論手法をエンコードし、定理を推測および証明できます。IsaPlanner は、推論状態、未解決の目標の記録、現在の証明計画、およびその他の重要な情報を操作することで機能します。コンビネータは、推論状態を後続の推論状態の遅延リストにマッピングする関数です。

IsaPlanner のライブラリは、分岐や反復などのタスクのためのコンビネータを提供しており、より単純な推論手法とこれらのコンビネータを組み合わせることで、強力な推論手法を作成できます。

IsaPlanner にはいくつかの推論手法があらかじめ実装されています。特に、IsaPlanner には、動的リップル、高次設定で動作可能なリップルヒューリスティック、ベスト ファーストリップル ヒューリスティック、および帰納法による証明の推論手法の実装が備わっています。

追加機能には、証明の試行を手動でステップ実行するためのインタラクティブなトレース ツールと、階層的な証明を表示および操作するためのモジュールが含まれます。

現在^{[いつ? ]}実装されている、または将来的に計画されている機能は、高階ドメインでの使用に適した証明批評の拡張セット、動的リレーショナル リプリング (関数式ではなくリレーショナル式のリプリングに適したリプリングヒューリスティック、これも高階ドメインでの使用に適しています)、および IsaPlanner と Proof General の統合です。^{[引用が必要]}

• IsaPlanner プロジェクトページ
• 数学的推論グループ