The resolution method and refutation strategies

Abstract

The article suggests a new inference control strategy to be used in the resolution method for first-order logic. This calculus is the basis of a logical model of knowledge representation, which is characterized by its high descriptive power. The notion of resolution inference used in predicate calculus is as formalised and efficient as possible. The logical model is mainly applicable to research systems, because it imposes high requirements and restrictions on the subject area. In the article, we discuss the basics of the formal theory of first-order logic and describe the existing strategies and criteria. We also suggest a new strategy and compare it with the existing ones. A distinctive feature of this strategy is that it uses ratings, which are calculated for each disjunction. The ratings take into account the ability of each disjunction to form a complementary pair to generate a resolvent. The article also describes the algorithms which implement the suggested strategy and recommends a new strategy criterion — the number of disjunctions which repeatedly participate in the generation of resolvents.