In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent X|- G, find a sentence H such that X, H|- G is provable (hypothesis generation); (ii) given a provable sequent X|-G, find a sentence H such that X|-H and the proof of X, H |-G is simpler than the proof of X|- 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.
Cut-Based Abduction
D'AGOSTINO, Marcello;
2008
Abstract
In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent X|- G, find a sentence H such that X, H|- G is provable (hypothesis generation); (ii) given a provable sequent X|-G, find a sentence H such that X|-H and the proof of X, H |-G is simpler than the proof of X|- 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.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
