Sintaxe e semântica do cálculo de predicados de primeira ordem. Sistemas dedutivos. Sistemas formais: axiomatização do cálculo de predicados, dedução natural no cálculo de predicados, tableaux semânticos no cálculo de predicados, teorema de herbrand, resolução no cálculo de predicados, lógica e programação em lógica.
