UNIVERSIDADE DO ESTADO DE SANTA CATARINA - UDESC

Provadores Automáticos de Teoremas (TOCI-17)

Ementa:

Aspectos teóricos da indecidibilidade da lógica clássica de primeira ordem. Lógicas
Para consistentes. Métodos de prova: tablôs e procedimento de Davis-Putnam. Implementação de
provadores baseados no método de tablôs. Implementação de provadores baseados no procedimento de
Davis-Putnam. Implementação de provadores para lógicas para consistentes.