Scholarly record
SOME GENERALIZATION OF THE RESOLUTION METHOD
Abstract
If we create intelligent automated systems, decision support systems, expert systems, and in general knowledge-based systems then the development of the inference mechanism is very important. This mechanism of inference makes it possible to carry out reasoning on the available knowledge and data, to develop recommendations and decisions, to make their justifications and explanations. In this paper, a model of inference in the form of a bipartite graph is considered. The elements of the graph correspond to clauses, literals of clauses, and complement pairs of literals. This gives the initial structure for the inference procedure. The logical inference is carried out step by step. At each step, we make local changes to the graph. The inference ends positively if the graph is transformed into one vertex of the first or second type. The conclusion ends negatively if the next step cannot do. Note that we didn?t model getting of the resolvent according to the resolution principle. However, the proposed structure is able to model both the resolution method and the inverse method. Moreover, it allows you to simulate these methods not only separately. It is possible to obtain a hybrid from the step-by-step application of the methods alternately. At the same time, the resolution method received from us a considerable generalization. Getting the resolvent was made possible not only from a pair of clauses, but also from any number of clauses, for example, one or three. The proposed new mechanism of inference in its expressiveness is equal to the resolution method. It got the software implementation and showed good results.
Publication Impact Profile
Publication details
References5
J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965 12 (1): pp. 23–41.
Maslov, S. Ju. An inverse method of establishing deducibility in the classical predicate calculus. Dokl. Akad. Nauk SSSR, 159, 1964: pp. 17–20.
G. V. Davydov. A synthesis of the resolution method and the inverse method, Studies in constructive mathematics and mathematical logic. Part IV, Zap. Nauchn. Sem. LOMI, 20, Nauka, Leningrad. Otdel., Leningrad, 1971, pp. 24–35.
A. Shajkin, A. Egorov, T. Savitskaya, E. Rudakovskaya, V. Osipchik. Modeling of fuzzy reasoning in predicate logic based on Petri nets. International Multidisciplinary Scientific GeoConference Surveying Geology and Mining Ecology Management, SGEM. ISSUE 2.1 №18 - STEP92 Technology Ltd Sofia, Bulgaria, 2018: pp. 569-574.
N. K. Zamov, V. I. Sharonov. Application of isograms in the search for inference. Issledovaniya po Prikladnoi Matematike, No. 1, 1973: pp. 94–102.
View or Download full articleAccess options
SWS access login
Login as SWS Scientific CommitteeLogin as SWS Scientific PartnerLogin as SWS AuthorAuthors and approved SWS contributors will read and export their own linked papers after identity matching by SWS profile, email and SGEM GlobalID.
For librarian assistance: [email protected]
Purchase Instant Access
- Article can be downloaded after successful payment.
- Article may be used according to SWS library access terms.
- Article cannot be redistributed.
