フォックス

自動定理証明において、PhoX は拡張可能な高階論理に基づく証明アシスタントです。ユーザーは PhoX に初期目標を与え、サブ目標と証拠を通してその目標を証明します。内部的には、自然演繹ツリーが構築されます。以前に証明された各式は、後の証明のルールになることができます。

PhoX はもともと Christophe Raffalli によってOCaml プログラミング言語で設計および実装されました。彼は、サヴォワ大学とパリ第 7 大学の共同作業である現在の開発チームを引き続き率いています。

PhoX プロジェクトの主な目的は、パリ第 7 大学の Jean-Louis Krivine が開発した型システムを使用して、ユーザーフレンドリーな証明チェッカーを作成することです。このシステムは、拡張性、効率性、表現力を維持しながら、他のシステムよりも直感的であることを目指しています。他のシステムと比較して、証明構築構文は簡素化され、自然言語に近いものになっています。その他の機能には、GUI 駆動型の証明構築、フォーマットされた出力のレンダリング、MLプログラミング言語でのプログラムの正しさの証明などがあります。

PhoXは現在、サヴォイ大学で論理学を教えるために使用されています。実験段階ですが、使用可能な状態です。CeCILL 2.0 でリリースされています。

• Phoxのウェブサイト