Using Abduction to Compute Efficient Proofs

Autor(es)

Finger, Marcelo

• 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