摘要
In this paper we present a generalized resolution method by using paramodulation and prove its completeness. Using this method, the equality relation is more natural and simpler. Definition 1. An E-interpretation I of a set S of generalized clauses is an interpretation of S satisfying the following four conditions. Let α, β, and ν be any terms in the
