自動定理証明において、PhoXは拡張可能な高階論理に基づく証明支援ツールです。ユーザーはPhoXに初期目標を与え、サブ目標と証拠を通してその目標を証明します。PhoXは内部的に自然演繹木を構築します。既に証明済みの各式は、後の証明の規則となることができます。
PhoXは、もともとChristophe RaffalliによってOCaml プログラミング言語で設計・実装されました。彼は現在も、サヴォワ大学とパリ第7大学の共同開発チームを率いています。
PhoXプロジェクトの主目的は、パリ第7大学のJean-Louis Krivine氏が開発した型システムを用いて、ユーザーフレンドリーな証明チェッカーを作成することです。拡張性、効率性、表現力を維持しながら、他のシステムよりも直感的に操作できるように設計されています。他のシステムと比較して、証明構築構文は簡素化され、自然言語に近いものとなっています。その他の機能としては、GUI駆動型の証明構築、フォーマットされた出力のレンダリング、MLプログラミング言語によるプログラムの正しさの証明などがあります。
PhoXは現在、サヴォイ大学で論理学の授業に使用されています。実験段階ですが、使用可能な状態です。CeCILL 2.0でリリースされています。
外部リンク
- Phoxのウェブサイト
