Cut-Based Abduction

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 finding suitable hypotheses or lemmas. When the original sequent is provable, the abduced formula can be seen as a 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-style Tableaux.

• Type: Journal
• Year: 2008
• Where: IGPL
• Authors: Marcello D'Agostino, Marcelo Finger, Dov M. Gabbay
• Keywords: Abduction Methods, IGPL 2008, Sequent, Traditional Abduction