Loading article…
MINLOGは、ヘルムート・シュヴィヒテンベルクのチームによってミュンヘン大学で開発された証明支援システムです。[ 1 ] [ 2 ]
MINLOGは、一階自然演繹計算に基づいています。古典論理や直観主義論理ではなく、最小論理を用いて計算可能な関数について推論することを目的としています。MINLOGの主な動機は、プログラム開発とプログラム検証のために、証明をプログラムとして扱うパラダイムを活用することです。実際、証明は正規化可能な第一級オブジェクトとして扱われます。式が存在する場合、その証明は、その式のインスタンスを読み出すために使用したり、証明変換によってプログラム開発用に適切に変更したりできます。この目的のために、MINLOGには、証明項から関数型プログラムを直接抽出するツールが備わっています。これは、洗練されたA変換を用いて、非構成的証明にも適用されます。このシステムは、効率的な項書き換え装置として、自動証明検索と評価による正規化によってサポートされています。