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.
2
25/09/2015
NLC pp 7-14
LICS 1.1-3-4
Linguagens do cálculo proposicional: símbolos primitivos e fórmulas. Subfórmulas. Semântica: atribuições de valores de verdade; tabelas de verdade;satisfazibilidade de fórmulas e conjuntos de fórmulas; tautologias. Consequência e equivalência semântica.
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.
4
02/10/2015
NLC pp 20-25
LICS 1.5.1-2.
SAT 84-88
Fórmulas de Horn. Satisfazibilidade. Cláusulas e
conjuntos de cláusulas. Algoritmo de Davis-Putnam para a
satisfazibilidade de cláusulas.
5
06/10/2015
NLC pp 26—33
LICS 1.1 e 1.2.1
LPL
Regras
Sintaxe da Lógica Proposicional. Métodos de dedução axiomáticos. Sistema de dedução natural. Regras de inferência: conjunção e disjunção. Exemplos.
6
09/10/2015
NLC pp 33-37
LICS 1.2
LPL
Regras
Sistema de dedução natural. Regras de inferência: negação e falso. Exemplos.
7
13/10/2015
NLC pp 37-45
LICS 1.2
LPL
Regras
Sistema de dedução natural (cont.). Regras de inferência: implicação. Exemplos. Regras derivadas: dupla negação, modus tollens, redução ao absurdo e terceiro excluído. Equivalência dedutiva.
8
16/10/2015
NLC pp 45-49
LICS 1.4.3
LPL
Regras
Fitch
Integridade e Completute de sistemas de dedução. Integridade do sistema DN de dedução natural.
9
20/10/2015
NLC pp 49-52
LICS 1.4
LPL
Regras
Fitch
Integridade e Completute de sistemas de dedução: completude do sistema DN de dedução natural. Decidibilidade da lógica preposicional
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".

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.
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.
18
20/11/2015
NLC pp 91-96
Integridade do sistema de dedução natural para lógica de primeira ordem.
19
24/11/2015
NLC pp 96-101
Completude do sistema de dedução natural para lógica de primeira ordem.
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.
21
01/12/2015
NLC pp 105-108
Axiomatizações. Axiomas de Peano para a aritmética.
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.