Abstract
We present a method for patching faulty conjectures in automatic theorem proving. The method is based on well-known folding/unfolding deduction rules. The conjectures we are interested in here are implicative formulas that are of the following form: For Allx phi(x) = For Allx There ExistsY Gamma(x,Y) <-- Delta(x). A faulty conjecture is a statement For Allx phi(x), which is not provable in some given program T, defining all the predicates occurring in phi, i.e, M(T) does not satisfy For Allx phi(x), where M(T) means the least Herbrand model of T, but it would be if enough conditions, say P, were assumed to hold, i.e., M (T boolean OR P) satisfies For Allx phi(x) <-- P, where P is the definition of P. The missing hypothesis P is called a corrective predicate for phi. To construct P, we use the abduction mechanism that is the process of hypothesis formation. In this paper, we use the logic based approach because it is suitable for the application of deductive rules.