What is the inverse method? (Q908895): Difference between revisions

The inverse method is a method of theorem proving in predicate calculus, invented by S. Maslov in 1964. It uses a special normal form of the formula, unification and search for contradiction much like the resolution method. The derivable objects, superclauses, are disjunctions of conjunctions. There are two derivation rules, A) generating tautologies from unifiable parts of the formula, and B), close to clash- resolution: \[ \frac{A_ 1\vee D_ 1,...,A_ n\vee D_ n}{sD_ 1\vee...\vee sD_ n}s\quad =\quad MGU(A_ 1,...,A_ n). \] The difference between the presented view of the inverse method and the traditional view is explained. The difference would, however, be substantial, if ordinary clause form, not the form with superclauses were used. The inverse method is also treated in a paper by \textit{N. K. Zamov} [Ann. Pure Appl. Logic 42, No.2, 165-194 (1989; Zbl 0692.03009)].