Código |
13916
|
Ano |
2
|
Semestre |
S1
|
Créditos ECTS |
6
|
Carga Horária |
PL(30H)/T(30H)
|
Área Científica |
Informática
|
Objectivos de Aprendizagem |
Objetivos de aprendizagem (conhecimentos, aptidões e competências a desenvolver pelos estudantes):
Esta disciplina apresenta os principais conceitos da Lógica, na sua vertente computacional, i.e. acompanhados dos algoritmos e das técnicas computacionais que permitam o seu uso num contexto de engenharia Informática.
Competências da UC ou Resultados da Aprendizagem:
Pretende-se que o aluno aprenda as noções básicas do raciocínio lógico e seja capaz de utilizar corretamente 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 Engenharia Informática.
|
Conteúdos programáticos |
1- Apresentação Contextual e Histórica da Lógica
2- Computação Simbólica: Introdução à Programação Funcional
3- Conjuntos Indutivos, Indução Estrutural e Bem Fundada
4- Lógica Proposicional
4.1- Sintaxe
4.2- Semântica
4.3- Sistema semântico: algoritmos para a resolução SAT
4.4- Sistema semântico: resolução
4.5- Sistema dedutivo: dedução natural
5- Lógica de primeira ordem
5.1- Sintaxe
5.2- Semântica:
5.2.1- Valoração e estrutura de interpretação: relação de satisfação
5.2.2-Validade e consequência lógica
5.2.3- Equivalência e raciocínio equacional
5.3- Sistemas semânticos: SMT
5.3.1- Método e algoritmo DPLL
5.3.2- Teorias de Primeira Ordem
5.3.3- Combinação de Teorias
5.4- Sistema dedutivo: resolução
5.5- Sistema dedutivo: dedução natural
6- Extensões à Lógica Predicativa
|
Metodologias de Ensino e Critérios de Avaliação |
As aulas presenciais são divididas em:
• Aulas Teóricas onde são expostos os conceitos teóricos, os algoritmos, as tecnologias capacitivas, próprios à construção de sistemas computacionais de análise lógica ou até mesmo de um sistema de processamento lógico.
• Aulas Práticas com aplicação das técnicas/conceitos introduzidos, uso das ferramentas lógicas existentes, a construção de provas e raciocínios lógicos com base nestas. Em termos de trabalhos e aplicações práticas, visar-se-á dois tipos de aplicações: aplicação destes conceitos a problemas concretos da engenharia informática, e a construção/programação de pequenas aplicações que decorrem dos algoritmos expostos
A avaliação será realizada por uma prova escrita e por avaliação contínua baseada em exercícios práticos.
NF = Nota final
NCP = Nota da componente prática (média dos exercícios)
NCT = Nota da componente teórica (prova escrita - exame ou frequência)
NF = SE (NCT >= 6) ENTÃO (NCT + NCP)/2 SENÃO Reprovado
|
Bibliografia principal |
[1] Mordechai Ben-Ari. Mathematical Logic for Computer Science. SV, 2nd edition, 2001.
[2] Jon Barwise and John Etchmendy. Language, Proof, and Logic. CSLI, 2000.
[3] Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning about systems. CUP, 2004.
[4] J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first edition, 307 p. 52 illus. edition, 2011.
[5] D. van Dalen. Logic and Structure. 5th Edition, Springer Verlag, Berlin, Germany, 2013.
|
Língua |
Português
|