07/06/22 11:53:27
>>593
コンピューターによる定理の自動証明
ｽﾚﾘﾝｸ(math板)l50
「Mizar」ミザール、プルーフチェッカーの一種
数学は非常に多分野に及んでおり
ひとつの専門分野が違うと、その分野の把握は困難ではある。
（また私たち人間も活動的な年齢や寿命もある）
これらの検索（というものか？）
人間ではなく、コンピュータにさせる方法。
言うまでもなくコンピュータは、人間以上に、早く正確に情報（データ）を
蓄積・検索してくれるし、これらのデーターベースは
後世の後輩たちにも（比較的容易に）引き継げるメリットをもつ。
似たような例で、将棋の棋譜をデーターベース化にし
同局面が存在したかを、過去の棋譜（局面）を参考に短時間で検索してくれるシステムがある。
（おそらくプロ棋士が（コンピュータを使わず自分の頭で）検索しても時間はかかるであろうし
それなのに、そうでない普通の人間がやれば膨大な時間がかかるであろう。）