Recognizing unnecessary clauses in resolution based systems

DOI10.1007/BF00247826zbMATH Open0784.68073MaRDI QIDQ688549FDOQ688549

Authors: Dan Benanav 

Publication date: 10 December 1993

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

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

zbMATH Keywords

resolutionautomated theorem provingsubsumptiondeletion strategiesgeometric reasoning

Mathematics Subject Classification ID

Cited In (3)

• Preprocessing of propagation redundant clauses
• Title not available (Why is that?)
• How to avoid the derivation of redundant clauses in reasoning systems

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)