Contextualização da histórica da lógica. As diversas lógicas e suas motivações. Avaliação semântica da lógica de primeira ordem. Transformações clausais e teorema de Herbrand. Cláusulas de Horn. Prova automática de teoremas: sistema formal da resolução. Resolução LSD (ResoluçãoSLD). Negação por falha finita. Aplicação na programação em lógica: bases de dados dedutivas, metalinguagens, notações gramaticais, programação por restrições, agentes lógicos e em sistemas
multiagentes.