Lógica Computacional
(cod.14336 & 14775 )

Departamento de Informática
Universidade da Beira Interior

—
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.”
—

Figure 1: from logicomix

Esta página no formato pdf

1 Novidades

A informação presente neste site é mínima. Queira consultar o Teams@UBI de Lógica Computacional para informação atualizada.
Mooshak: processo de registo (link aqui).

O sistema mooshak encontra-se desde já configurado para a presente disciplina. Queira proceder ao seu registo.
Aceita-se a formação de grupos de, no máximo, duas pessoas. No processo de registo, escolhe o grupo UBI e defina o nome da equipa da seguinte forma.
Se for um grupo de um só elemento: numero 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+numero de aluno do segundo elemento + primeiro nome. Assim se Luis forma grupo com o João (aluno 13245), então o grupo registra-se com o nome “12345Luis13245Joao”.
Consultar a secção 8 para aceder ao material electrónico (teórico e prático) exposto nas aulas.
Inscrição em turmas práticas: via site dos serviços académicos.
As aulas práticas começam logo na primeira semana de aulas.
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.

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

2 Docentes

Simão Melo de Sousa (regente) - Gabinete 3.17 - Laboratório Release/QuiVVer/NOVA-LINCS (6.25) - Bloco VI
Luis Horta
André de Matos Pedro

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

Tirar proveito do Grupo Teams da UC e colocar a dúvida no canal adequado - método preferido!
Comparecer nas aulas e colocá-la directamente ao docente.
Comparecer no horário de atendimento do regente e colocá-la directamente.
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.

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 relação de satisfação
  - Validade e consequência lógica
  - Equivalência e raciocínio equacional
- Sistema semântico: algoritmos para a resolução SAT
- Sistema semântico: resolução
  - Forma normal conjuntiva e forma clausal
  - Algoritmo de Horn
  - Resolução e refutação
- Sistema dedutivo: dedução natural
  - Regras de introdução e eliminação
  - Derivação e prova
  - Coerência e Completude
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 e raciocínio equacional
- Sistemas semânticos: SMT
  - Método e algoritmo DPLL
  - Teorias de Primeira Ordem
  - Combinação de Teorias
- Sistema semântico: resolução
  - Forma Normal de Skolem e skolemização
  - Unificação e resolução
- Sistema dedutivo: dedução natural
  - Regras de introdução e eliminação
  - Derivação e prova
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 por uma componente prática

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 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 grupo de um ou dois alunos. As datas exactas de entrega encontram-se na secção 6. A entrega é feita de forma electrónica no site mooshak da UC.
Os grupos com um exercício avaliado pelo Mooshak como “Accepted” deverão defender a solução entregue durante a aula prática (do primeiro elemento do grupo) que segue a data de entrega.
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, o "aproveitamento mínimo" 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 defendeu com sucesso pelo menos um dos dois exercícios da componente prática e que entregou a prova escrita da frequência.

Avaliação contínua quantitativa

No caso de “Frequência” (i.e. NCP ≥ 6 valores (em 20)), a avaliação quantitativa, designada aqui de Nota da Avaliação Contínua (NAC), é determinada da seguinte forma:

NAC=

componente prática (NCP) × 0.8 + componente teórica (NCT) × 1.2

5.5 Avaliação por Exame

A nota da prova escrita do exame substituirá a nota da componente teórica da Avaliação Contínua. Em consequência, a Nota da Avaliação por Exame segue o mesmo cálculo que a Nota da Avaliação Contínua.

6 Datas Importantes

Frequência: segunda-feira 29 de Maio de 2023 das 14h00 às 16h00.
Componente prática:
- Exercício 1: Entrega semana do 17 de Abril de 2023
- Exercício 2: Entrega semana do 29 de Maio de 2023
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 Atendimento

Por marcação (por email) ou

Horário	Docente
segunda-feira das 16h00 às 18h00	S. Melo de Sousa

8 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

aula inaugural - O que é a lógica?

Lógica Computacional

Aula 1 - Apresentação

Aula 2 - Sintaxe da Lógica Proposicional

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

Aula 4 Semântica da Lógica Proposicional

Aula 5 Semântica da Lógica Proposicional

Aula 6 Semântica da Lógica Proposicional

Aula 7 Semântica da Lógica Proposicional

Aula 8 Formas Normais e Forma Normal Conjunctiva

Aula 9 Algoritmo de conversão para a Formal Normal Conjunctiva

Aula 10 Algoritmo de Horn

Aula 11 Resolução para a Lógica Proposocional

Aula 12 Estratégias de Resolução

Aula 13 Dedução Natural para a Lógica Proposicional (Complemento: Formulário para a Dedução Natural)

Aula 14 Dedução Natural para a Lógica Proposicional

Aula 15 Sintaxe da Lógica de Primeira Ordem

Aula 16 Sintaxe da Lógica de Primeira Ordem

Aula 17 Semântica da Lógica de Primeira Ordem

Aula 18 Leis da Lógica de Primeira Ordem

Aula 19 Forma Normal Prenex

Aula 20 Forma Normal de Skolem e Unificação

Aula 21 Resolução em Lógica de Primeira Ordem

Aula 22 Dedução Natural em Lógica de Primeira Ordem (complemento: formulário extendido para a dedução natural para a Lógica de Primeira Ordem)

Aula 23 Dedução Natural em Lógica de Primeira Ordem

Práticas

Computação simbólica e Programação: consultar a página seguinte (link)

Ficha Técnicas Matemáticas de Demonstração (da UC Teoria de Computação)

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

Trabalhos Práticos

Problema A: Por definir

Problema B: Por definir

Complementos pedagógicos

Resolução da frequência 2016-2017 (aqui)

9 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.
(Capítulos 3,4 e 5)

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.14336 & 14775 )

Departamento de Informática Universidade da Beira Interior