Recognizing unnecessary clauses in resolution based systems

DOI10.1007/BF00247826MaRDI QIDQ688549zbMATH OpenFDO

Authors Dan Benanav

Publication date 10 December 1993

Published in Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

resolutionautomated theorem provingsubsumptiondeletion strategiesgeometric reasoning

Mathematics Subject Classification ID

Recommendations

• How to avoid the derivation of redundant clauses in reasoning systems
• scientific article; zbMATH DE number 7680806
• scientific article; zbMATH DE number 4164189
• scientific article; zbMATH DE number 440110
• On the termination of clause graph resolution
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• scientific article; zbMATH DE number 512974
• Elimination of self-resolving clauses
• scientific article; zbMATH DE number 1954131

Cited in

(3)

• Preprocessing of propagation redundant clauses
• How to avoid the derivation of redundant clauses in reasoning systems
• scientific article; zbMATH DE number 4164189 (Why is no real title available?)

This page was built for publication: Recognizing unnecessary clauses in resolution based systems

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