Teoricas de Lógica Computacional CC2003/CC216

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.