Computational Logic (2021/2022)

This page content is in portuguese.

Para mais informações, consultar a página do regente da disciplina aqui.

Equipa docente

Como colocar uma dúvida à equipa docente da Unidade Curricular?

1. Tirar proveito do Grupo Teams da UC e colocar a dúvida no canal adequado - método preferido!
2. Comparecer nas aulas e colocá-las diretamente aos docentes.
3. Comparecer no horário de atendimento do regente e colocá-las diretamente.
4. Enviar um email aos docentes 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.

Horário da disciplina

• SMDS: Simão Melo de Sousa
• JR: João Reis
• LH: Luís Horta

Avaliação da 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 exercícios práticos. Esta avaliação tomará a forma da resolução de desafios de programação dos conceitos introduzidos nas aulas. Os exercícios avaliados são em número de 2 e resolvidos de uma forma sequencial e em grupos de um ou dois alunos. As datas de entrega são as seguintes:

• Exercício 1: Entrega semana do 26 de Abril de 2022.
• Exercício 2: Entrega semana do 7 de Junho de 2022.

A entrega é feita de forma eletrónica no site Mooshak da UC.

O sistema Mooshak encontra-se desde já configurado para a presente disciplina. Queiram proceder ao registo dos grupos. Aceita-se a formação de grupos de, no máximo, duas pessoas. No processo de registo, escolham o grupo UBI e definam o nome da equipa da seguinte forma:

• Se for um grupo de um só elemento: número de aluno + primeiro nome. Por exemplo, Luís com o numero 12345 tem por registo Mooshak “12345Luis”.
• Se for um grupo de duas pessoas: numero de aluno do primeiro elemento (o de número mais baixo) + primeiro nome + número de aluno do segundo elemento + primeiro nome. Assim se o Luís com o número 12345 forma grupo com o João (aluno 13245), então o grupo regista-se com o nome “12345Luis13245Joao”.

Configurar um ambiente de desenvolvimento OCaml

Recomenda-se consultar a página seguinte para instalar e configurar um ambiente de desenvolvimento OCaml: Up and Running with OCaml

Aulas Práticas

• Aula Prática 1
  • Tradução de asserções em línguagem natural para fórmulas em lógica proposicional.
  • Verificação que sequências de símbolos são fórmulas.
• Aula Prática 2
  • Definições indutivas e indução estrutural.
• Aula Prática 3
  • Semântica da lógica proposicional: álgebra de Boole e tabelas de verdade.
• Aula Prática 4
  • Semântica da lógica proposicional: noção de consequência semântica.
• Aula Prática 5
  • Semântica da lógica proposicional: equivalência lógica.
• Aula Prática 6-7
  • Forma Normal Conjuntiva.
• Aula Prática 8
  • Análise do algoritmo T.
• Aula Prática 9
  • Algoritmo de Horn.
• Aula Prática 10
  • Algoritmo de Horn.
• Aula Prática 11
  • Resolução em Lógica Proposicional.
• Aula Prática 12
  • Resolução em Lógica Proposicional.
• Aula Prática 13
  • Dedução natural em lógica proposicional: provas de teoremas.
• Aula Prática 14
  • Dedução Natural em Lógica Proposicional.
• Aula Prática 15
  • Dedução natural em lógica proposicional: provas de teoremas.
• Aula Prática 16
  • Dedução natural em lógica proposicional: provas de consequência sintática.
• Aula Prática 17
  • Tradução de asserções em linguagem natural para fórmulas em lógica de primeira ordem.
• Aula Prática 18
  • Manipulação de variáveis em termos e fórmulas.
• Aula Prática 19
  • Semântica da Lógica de Primeira Ordem.
• Aula Prática 20
  • Consequência Semântica em Lógica de Primeira Ordem.
• Aula Prática 21
  • Leis da Lógica de Primeira Ordem.
• Aula Prática 22
  • Forma Normal Conjuntiva Prenex e Skolemização.
• Aula Prática 23
  • Resolução em Lógica de Primeira Ordem.
• Aula Prática 24
  • Dedução Natural em Lógica de Primeira Ordem.