One modification of the ordering strategy in the resolution method

DOI10.1007/BF01097068MaRDI QIDQ1115411zbMATH OpenOpenAlexFDO

Authors Nail Zamov

Publication date 1988

Published in Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01097068

zbMATH Keywords

decision algorithmdeduction searchordering strategyresolution method

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Review text

One of the simplest deduction search strategies in the resolution method is the strategy with ordering developed by \textit{I. R. Slagle} [J. Assoc. Comput. Mach. 14, 687-697 (1967; Zbl 0157.024)] and \textit{S. Yu. Maslov} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 16, 126-136 (1969; Zbl 0206.291)]. The ordering strategy restricts the choice of the principal terms for the application of the resolution rule (the R rule). In some cases, this reduces the complexity of deductions and produces decision algorithms for some decidable classes of predicate calculus. In this note, we consider a modification of the ordering strategy and its application to the construction of a decision algorithm for one class of formulas in the predicate calculus.

Recommendations

• Application of the strategy of ordering disjunctives for a modification of the method of resolutions
• A strategy for ordering disjunctives in the resolution method
• An order-sorted resolution in theory and practice
• Strategy of defactorization in the resolution method
• scientific article; zbMATH DE number 516992
• An algorithmic approach to resolutions
• scientific article; zbMATH DE number 2085285
• Improved SOR method with orderings and direct methods
• Publication:4729409
• On paramodulation in linear strategies of the resolution method

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• scientific article; zbMATH DE number 3212023 (Why is no real title available?)
• On a bound for the complexity of terms in the resolution method

Cited in

(4)

• Decision tactics for derivation search in the resolution method
• Application of the strategy of ordering disjunctives for a modification of the method of resolutions
• On resolution strategies with weak factorization
• Soft typing for ordered resolution

This page was built for publication: One modification of the ordering strategy in the resolution method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1115411)