Reference : Cut-Based Abduction
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/15880
Cut-Based Abduction
English
D'Agostino, G.-C. [> >]
Gabbay, Dov M. []
2008
Journal of Logic & Computation
Oxford University Press
16
6
537–560
Yes
0955-792X
[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.
http://hdl.handle.net/10993/15880

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
DFG09.pdfPublisher postprint301.53 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.