ミニログ

MINLOGはミュンヘン大学のヘルムート・シュヴィッテンベルクのチームによって開発された証明支援システムである。^{[1] [2]}

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

参考文献

1. Wiesnet, Franziskus (2018年4月25日). 「Minlog入門」 .証明と計算. WORLD SCIENTIFIC: 233–288 . doi :10.1142/9789813270947_0008. ISBN 978-981-327-093-0. 2025年2月15日閲覧。
2. "数学ロジック - www.minlog-system.de". www.mathematik.uni-muenchen.de。ルートヴィヒ・マクシミリアン大学ミュンヘン。2025 年2 月 15 日に取得。

外部リンク

• MINLOGホームページ