自動証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/11/14 16:23 UTC 版)
一方、システムの正当性の証明を自動的に生成することに関心が集まりつつある。自動化技術は2つに分類される: 自動定理証明では、何もないところから形式的証明を生成する。入力となるのはシステムの説明、論理的公理群、推論規則群である。 モデル検査では、実行時に取りうる全状態を検索し、一定の特性を照合する。 一部の自動定理証明は人間の補助なしには機能せず、追跡すべき特性を人間が指定してやる必要がある。モデル検査ではうまく抽象化されたモデルを与えないと、膨大な数の状態によって身動きが取れなくなる。 これらシステムの提唱者は、詳細に渡ってアルゴリズム的に照合が行われるため、その結果は人間による証明よりも数学的にずっと正確であると主張する。これらシステムを使うための訓練は手で証明を書くための訓練よりも簡単であり、多くの人材を生み出せるとしている。 批判的な人々は、それらシステムの「神託」的性格を問題にする。それらは真実であると宣言しているが、その詳細は説明されない。また「検査機構の検査」と呼ばれる問題もある。検証に関わるプログラム自体が検証されていない場合、その結果を疑う余地があるだろう。
※この「自動証明」の解説は、「形式手法」の解説の一部です。
「自動証明」を含む「形式手法」の記事については、「形式手法」の概要を参照ください。
ウィキペディア小見出し辞書の「自動証明」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 自動証明のページへのリンク
