01 / UNDERSTAND
仕組みと使いどころ
証明検証器は、形式的に記述された証明を検査するソフトウェアである。HOL Lightは対話型定理証明器兼証明検証器として公開されている。CarcaraはAlethe形式のSMT証明を対象とし、証明ファイルと元のSMT-LIB問題ファイルを受け取って検査する。Isabelle向けには、証明項を検査する実行可能な検証器が形式化され、そのメタ論理に対する正しさが証明されている。対象となる論理体系や入力形式は検証器ごとに異なる。
02 / IN PRACTICE
Proof Checkerの活用例
たとえば、こんな場面で
Alethe形式のSMT証明をCarcaraで検査する場合、証明ファイルと対応する元のSMT-LIB問題ファイルをcheckコマンドへ渡す。
03 / GOOD TO KNOW
使うときのポイント
利用する検証器が対応する論理体系、証明形式、必要な付随ファイルを事前に確認する。
参考資料
GitHub - jrh13/hol-light: The HOL Light theorem prover （新しいタブで開きます）GitHub - ufmg-smite/carcara （新しいタブで開きます）Isabelle's Metalogic: Formalization and Proof Checker （新しいタブで開きます）用語の説明や活用例に関連する参考資料です。
READ & LEARN
記事一覧を見る 用語を知ったら、活用を知る。
AI LABで、AIの動向や業務に取り入れるヒントを読む。