Seminário de Teoria da Computação

       
              Um Provador de Teoremas Multi-Estratégia

                  Adolfo Gustavo Serra Seca Neto

		           IME-USP

              Sexta-feira, 1 de abril de 2005 

                Sala 85  14:00hs  <-----  Notem mudança de sala e de horário



Resumo:

As regras de inferência de sistemas automatizados de dedução são
tipicamente não determinísticas. Elas especificam o que se pode fazer,
mas não como fazer.  Portanto, para obter um procedimento mecanizável,
as regras de inferência precisam ser complementadas por outro
componente, chamado de estratégia.  Num provador de teoremas
multi-estratégia podemos escolher entre diversas estratégias no
momento de realizar uma dedução.  Um provador de teoremas
multi-estratégia pode ser usado, entre outras coisas, para ilustrar
como a escolha da estratégia pode afetar a performance do provador,
assim como para testar novas estratégias e fazer comparaçoes entre
elas. Nesta palestra apresentaremos um provador de teoremas
multi-estratégia baseado no método de tablôs KE (de Marco Mondadori e
Marcello D'Agostino).