Формально-графическая интерпретация логического вывода

Abstract

In this paper restricting (reducing search) strategies for resolution algorithms of logical inference in knowledge bases formed in terms of logical model of knowledge are considered. Peculiarity of these strategies is preliminary adjustment to a concrete knowledge bases. For the adjustment an abstraction and formal-grammar interpretation of the deduction problem is used. An abstraction is a function that maps certain class of problems K1 onto a simpler class K2. In order to solve a problem A  K1 it is mapped onto a problem B  K2. Then B is solved and its solutions are used for searching solutions of the initial problem A. In the paper class K1 is the deduction problem in the first-order predicate calculus. Two abstractions are considered for K1. The first one is propositional abstraction in which K2 is the deduction problem in the propositional calculus. In the second one the deduction problem is solved for structures named pseudo-predicates. For both abstractions formal-grammar interpretations are proposed that allow to fulfill the preliminary adjustment which guarantees searching only successful variants of inference . Given examples illustrate virtues of suggested methods.