An overview of resolution decision procedures

MaRDI QIDQ2702565zbMATH OpenFDO

Authors Hans de Nivelle

Publication date 12 March 2001

zbMATH Keywords

decidable subclasses of first-order logicdecision proceduresresolution

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1418449
• scientific article; zbMATH DE number 512974
• Resolution decision procedures
• scientific article; zbMATH DE number 19146
• Resolution methods for the decision problem

Cited in

(11)

• Deciding H₁ by resolution
• Resolution methods for the decision problem
• SCL clause learning from simple models
• scientific article; zbMATH DE number 1614714 (Why is no real title available?)
• Resolution decision procedures
• scientific article; zbMATH DE number 4200168 (Why is no real title available?)
• scientific article; zbMATH DE number 4114095 (Why is no real title available?)
• Completeness and decidability results for first-order clauses with indices
• scientific article; zbMATH DE number 1418449 (Why is no real title available?)
• Computer Aided Verification
• First-order temporal verification in practice

This page was built for publication: An overview of resolution decision procedures

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