Lógica Computacional
(cod.11555)

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2014/2015

Three logicians walk into a bar. The bartender says
“Do you all want something to drink?”
The first logicians says “I don’t know.”
The second logician says “I don’t know.”
The third logician says “Yes.”

Esta página no formato pdf

1 Novidades

Notas do Exame de Recurso: Aqui.
Notas do Exame: Aqui.
Notas da Avaliação Contínua: Aqui.
Entrega de trabalho de forma electrónica: até ao dia 11 às 18h00.
Para os trabalhos de prolog, veja a secção “Trabalhos Práticos” (secção 9) para informação complementar.
(15/10/2014) - Mudança da data da Frequência. Nova data: Segunda feira 5 de Janeiro das 18h00 às 20h00. Consultar as secções 6
Consultar a secção 9 para aceder aos material electrónico (teórico e prático) exposto nas aulas.
Como colocar uma dúvida ao regente da Unidade Curricular?
1. Comparecer nas aulas e colocá-la directamente ao regente
2. Comparecer no horário de atendimento do regente e colocá-la directamente
3. enviar um email ao regente (desousaUUU@UUUdi.ubi.pt, (retire os UUU) ) com o assunto "LC: XXXX" em que XXX é o título da dúvida em questão. Qualquer outro formato no assunto arrisca condenar o email ao esquecimento.
Inscrição em turmas práticas: via site dos serviços académicos.
Os alunos com estatuto de trabalhador estudante são convidados a dirigir-se ao regente para discutir eventuais alterações dos critérios de avaliação.
Primeira versão da página. Encontrará aqui as novidades associadas à disciplina de Lógica Computacional. A sua consulta regular é necessária ao bom funcionamento da Unidade Curricular.

1 Novidades
2 Docentes
3 Objectivos
- 3.1 Agradecimentos
4 Programa
5 Critérios de Avaliação
6 Datas Importantes
7 Horário
8 Atendimento
9 Material Pedagógico e Funcionamento da Disciplina
10 Resultados da avaliação
11 Bibliografia Principal

2 Docentes

Simão Melo de Sousa (regente) - Gabinete 3.17 - Laboratório Release (6.25) - Bloco VI.

3 Objectivos

Esta disciplina apresenta as 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.

3.1 Agradecimentos

O regente da disciplina gostaria de agradecer ao Professor Doutor António Ravarra (DI-FCT-UNL- Nova lincs) por lhe ter facultado a sebenta de Lógica Computacional de que é autor e por lhe permitido um uso livre e intensivo desta última.

4 Programa

Apresentação Contextual e Histórica da Lógica
Conjuntos Indutivos, Indução Estrutural e Bem Fundada
Lógica Proposicional
- Sintaxe:
  - Termos a partir de descrições em linguagem natural
  - Conectores lógicos
  - Definição indutiva de linguagem proposicional
  - Formas Normais: Negativa, Conjuntiva e Disjuntiva
- Semântica:
  - Tabelas de verdade e álgebra de Boole
  - Valoração e estrutura de interpretação: relação de satisfação
  - Validade e consequência lógica; equivalência
- Métodos Semânticos: Algoritmos para a resolução SAT
- Sistema dedutivo: dedução natural
  - Regras de introdução e eliminação
  - Derivação e prova
  - Coerência e Completude
- Sistema dedutivo: resolução
  - Forma normal conjuntiva e forma clausal
  - Algoritmo de Horn
  - Resolução e Refutação
Lógica de primeira ordem
- Sintaxe:
  - Termos a partir de descrições em linguagem natural
  - Alfabeto e Definição indutiva de linguagem de 1^ra ordem
  - Variáveis livres e substituição
- Semântica:
  - Valoração e estrutura de interpretação: relação de satisfação
  - Validade e consequência lógica; equivalência
  - Sistema dedutivo: dedução natural
  - Regras de introdução e eliminação
  - Derivação e prova
- Sistema dedutivo: resolução
  - Forma Normal de Skolem e skolemização
  - Unificação e resolução
- Sistemas semânticos: SMT
  - Método e algoritmo DPLL
  - Teorias de Primeira Ordem
  - Combinação de Teorias
Extensões à Lógica Predicativa

5 Critérios de Avaliação

5.1 Actividades de Ensino-Aprendizagem e Metodologias Pedagógicas

Por fim a avaliar as competências adquiridas, as actividades de Ensino-Aprendizagem avaliarão tanto a compreensão dos conceitos teóricos expostos como a capacidade em por estes em prática.

Assim, a avaliação será constituída por uma componente teórica e, de forma optativa, por uma componente prática (exercício prático entregue e apresentado à equipa docente).

Fraudes

A equipa docente realça que qualquer tipo de fraude em qualquer dos itens desta disciplina implica a reprovação automática do aluno faltoso, podendo ainda vir a ser este alvo de processo disciplinar.

Listamos a seguir as diferentes componentes da avaliação.

5.2 Componente Prática

Esta avaliação mede em termos práticos a aquisição dos conceitos expostos. Como tal é baseada na avaliação da resolução de trabalho prático. Esta avaliação tomará em conta a resolução do desafio prático mas também a documentação (relatório) entregue e a apresentação feita à equipa docente.
A Nota da Componente Prática (NCP, 20 valores) é resultante da avaliação atribuída ao trabalho prático.

5.3 Componente Teórica

A avaliação da componente teórica consiste numa frequência (ver secção 6 para conhecer a data prevista da frequência).

Da avaliação desta prova resulta a Nota da Componente Teórica (NCT, 20 valores).

5.4 Concessão de Frequência e Avaliação Contínua

O parâmetro de "Frequência" atribuído no final desta unidade curricular traduz, no contexto da avaliação contínua, a "avaliação mínima" do estudante ao longo do processo de ensino-aprendizagem no final das actividades de contacto.

Considera-se que o estudante demonstrou ter adquirido o grau de conhecimentos mínimos (durante o processo de aprendizagem ao longo das actividades lectivas) quando este demonstrou as mínimas competências nas componentes avaliadas.

É assim concedido Frequência ao aluno que obteve os mínimos (6) em vigor na Universidade da Beira Interior na avaliação das componentes obrigatórias: a componente teórica (NCT).

No caso de Frequência, a avaliação quantitativa, designada aqui de Nota da Avaliação Contínua (NAC), é determinada da seguinte forma:

NAC = NCT

ou (caso se opte para a realização da componente prática)

NAC =

componente prática (NCP) × 0.5 + componente teórica (NCT) × 1.5

Se a avaliação quantitativa resultar numa nota maior ou igual a 10 então o aluno é dispensado de exame (Frequência com dispensa de exame).

5.5 Avaliação por Exame

A nota prova escrita do exame substituirá a Nota da Avaliação Contínua.

6 Datas Importantes

Frequência: Segunda feira 5 de Janeiro de 2015 das 18h00 às 20h00.
Trabalho:
- Entregue do enunciado do trabalho: Última semana lectiva de Outubro.
- Entrega do trabalho: (extensão) Até dia 11 de Janeiro 2014 às 18h00.
- Defesa do trabalho: Por anunciar.
Exame Época 1 : (conferir no site dos académicos).
Exame Época 2 : (conferir no site dos académicos).
Exame Época Especial : (conferir no site dos académicos).

7 Horário

Tipo de aula	Horário	Sala	Docente
Teórica	Quarta-Feira das 14h00 às 16h00	6.03	S. Melo de Sousa
Práticas Laboratoriais 3	Quinta-Feira das 16h00 às 18h00	6.13	S. Melo de Sousa
Práticas Laboratoriais 2	Sexta-Feira das 9h00 às 11h00	6.14	S. Melo de Sousa
Práticas Laboratoriais 1	Sexta-Feira das 16h00 às 18h00	6.14	S. Melo de Sousa

8 Atendimento

Horário	Docente
Quinta Feita das 9h00 às 13h00	S. Melo de Sousa

9 Material Pedagógico e Funcionamento da Disciplina

Os Apontamentos serão atempadamente disponibilizados nas aulas e por meios electrónicos. É esperado e assumido que o aluno tenha lido os acetatos referentes ao capítulo em curso antes das aulas teóricas.

Teóricas

(Regra geral: cada conjunto de acetatos (aula) corresponde a uma hora teórica)

Práticas

(Regra geral: cada ficha prática corresponde a uma hora de aulas práticas)

Trabalhos Práticos

Definido individualmente para cada grupo.

Introdução ao Prolog, pequena mas completa e pedagógica: link

Alguns exercícios Prolog resolvidos representativos: link

10 Resultados da avaliação

Nada por enquanto

11 Bibliografia Principal

As referencias principais são:

Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, 2004.
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 UTiCS. Springer-Verlag, first edition, 307 p. 52 illus. edition, 2011.

Utilizaremos ocasionalmente as referências:

D. van Dalen. Logic and Structure. 5th Edition, Springer Verlag, Berlin, Germany, 2013
René Cori e Daniel Lascar. Mathematical Logic: a course with exercices. Part I: propositional calculus, boolean algebras, predicate calculus. Oxford Press, 2007.
Mordechai Ben-Ari. Mathematical Logic for Computer Science. SV, 2nd edition, 2001.
Shawn Hedman. A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Oxford Texts in Logic, 2004.
Jon Barwise and John Etchemendy. Language Proof and Logic (4th edition) CSLI Publications, 2003.

Enviar comentários e dúvidas para (retire os UUU) : desousaUUU@UUUdi.ubi.pt

This document was translated from L^AT_EX by H^EV^EA.

Lógica Computacional (cod.11555)

Departamento de Informática Universidade da Beira Interior