What is the inverse method?
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)].
- On linear logic planning and concurrency
- Connection methods in linear logic and proof nets construction
- Theorem prover for intuitionistic logic based on the inverse method
- Why does the complete iterative inversion method work so well?
- The inverse method
- Evidence algorithm and inference search in first-order logics
- To Vladimir Lifschitz on His 65th Birthday
- What is invexity?
- scientific article; zbMATH DE number 4047178 (Why is no real title available?)
- Lemma matching for a PTTP-based top-down theorem prover
- Maslov's inverse method and decidable classes
- Who Invented the Delta Method?
- On the complexity of Maslov's class K
This page was built for publication: What is the inverse method?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q908895)
