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

resolution methoddecision algorithmordering strategydeduction search

Mathematics Subject Classification ID

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

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

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

Cited in

(4)

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

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)