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.
Downloads
References
2. Chen Ch., Li R. (1983) The mathematical logic and automated theorem proving. Moscow : Science.
3. Teise A. [et al.] (1990) A logical approach to artificial intelligence. T.1. From classical logic to logic programming. Moscow : Mir.
4. Baader F. (2003) The Description Logic Handbook. New York : Press of the Cambridge University.
5. Nilsson N. (1973) Artificial intelligence. Methods for finding solutions. Per. from English Stefanyuk V. L. Ed. Fomina S. V. Moscow : Mir. 272 p.
6. Maslov S. Yu. (1964) Backward method for establishing deducibility in the classical predicate calculus. SSS. Iss. 159, No 1. P. 17–20.
7. Ledeneva T. M., Aristova E. M. (2016) The formal axiomatic theories. Calculus of predicates. Part 1. Voronezh : Publishing House of the Voronezh State University.
8. Ledeneva T. M. (2020) The formal axiomatic theories. Calculus of predicates. Part 2. Voronezh : Publishing House of the Voronezh State University.
9. Pospelov D. A. (1990) Artificial intelligence. In 3 books. Book. 2. Models and Methods: Handbook. Ed. D. A. Pospelova. Moscow : Radio and communication. 304 p.
10. Novikov F. A. (2011) The systems of knowledge representation. St. Petersburg : Publishing House of the Polytechnic University.
11. Sowyer B., Foster D. (1986) Programming Expert Systems in Pascal. John Wiley & Sons, Inc. 198 p.
12. Maciol A. (2008) An application of rule based tool in attributive logic for business rules modeling // Expert Systems with Applications. April 2008. Vol. 34, No. 3. P. 1825–1836.
13. Robinson J. A. A Machine-Oriented Logic Based on the Resolution Principle // J. ACM.No 12.
14. Tyurin S. F., Gorodilov A. Yu. (2019) The features of logical inference in prolog programs // Bulletin of Perm University. Series: Mathematics. Mechanics. Computer science. No 3 (46). P. 91– 97.
15. Slagle J. (1967) Automatic theorem proving with renamable and semantic resolution // Journal of the Association for Computing Machinery. Vol. 14. P. 687–697.
16. Bratchikov I. L., Sazonova N. V. (2010) The formal-grammatical interpretation of logical inference. St. Petersburg, St. Petersburg Electrotechnical University “LETI” them. V. I. Ulyanov (Lenin). Computer tools in education, n. 6. P. 31–40.
17. Kasyanov V. N., Evstigneev V. A. (2003) The graphs in programming: processing, visualization and application. SPb. : BHV-Petersburg. 1104 p.
Условия передачи авторских прав in English
