Prologによる数学上の定理証明

スポンサーリンク

概要

論文の詳細を見る
Prologをもちいて数学上の定理証明を行うには、一般につぎのような問題があることが知られている。(1)Prologでは一般の節ではなくHorn節が基礎となっている。(2)occur checkを行っていない。(3)多くのシステムでは深さ優先探索を採用しており探索の完全性をもっていない。定理証明については特に(1)の問題の解決が心要である。実際のPrologではnot述語の導入によって、この問題の制限を緩めている。Lloydはnotをもちいて一階の述語諭理式の目標をPrologの節に書き換える方法を示しているが、実際の定理証明にもちいるには十分ではない。われわれはPrologに拡張目標と呼ばれる特別な機能を付け加えて定理証明を行う方法を調べている。拡張目標をPrologで扱うには多少の制限が必要であるが、数学上の定理証明を行うには十分であると考えられる。本報告では拡張目標の定義と性質、およびPrologでの実行例を示す。
一般社団法人情報処理学会の論文
1986-10-01

著者

関連論文

もっと見る

スポンサーリンク