Basic Construction of A New Method of Theorem Proving

スポンサーリンク

概要

• 論文の詳細を見る

• I have constructed a new method (denoted by Alg.EE) for automatic theorem proving in first order predicate calculus. Alg.EE stands on the idea of Prawitz. For any given unsatisfiable set S of clauses, Alg.EE can achieve the test for S with the construction of such a set of copies of elements of S as is minimal in the sets (of copies)that are sufficiently large for the test. In Alg.EE, I have introduced an effective concept (named "uniformly non-minimal derivation") showing a large range of redundant derivations, based on a certain order relation. And, I have found a method for easy elimination of almost all of this redundancy. Further, Alg.EE achieves the test for the set S mentioned above without constructing any instance of copies of literals in S by their unifier, so that Alg.EE becomes very effective on the subject of capacity of memory and that we can prevent the occurrences of overlapping operations that occur in the step of finding unifiers. In this report, the basic theory of Alg.EE is presented.

• 一般社団法人情報処理学会の論文
• 1986-09-30

著者

• Hagiwara Y

  Iwate Univ. Morioka Jpn

• HAGIWARA YOSHIKI

  Department of Mathematics, Faculty of Engineering, Iwate University

• Hagiwara Yoshiki

  Department Of Mathematics Faculty Of Engineering Iwate University

関連論文

• Basic Construction of A New Method of Theorem Proving
• The Elimination of Redundant Alg. EE Derivations That are Uniformly Non-minimal

スポンサーリンク