Lógica e Programação

Código:

CC216

Sigla:

CC216

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2011/2012 - 2S

Ativa?	Sim
Página Web:	http://www.dcc.fc.up.pt/~nam/web/Teaching/LP1112/index.html
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Licenciatura em Geologia

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
L:AST	0	Plano de Estudos a partir de 2008	3	-	7,5	-
L:B	0	Plano de estudos a partir de 2008	3	-	7,5	-
L:CC	55	Plano de estudos de 2008 até 2013/14	2	-	7,5	-
L:F	2	Plano de estudos a partir de 2008	3	-	7,5	-
L:G	2	P.E - estudantes com 1ª matricula anterior a 09/10	3	-	7,5	-
		P.E - estudantes com 1ª matricula em 09/10	3	-	7,5	-
L:M	4	Plano de estudos a partir de 2009	3	-	7,5	-
L:Q	0	Plano de estudos Oficial	3	-	7,5	-
MI:ERS	81	Plano de Estudos a partir de 2007	2	-	7,5	-

Língua de trabalho

Português

Objetivos

Introdução à lógica matemática numa perspectiva computacional.

Pretende-se que o aluno aprenda as noções básicas do raciocínio lógico e seja capaz de utilizar correctamente os sistemas dedutivos; compreenda as relações entre as semânticas e os sistemas dedutivos e a sua caracterização do ponto de vista da decidibilidade; reconheça o papel dos sistemas formais nas várias áreas da Ciência de Computadores e em especial na Programação em Lógica.

Programa

Lógica proposicional
Sintaxe.
Semântica: satisfazibilidade, validade, consequência.
Formas normais.
Sistema dedutivo de dedução natural.
Completude e integridade do sistema dedutivo. Decidibilidade.
Outros sistemas dedutivos.
Lógica de primeira ordem (de predicados)
Linguagens.
Sintaxe.
Semântica: estruturas, interpretações, modelos.
Sistemas dedutivo de dedução natural.
Completude e integridade dos sistemas dedutivos.
Teorias e axiomatizações
Indecidibilidade da lógica de primeira ordem.
Limite dos métodos formais (Teorema de Gödel)
Programação em lógica
Resolução
Fórmulas de Horn e programas definidos
Unificação de termos
Resolução-SLD
Introdução à programação em Prolog
sintaxe
recursão e retrocesso
corte de alternativas
negação por insucesso
predicados prédefinidos.

Bibliografia Obrigatória

Mordechai Ben-Ari. ; Mathematical Logic for Computer Science.
Jon Barwise and John Etchmendy; Language, Proof, and Logic.

Bibliografia Complementar

W. Clocksin; Clauses and Effects

Métodos de ensino e atividades de aprendizagem

Serão propostos trabalhos para os alunos resolverem e haverá aulas de apresentação e discussão da resolução dos problemas que foram propostos.

Há aulas teóricas de exposição da matéria e exemplificação de problemas. As aulas práticas são divididas em aulas de exemplificação e apresentação de trabalhos realizados pelos alunos.

Tipo de avaliação

Avaliação distribuída com exame final

Fórmula de cálculo da classificação final

A avaliação será composta por:

os trabalhos apresentados nas aulas práticas.
exame final

(Trab∗6+Exame∗14)≥9.5,Trab∗6≥2,Exame∗14≥6