[en] In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent G, find a sentence H such that, H
G is provable (hypothesis generation); (ii) given a provable sequent G, find a sentence H such that H and the proof of , H G is simpler than the proof of G
(lemma generation). We argue that the two tasks should not be distinguished,and present a general procedure for indingsuitable hypotheses or lemmas. When the original sequent is provable, the abduced formula can be seen asa cut formula with respect to Gentzen's sequent calculus, so the abduction method is cut-based. Our method is based on the tableau-like system KE and we argue for its advantages over existing abduction methods based on traditional Smullyan-styleTableaux.
