定理の自動証明のためのプログラミングシステムの構成

概要

論文の詳細を見る
Many strategies have been proposed for the resolution theorem provers. And there is a need for utilizing these various kind of strategies in practical theorem proving programs, because the effectiveness of each strategy depends on the charactor of a problem. This paper presents a programming system which satisfies the need. The system is composed of five groups of LISP functions, those are (1) extracting a pair of clauses from lists of clauses, (2) handling a list of clauses, (3) executing resolution, factoring etc., (4) subsidiary functions which are used together with (2),or (3) functions ,and (5) miscellaneous functions. Using this system, users can easily implement a large number of known strategies, and can also evaluate the effectiveness of a new strategy . Another feature of this system is that it is designed in consideration of the extensibility to an interactive system.
一般社団法人情報処理学会の論文
1976-05-15