Loading article…
Matita [ 1 ]は、ボローニャ大学コンピュータサイエンス学科で開発中の実験的な証明支援 ツールです。これは、人間と機械の協働による形式的証明の開発を支援するツールであり、形式仕様、実行可能なアルゴリズム、および自動的に検証可能な正当性証明書が自然に共存するプログラミング環境を提供します。
Matitaは、(共)帰納的構成の計算（構成の計算の派生）として知られる依存型システムに基づいており、ある程度Rocqと互換性があります。
「matita」という言葉はイタリア語で「鉛筆」（シンプルで広く普及している編集ツール）を意味します。これは比較的小さくシンプルなアプリケーションで、[ 2 ]学生がそのアーキテクチャとソフトウェアの複雑さを習得できるように設計されており、革新的なアイデアやソリューションをテストするのに特に適したツールを提供します。 Matita はタクティクスベースの編集モードを採用しており、（XMLエンコードされた）証明オブジェクトが生成され、保存および交換されます。
Matitaでは存在変数がネイティブに実装されているため、依存目標の管理がより簡単になります。[ 3 ]
Matitaは、推論された型と期待される型の両方を利用する双方向型推論アルゴリズム[ 4 ]を実装しています。
型推論システム（リファイナー）の力は、ユーザーが指定した特定の状況でユニファイア を合成するのに役立つヒントのメカニズム[ 5 ]によってさらに強化されます。
Matitaは、パーサーと型チェッカー 間の対話に基づく高度な曖昧性解消戦略[ 6 ]をサポートしています。
対話レベルでは、システムは構造化された戦術の小さなステップ実行[ 7 ]を実装し 、証明開発のより良い管理を可能にし、より構造化され読みやすいスクリプトに自然とつながります。
Matitaは、 CerCo（Certified Complexity）という FP7欧州プロジェクトに採用されました。このプロジェクトは、 C言語の大規模なサブセットからMCS-51マイクロプロセッサのアセンブリ言語への、形式的に検証された複雑性保持コンパイラの開発に焦点を当てています。
Matitaチュートリアル[ 8 ]は、Matita対話型定理証明器の主な機能への実践的な入門を提供し、ソフトウェア仕様と検証の分野における一連の非自明な例を通してガイド付きツアーを提供します。