scientific article; zbMATH DE number 4128784

MaRDI QIDQ4207882zbMATH OpenFDO

Authors Alexander Leitsch

Publication date 1988

zbMATH Keywords

binary resolutionlifting lemmaresolution theorem provingunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On Different Concepts of Resolution
• Resolution theorem proving
• Completeness of resolution revisited
• scientific article; zbMATH DE number 8781
• scientific article; zbMATH DE number 3904558

Cited in

(7)

• Modification of the Robinson's resolution method for built-in predicates
• Understanding Resolution Proofs through Herbrand’s Theorem
• Resolution-Like Theorem Proving for High-Level Conditions
• On Different Concepts of Resolution
• scientific article; zbMATH DE number 1134678 (Why is no real title available?)
• A classification of non-liftable orders for resolution
• Formalizing Bachmair and Ganzinger's ordered resolution prover

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 Q4207882)