Reference : Cut-Based Abduction
Scientific journals : Article
Engineering, computing & technology : Computer science
Cut-Based Abduction
D'Agostino, G.-C. [> >]
Gabbay, Dov M. [> >]
Journal of Logic and Computation
Oxford University Press
[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.

File(s) associated to this reference

Fulltext file(s):

Open access
DFG09.pdfPublisher postprint301.53 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.