scientific article; zbMATH DE number 1418449

MaRDI QIDQ4942004zbMATH OpenFDO

Authors Alexander Leitsch

Publication date 19 March 2001

zbMATH Keywords

automated deductiondecision problemdecision procedurehyperresolutionresolution principle

Mathematics Subject Classification ID

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

Review text

The author presents a proof-theoretic approach to the decision problem based on the resolution principle. It is the purpose of the paper to show that resolution-based theorem provers can be used not only for producing proofs for sentences but they can also be used as decision procedures. The author shows that \(A\)-ordering refinement is a decision procedure for the one-variable class and the monadic class. Most of the classical decidable classes (Maslov's Krom class, Skolem class etc.) can be decided in a similar way. Another refinement of the resolution principle is hyperresolution. The author shows that for any positively \(\alpha\)-dominated class (where \(\alpha\) is some atom complexity measure), hyperresolution is a decision procedure. For the entire collection see [Zbl 0927.00020].

Recommendations

• Resolution decision procedures
• scientific article; zbMATH DE number 19146
• An overview of resolution decision procedures
• Resolution methods for the decision problem
• scientific article; zbMATH DE number 976360

Cited in

(19)

• Decision tactics for derivation search in the resolution method
• Resolution methods for the decision problem
• Deciding the E^+-class by an a posteriori, liftable order
• Automated deduction by theory resolution
• An overview of resolution decision procedures
• Resolution theorem proving
• Resolution decision procedures
• Decision problems and recursiveness in formal logic systems
• scientific article; zbMATH DE number 4200168 (Why is no real title available?)
• scientific article; zbMATH DE number 4029278 (Why is no real title available?)
• scientific article; zbMATH DE number 4101136 (Why is no real title available?)
• scientific article; zbMATH DE number 3715502 (Why is no real title available?)
• scientific article; zbMATH DE number 8775 (Why is no real title available?)
• scientific article; zbMATH DE number 512974 (Why is no real title available?)
• scientific article; zbMATH DE number 516992 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• Principles and Practice of Constraint Programming – CP 2003
• Defining answer classes using resolution refutation
• From decision problems to dethroned dictators

This page was built for publication:

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