In this paper we explore a generalization of traditional abduction which as simultaneously perform two different tasks: (i) given an unprovable sequent Gamma proves G, find a sentence II such that Gamma, II proves G is provable (hypothesis generation); (ii) given a provable sequent Gamma proves G, find a sentence II such that Gamma proves II and the proof of Gamma, II proves G is simpler than the proof of Gamma proves 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 tablean-like system KE and we argue for its advantages over existing adduction methods based on traditional Smullyan-style Tableaux.

Cut-based abduction / M. D'Agostino, M. Finger, D. Gabbay. - In: LOGIC JOURNAL OF THE IGPL. - ISSN 1367-0751. - 16:6(2008), pp. 537-560.

Cut-based abduction

M. D'Agostino;
2008

Abstract

In this paper we explore a generalization of traditional abduction which as simultaneously perform two different tasks: (i) given an unprovable sequent Gamma proves G, find a sentence II such that Gamma, II proves G is provable (hypothesis generation); (ii) given a provable sequent Gamma proves G, find a sentence II such that Gamma proves II and the proof of Gamma, II proves G is simpler than the proof of Gamma proves 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 tablean-like system KE and we argue for its advantages over existing adduction methods based on traditional Smullyan-style Tableaux.
Abduction; cut rule; KE method
Settore M-FIL/02 - Logica e Filosofia della Scienza
Settore MAT/01 - Logica Matematica
Settore INF/01 - Informatica
2008
Article (author)
File in questo prodotto:
File Dimensione Formato  
CBA.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 348.63 kB
Formato Adobe PDF
348.63 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/550471
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 9
social impact