Título: Using Abduction to Compute Efficient Proofs
Palestrante:  Marcelo Finger

Data:   15/09/2008, 14h30
Local:  Sala 03B, IME-USP

Resumo:
--------------

  The aim of this work is to present a solution to the problem 
  of computing non-analytic cuts. Several algorithms are 
  provided that compute efficient proofs with non-analytic 
  cuts via extended abductive reasoning.

  Extended abductive reasoning computes an extra hypothesis
  to a statement whose validity is unknown, such that:

  -- The statement becomes provable with the addition 
     of the extra hypothesis.
  -- The extra hypothesis is not trivial (in some precisely 
     defined sense).
  -- If the statement was originally valid (which is not known a priory) 
     then the addition of the extra hypothesis leads to a statement 
     with 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
  to be invalid.

  The idea is that the input is a contextual database, containing
  background knowledge, plus a goal formula representing some fact
  or evidence that one wants to explain or prove, and we want to 
  compute an hypothesis that explains the evidence in the presence 
  of the background knowledge or that facilitates the proof of 
  $G$ from $\Gamma$.

  This is a joint work with Marcello D'Agostina and Dov Gabbay.