UDESCCiência da Computação: Disciplinas
PROVADORES AUTOMÁTICOS DE TEOREMAS (OPAT001)
Fase: 0ª, CHT = 36, CHP = 36, CHTT = 72
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.
Centro de Ciências Tecnológicas - CCT
Rua Paulo Malschitzki, 200 - Campus Universitário Prof. Avelino Marcante - Bairro Zona Industrial Norte - Joinville - SC - Brasil
CEP: 89.219-710 - Fone:(47) 3481-7900
© 2016 - CINF - UDESC/Joinville
Rua Paulo Malschitzki, 200 - Campus Universitário Prof. Avelino Marcante - Bairro Zona Industrial Norte - Joinville - SC - Brasil
CEP: 89.219-710 - Fone:(47) 3481-7900