A teoria da programação em lógica é aprofundada nesta cadeira, com o objectivo de estudar processos de demonstração automática de teoremas. Alguns dos tópicos abordados serão: fórmulas e interpretações na lógica, formas normais, teorema de Herbrand, princípio de resolução, resolução semântica, resolução linear, paramodulação.