Título: Abduzindo Eficiências 

Palestrante: Marcelo Finger

Resumo:

Abdução é uma forma de raciocínio que gera explicações plausíveis para
um fato.  Dada uma teoria T que expressa o conhecimento de fundo sobre
algum domínio e uma obsevação meta M que se deseja explicar, a abdução
produz uma hipótese H tal que T+H prova M.

Tradicionalmente, exige-se que T não prove M para se realizar uma
abdução.  Nós abolimos esta exigência, e mostramos dois métodos
distintos que permitem abduzir (computacionalmente) H
independentemente de T provar ou não M.  Além disso, mostramos que no
caso em que T prova M, T+H prova M muito mais eficientemente, portanto
o nome do método de abdução de eficiências.

Este método pode ser iterado para provar uma prova não-analítica de M
dado T.  Sabe-se que provas não-analíticas podem ser exponencialmente
menores que provas analíticas, e o método de abdução de eficiências é
uma forma de computar uma prova não analítica.  Mostramos que neste
caso, temos a propriedade de terminação fraca.  Ou seja, o algoritmo
pode sempre ser terminado, se forem feitas as escolhas corretas.