自動定理証明

自動定理証明

数学の命題を入力して、その命題が真であれば証明を出力し、偽であればそのことを示す

歴史

1920年代

数学的な課題の証明を、手順的な方法で得ることができるかどうかという研究が一定の成果を見せ始めていた

1950年代以降

コンピュータが実用化した,実際に定理を証明する自動定理証明システムの研究が始まった

1984年には SYSTEM5 (匿名の数学者の連名)により、 CLC という論理体系が定義され、当時のパソコンでも動作する自動証明定理プログラムが作成された。

1990年代

簡単な非論理公理と論理公理からなる体系であれば、真の命題の証明を得ることができるようになった

当初,自動定理証明システムは,単なる数学の定理の証明に過ぎなかった。

2000年代

信号システムに代表される「プログラムが正しく動くのかを客観的に証明する検証」に用いられるようになり、実用的なシステムとして発展した