sexta-feira, 19 de setembro de 2008

Seminário LIAMF 15/09/2008

Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP

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

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


 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.
 Marcelo Finger
 Departamento de Ciencia da Computacao
 Instituto de Matematica e Estatistica | home page:
 Universidade de Sao Paulo             |
 Rua do Matao, 1010                    | Tel: +55 11 3091 6310, 3091 6135
 05508-090    Sao Paulo, SP     Brazil | Fax: +55 11 3091 6134, 3814 4135

Nenhum comentário: