scientific article; zbMATH DE number 4041864

MaRDI QIDQ3781065zbMATH OpenFDO

Authors Maokang Wu

Publication date 1987

zbMATH Keywords

resolutionparamodulationinput refutationHorn sets containing equalityunit refutation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 991069
• scientific article; zbMATH DE number 4118335
• Nonequivalence of input paramodulation refutation and unit paramodulation refutation
• Theorem-proving with resolution and superposition
• Efficient deduction in equality Horn logic by Horn-completion

Cited in

(4)

• scientific article; zbMATH DE number 4037814 (Why is no real title available?)
• scientific article; zbMATH DE number 4089522 (Why is no real title available?)
• Nonequivalence of input paramodulation refutation and unit paramodulation refutation
• scientific article; zbMATH DE number 4118335 (Why is no real title available?)

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