Busca avançada
Ano de início
Entree
(Referência obtida automaticamente do Web of Science, por meio da informação sobre o financiamento pela FAPESP e o número do processo correspondente, incluída na publicação pelos autores.)

Cut-Based Abduction

Texto completo
Autor(es):
D'Agostino, Marcello ; Finger, Marcelo ; Gabbay, Dov
Número total de Autores: 3
Tipo de documento: Artigo Científico
Fonte: LOGIC JOURNAL OF THE IGPL; v. 16, n. 6, p. 537-560, DEC 2008.
Citações Web of Science: 8
Resumo

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. (AU)

Processo FAPESP: 04/14107-2 - Logical consequence and combinations of logics: fundaments and efficient applications
Beneficiário:Walter Alexandre Carnielli
Modalidade de apoio: Auxílio à Pesquisa - Temático