A Programming System for Resolution Theorem Prover

概要

論文の詳細を見る
This paper describes a programming system for resolution theorem prover. Users can easily implement various kinds of strategies which are previously known or newly developed, therefore the system is effective in evaluations or comparisons of the strategies. High descriptive ability of the system enables users to implement complicated strategies such as the semantic resolution. The system is composed of five groups of LISP functions: (l) 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 functions in (2) or (3) , and (5) miscellaneous functions.
一般社団法人情報処理学会の論文