Using Abduction to Compute Efficient Proofs
Marcelo Finger · Electronic Notes in Theoretical Computer Science · 2009
The aim of this work is to show how to compute an extra hypothesis H to an unproved sequent Γ⊢?G, such that: Γ,H⊢G is provable; H is not trivial. If Γ⊢G (which is not known a priory) then Γ,H⊢G has a much simpler proof. The idea is that Γ 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 Γ. 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.