-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
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.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
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.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
