Using Abduction to Compute Efficient Proofs

Full text
Author(s):	Finger, Marcelo Total Authors: 1
Document type:	Journal article
Source:	ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 247, p. 11-pg., 2009-08-04.
Abstract
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)

FAPESP's process:	04/14107-2 - Logical consequence and combinations of logics: fundaments and efficient applications
Grantee:	Walter Alexandre Carnielli
Support Opportunities:	Research Projects - Thematic Grants