The Elimination of Redundant Alg. EE Derivations That are Uniformly Non-minimal

スポンサーリンク

概要

• 論文の詳細を見る

• I have already presented, in Ref. [1], the basic part of a new method (named Alg. EE) of theorem-proving in first order predicate logic. The basic part of Alg. EE has an intimate relation with "connection method" by W.Bibel. However, in comparison with "connection method", the basic structure of Alg. EE is considered to be clearer and more general and natural as a mathematical system. Based on this clear structure, I introduce, in this report, two basic effective concepts. One of these concepts is the concept of "being uniformly non-minimal". It is a concept expressing a very general type of redundant searchings. And, I have found the method for eliminating this redundancy. The other concept is "global variant relation". Then, as the result of consideration of the structure of the combination of these two concepts, I have achieved the expansion of the range of elimination of above-mentioned redundant searchings. Further, as given in the successive report, we can introduce the reduced form of any Alg. EE derivation, as the result of this consideration.

• 一般社団法人情報処理学会の論文
• 1988-01-15

著者

• 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

スポンサーリンク