Алгоритм поиска вывода в классической логике предикатов.

Abstract

In this paper the authors introduce an algorithm of searching the proof in natural deduction calculus of classical predicate logic. The system of natural deduction is a Fitch-style subordinate proof Special mechanism of generating two sequences of formulae, namely, a list of formulae of the proof itself and a list of formulae-goals is the very idea of the algorithm. Due to the specifics of the searching procedures the synthetical rules that introduce logical constants are applied automatically. This fact can be interpreted as the argument against the widespread criticism of the natural deduction. The unification problem, which is the crucial point of searching for the proof in predicate logic, has found its solution in the algorithm following the famous method of using dummy variables. Terms or quasi-terms in the proof are considered as objects for the substitution instead o f the dummy variables. The authors propose the special procedure of the evaluation of the dummy variables which plays the main role in the solution of the unification problem. The implementation of the algorithm and some open problems are discussed in the conclusion.