Sumários
Aula |
Data |
Sumário |
Apont. |
Bib |
1 |
23/9 |
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 |
26/9 |
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. |
LC Pag. 1-11 |
LICS 1.1-3-4 |
3 |
30/9 |
Funções de
verdade. Conjuntos completos de conectivas. Completude dos
conjuntos "não","e","ou" e "não","implicação". Fórmulas em forma normal
negativa e normal disjuntiva. |
LC Pag 11-16 |
LICS 1.5.1-2 |
4 |
3/10 |
Forma normal conjuntiva. Satisfazibilidade. Cláusulas e
conjuntos de cláusulas. Algoritmo de Davis-Putnam para a
satisfazibilidade de cláusulas. |
LC Pag 17-18, 19-23 |
|
5 |
7/10 |
Métodos de dedução axiomáticos. Sistema de dedução natural. Regras de inferência: conjunção e disjunção. Exemplos.
| LC Pag 24-29 |
Regras DN P
(Fitch) |
6 |
10/10 |
Sistema de dedução natural (cont.). Regras de inferência: negação e falso. Exemplos.
| LC Pag 29-32 |
Regras DN P
(Fitch)
|
7 |
14/10 |
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.
| LC Pag 32 - 39 |
Regras DN P
(Fitch)
|
8 |
17/10 |
Integridade e Completute de sistemas de dedução. Integridade do sistema DN de dedução natural.
| LC Pag 39- 43 |
Regras DN P
(Fitch)
|
9 |
21/10 |
Completute de sistemas DN de dedução natural.
| LC Pag 43- 46 |
Regras DN P
(Fitch)
|
10 |
24/10 |
Decidibilidade da lógica proposicional. 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.
| LC Pag 46- 51 |
|
11 |
28/10 |
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.
| LC Pag 52-57 |
|
12 |
31/10 |
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".
| LC Pag 57-60 |
|
13 |
04/11 |
Semântica da lógica de primeira ordem (cont.). Satisfabilidade, validade, e consequência semântica. Modelos para proposições. Exemplos.
| LC Pag 60-67 |
|
14 |
07/11 |
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.
| LC Pag 68-72 |
|
15 |
11/11 |
Equivalências semânticas envolvendo quantificadores e operações lógicas. Noção de substituição e variável substituível por um termo. Forma normal Prenexa. Conversão para forma normal prenexa.
| LC (nova versão) Pag 73-76 |
|
16 |
14/11 |
Sistema de dedução natural para lógica de primeira ordem: regras de introdução e eliminação da igualdade e quantificador universal. Exemplos.
| LC (nova versão) Pag 77-80 |
Regras DN LPO |
17 |
18/11 |
Sistema de dedução natural para lógica de primeira ordem: regras de introdução e eliminação para o quantificador existêncial. Exemplos.
| LC (nova versão) Pag 81-83 |
Regras DN LPO(Fitch) |
18 |
21/11 |
Sistema de dedução natural para lógica de primeira ordem: equivalência dedutiva. Exemplos.
| LC (nova versão) Pag 83-89 |
Regras DN LPO (Fitch) |
19 |
25/11 |
Integridade e Completude do sistema de dedução natural para lógica de primeira ordem.
| LC (nova versão) Pag 90-97 |
Regras DN LPO (Fitch) |
20 |
28/11 |
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.
| LC (nova versão) Pag 97-101 |
|
21 |
2/12 |
Aplicações da Compacidade. Axiomatizações. Axiomas de Peano para a aritmética.
| LC (nova versão) Pag 101-108 |
|
22 |
5/12 |
Teorias de lógica de primeira ordem. Axiomatizações e Teorias completas. Incompletude dos axiomas de Peano e indecididabilidade da lógica de primeira ordem.
| LC (nova versão) Pag 108
Complementar Cap. 3 |
|
23 |
9/12 |
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.
| |
|
24 |
12/12 |
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.
| |
|
25 |
16/12 |
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.
| |
|