A method is proposed which allows to abduce the definition of a predicate G during the proof attempt of a (faulty) conjecture H(x) such tha A x. G(x) ->H(x) holds by construciton. It is demonstrated how the synthesized predicate may help to complete an induction proof if the faulty conjecture has been obtained as an (over-) generalization ofa true conjecture H'(x). An equivalence preserving transformation of predicates is presented which in some cases allows to unblock induction proofs which fail otherwise.
展开▼
