Busca avançada
Ano de início
Entree


Using Abduction to Compute Efficient Proofs

Texto completo
Autor(es):
Finger, Marcelo
Número total de Autores: 1
Tipo de documento: Artigo Científico
Fonte: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 247, p. 11-pg., 2009-08-04.
Resumo

The aim of this work is to show how to compute an extra hypothesis H to an unproved sequent Gamma proves(?) G, such that: Gamma, H proves G is provable; H is not trivial. If Gamma proves G (which is not known a priory) then Gamma, H proves G has a much simpler proof. Due to the last item, this is not exactly the usual abductive reasoning found in literature, for the latter requires the input sequent not to be derivable. The idea is that Gamma is a contextual database, containing background knowledge, G is a goal formula representing some fact or evidence that one wants to explain or prove, and H is an hypothesis that explains the evidence in the presence of the background knowledge or that facilitates the proof of G from Gamma. We show how this task is related to the problem of computing non-analytic cuts. Several algorithms are provided that compute efficient proofs with non- analytic cuts via abductive reasoning. This is a joint work with Marcello D'Agostino and Dov Gabbay. (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