Aula
Data
Bibliografia
Sumário
1
20/09
Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada. Breve história da lógica e algumas aplicações na Ciência de Computadores.
3
29/09/2015
Funções de verdade (ou boleadas). Conjuntos completos de conectivas. Completude dos conjuntos "não","e","ou" e "não","implicação". Fórmulas em forma normal negativa. normal disjuntiva e normal conjuntiva.
10
23/10/2015
NLC pp 52-57
Outros sistemas dedutivos. Sistemas dedutivos analíticos (automáticos). Tableaux semanticos: regras, expansão e tabieaus fechados. Integridade e Completude dos tableaux semanticos. Resolução: integridade.
11
27/10/2015
NLC pp 57-62
Lógica de primeira ordem. Linguagens da lógica de primeira ordem. Símbolos lógicos e não lógicos, termos e fórmulas. Exemplo duma linguagem para a aritmética.
12
30/10/2015
NLC pp 62-67
Variáveis ligadas e livres. Proposições.
Semântica da lógica de primeira ordem: estruturas das linguagens de primeira ordem, interpretações de variáveis, relação de satisfabilidade. Exemplo do "Mundo dos Blocos".
Semântica da lógica de primeira ordem: estruturas das linguagens de primeira ordem, interpretações de variáveis, relação de satisfabilidade. Exemplo do "Mundo dos Blocos".
13
3/11/2015
NLC pp 67-74
Semântica da lógica de primeira ordem (cont.). Satisfabilidade, validade, e consequência semântica. Modelos para proposições. Exemplos.
14
6/11/2015
NLC pp 74-78
Caracterização de estruturas por fórmulas da lógica de primeira ordem. Grafos e Digrafos como estruturas.
Validade e Satisfabilidade. Equivalência Semântica. Equivalências semânticas envolvendo quantificadores e operações lógicas.
Validade e Satisfabilidade. Equivalência Semântica. Equivalências semânticas envolvendo quantificadores e operações lógicas.
15
10/11/2015
NLC pp 78-80
Noção de substituição e variável substituível por um termo. Forma normal Prenexa. Conversão para forma normal prenexa.
16
13/11/2015
NLC pp 81-85
Sistema de dedução natural para lógica de primeira ordem: regras de introdução e eliminação da igualdade e quantificador universal. Exemplos.
17
17/11/2015
NLC pp 85-91
Sistema de dedução natural para lógica de primeira ordem: regras de introdução e eliminação para o quantificador existêncial. Equivalência dedutiva.Exemplos.
20
27/11/2015
NLC pp 101-105
Consequências da completude e integridade da lógica de primeira ordem. Teorema da compacidade. Aplicações da compacidade. Teoremas de Lowenheim-Skolem. Limitações da expressividade da lógica de primeira ordem.
22
04/12/2015
Introdução à Programação em lógica. Objectivos. Resolução para a lógica proposicional. Cláusulas de uma linguagem de primeira ordem. Conversão para forma clausal. Resolução para cláusulas fechadas.
23
11/12/2015
Substituições. Propriedades de substituições, variantes, mudanças de nome. Exemplos. Unificadores e unificadores mais gerais. Conjunto de diferenças de um conjunto de expressões simples. Algoritmo de unificação. Teorema do algoritmo de unificação. Resolução Geral.
23
11/12/2015
Fórmulas de Horn para a lógica proposicional:satisfabilidade. Fórmulas de Horn para a lógica de primeira ordem: positivas, unitárias e negativas. Programas definidos e objectivos. Exemplos.Resolução SLD para cláusulas de Horn. Árvores de derivação SLD. Exemplo de um programa em Prolog.
25
18/12/2015
A aula é substituída por uma aula de dúvidas em Janeiro.