Título: PROVADORES DE TEOREMAS BASEADOS EM TABLEAUS
       Palestrante: Adolfo Gustavo Serra Seca Neto 

       Resumo: Os provadores automáticos de teoremas (PAT´s) foram uma das 
               primeiras aplicações interessantes na Ciência da
               Computação. Desde os anos 50 eles têm sido tema de pesquisa e
               implementações. Além de serem utilizados para a prova de
               teoremas matemáticos, os PAT´s atualmente são aplicados na
               verificação, otimização e síntese de software, e também como
               motor de inferência em sistemas de Inteligência Artificial. A
               área de "Raciocínio Automatizado" continua sendo uma área
               fértil, com várias conferências internacionais e inclusive uma
               competição anual que escolhe as melhores implementações de
               PAT´s, uma espécie de "campeonato mundial" para provadores de
               teoremas. 

               A maioria dos PAT´s é baseada numa técnica chamada
               Resolução. Neste seminário iremos apresentar o formalismo
               lógico dos Tableaus e mostrar como podem ser implementados
               PAT´s baseados em Tableaus.