Esta disciplina tem por objectivo aprofundar a relação existente entre lógica formal e a computação. Esta relação pode assumir diferentes formas, dependendo da perspectiva sobre a qual é analisada:

• Uma primeira perspectiva consiste em eleger o processo de verificar a validade de fórmulas lógicas como problema computacional - por outras palavras, procuram-se construir programas que estabeleçam a validade de fórmulas lógicas. Tal como iremos ter oportunidade de estudar neste curso, este problema é difícil, mesmo para lógicas muito simples (e.g. lógica proposicional).
• Uma segunda perspectiva consiste em adoptar a noção de dedução lógica como motor de cálculo de uma linguagem de programação. Uma destas linguagens é o Prolog, que será estudada neste curso.
• Por último, iremos também abordar o que é habitualmente designado por Analogia de Curry-Howard: esta analogia permite-nos estabelecer um paralelo entre sistemas lógicos e linguagens de programação funcionais, constituindo assim uma fundamentação lógica para essas linguagens.