Título: "Prova Automática de Teoremas para Lógicas Modais"

Resumo: Lógicas modais têm sido utilizadas para descrever situações 
computacionais complexas tais como as que ocorrem em sistemas 
distribuídos. Dada a descrição lógica de um sistema computacional, 
propriedades deste sistema podem ser verificadas com o auxílio de 
ferramentas automáticas de prova. Nesta palestra, descreveremos a lógica 
modal de conhecimento, exemplos de sua aplicação na especificação de 
sistemas computacionais, bem como o cálculo baseado em resolução que 
pode ser empregado no processo de verificação.