Maslov's inverse method and decidable classes
type: Item
instance of: scholarly article
title: Maslov's inverse method and decidable classes
zbMATH Open document ID: 0692.03009
DOI: 10.1016/0168-0072(89)90053-5
author: Nail Zamov
published in: Annals of Pure and Applied Logic
publication date: 1989-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 4132125
zbMATH Keywords: Maslov's inverse method
zbMATH Keywords: deducibility
zbMATH Keywords: resolution
zbMATH Keywords: unification
zbMATH Keywords: decidable classes
zbMATH Keywords: extension of the clash rule
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: 0168-0072(89)90053-5
OpenAlex ID: W1986341459
cites work: The Specialization of Programs by Theorem Proving
cites work: Q3905252
cites work: Q5557485
cites work: Resolution Strategies as Decision Procedures
cites work: Q5523671
cites work: The inverse method for establishing deducibility for logical calculi
cites work: Q5639373
cites work: On a bound for the complexity of terms in the resolution method
description: scientific article; zbMATH DE number 4132125