Evidence Algorithm and Inference Search in First-Order Logics

摘要

In the early 1970s, in Kiev, research on automated theorem proving started in the framework of the so-called Evidence Algorithm (EA) programme, having some general features with the Mizar project and, in particular, being oriented to the development of such a technique for inference search in various first-order logics that satisfies the following requirements: the syntactic form of a problem under consideration should be preserved, logical transformations should be performed in the signature of the original theory, equality handling should be separated from deduction. For these reasons, the main efforts of the EA developers were concentrated on modifying the sequent formalism to obtain sufficient efficiency in sequent proof search, although some attention was paid to the construction of resolution-type methods. This paper contains a brief summary of the author's results in this field. It is shown that the proposed approach enables to construct (sound and complete) quantifier-rule-free sequent calculi for classical and non-classical logics, including the intuitionistic and modal cases. Besides, two sound and complete resolution-type methods based on a certain generalization of the notion of a clause are described. One of them gives the possibility to interpret Maslov's inverse method in resolution terms.