Objetivos Gerais:

1 - Introduzir as noções básicas do raciocínio lógico e a problemática dos sistemas formais (lógicos) e principais conceitos associados. Apresentar vários sistemas dedutivos para as lógicas proposicional e de primeira ordem. Expor as relações entre as semânticas e os sistemas dedutivos.
2 - Abordar a relação existente entre lógica formal e a computação (nomeadamente apresentando uma linguagem de programação (Prolog) que adopta a noção de dedução lógica como motor de cálculo).

Conteúdos / Programa:

1 - Lógica Proposicional (Cálculo Proposicional).
1.1 - A noção de sistema formal (lógico): linguagem, semântica e sistema dedutivo.
1.2 - A(s) Linguagem(ns) do Cálculo Proposicional.
1.3 - Uma aplicação do princípio de indução estrutural na lógica proposicional.
1.4 - Semântica do cálculo proposicional (tabelas de verdade; tautologias; a noção de consequência semântica; formas normais; conjuntos adequados de conectivos).
1.5 - Uma axiomatização (à Hilbert) para o cálculo proposicional (provas e derivações, metateorema da dedução, correcção, coerência e adequação/completude da axiomatização).
1.6 - Outros sistemas dedutivos para o cálculo proposicional.
2 - Lógica de Primeira Ordem (Cálculo de Predicados).
2.1 - Linguagens de 1ª ordem e sua semântica (termo livre para uma variável numa fórmula; instância de uma tautologia; interpretação, valoração e validade).
2.2 - Uma axiomatização (à Hilbert) para o cálculo de predicados (sua correcção e coerência; metateorema da dedução; adequação/completude da axiomatização proposta).
2.3 - Outro sistema dedutivo para o cálculo de predicados.
3 - Introdução ao Prolog.
3.1 - O paradigma de programação em lógica.
3.2 - Introdução à programação em Prolog.

Bibliografia / Fontes de Informação:

Hamilton, A.G. , 1988 , Logic for Mathematicians , Cambridge University Press
E. Mendelson , 1997 , Introduction to Mathematical Logic , Chapman & Hall
J. H. Gallier , 1986 , Logic For Computer Science: Foundations of Automatic Theorem Proving , John Wiley & Sons
Reis, M.D.L. , 2014 , Folhas de apoio às aulas de lógica computacional , Universidade da Madeira
Makinson, D. , 2012 , Sets, Logic and Maths for Computing , Springer
Martins, J. P. , 2014 , Lógica e Raciocínio , College Publications
U. Nilsson and J. Maluszynski , 1995 , Logic, Programming and Prolog , John Wiley & Sons Ltd.
Blackburn, P. & Bos, J. & Striegnitz, K. , 2006 , Learn Prolog Now! , College Publications
Carmo, J. & Gouveia, P. & Dionísio, F. M. , 2013 , Elementos de Matemática Discreta , College Publications
Fitting, M. , 1996 , First-Order Logic and Automated Theorem Proving , Springer
Gabbay, D.M. , 2007 , Logic for Artificial Intelligence and Information Technology , King's College Publications
Oliveira, A. J. F. , 1980 , Lógica Elementar , AEFCL
Oliveira, A. J. F. , 1981 , Teoria dos Conjuntos: Indutiva e Axiomática (ZFC) , Livraria Escolar Editora
Oliveira, A.J.F. , 2010 , Lógica & Aritmética: Uma introdução à lógica, matemática e computacional , Gradiva
Sterling, L. & Shapiro, E. , 1986 , The Art of PROLOG: Advanced Programming Techniques , MIT Press

Métodos e Critérios de Avaliação:

Tipo de Classificação: Quantitativa (0-20)

Metodologia de Avaliação:
Metodologias de Ensino: Aulas teóricas expositivas; Aulas teórico-práticas destinadas à resolução de problemas; Aulas teórico-práticas destinadas à utilização do Prolog. Método de avaliação: A avaliação é feita através de um dos dois seguintes conjuntos de elementos de avaliação (a determinar pelo docente responsável pela disciplina no início do semestre): (i) Duas frequências obrigatórias e um trabalho, tendo a primeira e a segunda frequências os pesos de 40% e de 45%, respectivamente, e o trabalho o peso de 15% na classificação final. (ii) Duas frequências obrigatórias e um mini-teste, tendo cada uma das frequências o peso de 40%, e o mini-teste o peso de 20% na classificação final.