Recognizing Unnecessary Inference

Intelligent reasoners sometimes draw conclusions that lack new or relevant information. Similarly, automated reasoning systems can produce formulas that are not necessary for the problem at hand. We concentrate on the problem of unnecessary inference in the context of resolution based systems. In such systems several strategies have been developed that allow for the deletion of clauses without sacrificing completeness. Unfortunately these strategies fail to recognize other frequently generated unnecessary formulas. We will present a generalized subsumption theorem that can be used to recognize such formulas and to develop new deletion methods which retain completeness. 1 I n t r o d u c t i o n Intelligent reasoners expend much effort deciding what information is necessary for the problem at hand. When a conclusion is drawn we decide if it contains new and relevant information. It is well known that the performance of automated reasoning systems can be enhanced by eliminating unnecess...

• Type: Conference
• Year: 1989
• Where: IJCAI
• Authors: Dan Benanav
• Keywords: IJCAI 1989, IJCAI 2007, Resolution Based Systems, Unnecessary Formulas, Unnecessary Inference