Maslov's inverse method and decidable classes (Q583187)

Maslov's inverse method for establishing deducibility in predicate logic proposed at the same time as resolution [\textit{S. Yu. Maslov}, Dokl. Akad. Nauk SSSR 159, 17-20 (1964; Zbl 0146.246)] has the same distinguishing features: use of unification and local character of deduction. It is inverse relative to the bottom-up search in Gentzen-type calculus, and so would be called ``direct'' by most researchers now. Maslov established its equivalence to resolution not only up to derivability of clauses, but also with respect to the structure of derivation. Computer programs based on the inverse method competed successfully with reslution-based programs in the early seventies. The main theoretical use of the inverse method was a unified treatment of the decidable cases of predicate logic. Maslov defined a class K containing most of the familiar decidable classes (Ackermann's, Gödel's etc.) and gave bounds for the number of inferences which should produce either a derivation or at least an essential simplification of any derivable formula belonging to the class K. The paper under review contains a new self-contained proof of the decidability of K by the inverse method. This method is reformulated here in modern terms as an apparatus for deriving clauses by means of a resolution-type rule, more precisely by an extension of the clash rule. The decision is provided by a special strategy for this rule determined by a special ordering of literals in the original formula. The derivation according to this strategy preserves a characteristic property of the class K, which is roughly speaking the existence of a maximal literal in each clause ``covering'' all other literals. Only finitely many clauses with this property can be generated during the proof search, and so it is bound to terminate.