Teóricas de Lógica e Programação 2011/2012
| Aula | Data | Sumário | Apont. | Bib |
|---|---|---|---|---|
| 1 | 28/2 | 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 | 1/3 | 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 | 6/3 | Funções de verdade. Conjuntos completos de conectivas. Completude dos conjuntos "não","e","ou" e "não","implicação". Formas normais:satisfazibilidade e validade. Fórmulas em forma normal negativa, normal disjuntiva e normal conjuntiva. Fórmulas em forma normal conjuntiva. . | LC Pag 11-17 | LICS 1.5.1-2 |
| 4 | 9/3 | Fórmulas de Horn. Satisfazibilidade.Cláusulas e conjuntos de cláusulas. . | LC Pag 18-22 | |
| 5 | 13/3 | Algoritmo de Davis-Putnam para a satisfazibilidade de cláusulas.Raciocínios. Consequência lógica. Métodos de dedução axiomáticos. Sistema de dedução natural. Regras de inferência: conjunção e disjunção. Exemplos. . | LC Pag 20-29 | Regras DN P |
| 6 | 15/3 | Sistema de dedução natural. Regras de inferência: negação, falso e implicação. Exemplos.Regras derivadas: dupla negação, modus tollens, redução ao absurdo e terceiro excluído. . | LC Pag 29-35 | Regras DN P |
| 7 | 20/3 | Equivalência dedutiva. Contraposição. Exemplos. Integridade do sistema de dedução natural para a lógica proposicional. . | LC Pag 35-43 | Regras DN P |
| 8 | 27/3 | Completude do sistema de dedução natural para a lógica proposicional. . | LC Pag 43-46 | Regras DN P |
| 9 | 29/3 | Outros sistemas dedutivos. Sistemas dedutivos automáticos. 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. Variáveis ligadas e livres. Proposições . | LC Pag 53-58- | |
| 10 | 10/4 | 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 58-61 | |
| 11 | 12/4 | Satisfazibilidade de fórmulas e de conjuntos de fórmulas, fórmulas válidas, consequência semântica. Veracidade ou falsidade de proposições numa estrutura. Modelos. Caracterização de modelos por proposições. Equivalência semântica. Algumas fórmulas semanticamente equivalentes: leis de Morgan para quantificadores, passagem da negação para o âmbito de quantificadores; distributividade dos quantificadores sobre conectivas. | LC Pag 61-72 | |
| 12 | 17/4 | Substituição de variáveis ligadas; passagem de quantificadores para fora de fórmulas onde a variável ligada não ocorre. Substituições e noção de variável substituível. Forma normal prenexa. Sistema de dedução natural para a lógica de primeira ordem: regras de introdução e eliminação para os quantificadores e a igualdade | LC Pag 72-80 | Regras DN LP |
| 13 | 19/4 | Sistema de dedução natural para a lógica de primeira ordem. Exemplos. Equivalência dedutiva. Integridade do sistema de dedução natural para uma linguagem da lógica de primeira ordem. | LC Pag 76- 84 | Regras DN LP |
| 14 | 24/4 | Teorema da completude. Demonstração do teorema da completude para o sistema dedutivo de dedução natural duma linguagem lógica de primeira ordem. | LC Pag 86-93 | |
| 15 | 26/4 | Axiomatizações e Teorias da lógica de primeira ordem. Axiomas de Peano (PA) Utilização do sistema de dedução natural para a demonstração de teoremas da aritmética. | LC Pag 97-102 | |
| 16 | 3/5 | Objectivos da Programação em lógica. Resolução para a lógica proposicional. Cláusulas de uma linguagem de primeira ordem. Conversão para forma clausal. Fórmulas de Horn: positivas, unitárias e negativas. Programas definidos e objectivos. Exemplos. | slow.pl | |
| 17 | 15/5 | 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. | ||
| 18 | 17/5 | Resolução Geral. Resolução SLD para cláusulas de Horn. Árvores de derivação SLD. Programação em Prolog. Regra de Computação e de Procura. Retrocesso. Bases de conhecimento simples. Caminhos num grafo acíclico dirigido. Fecho transitivo de relações binárias. | YAP |
familia.pl
grafos.pl |
| 19 | 22/5 | Programação em Prolog: programação com listas e uso de acumuladores. | YAP | listas.pl |
| 20 | 24/5 | Programação em Prolog: programação com listas, ordenação. Corte de alternativas: !. Árvores. | YAP | grapc.pl,
cortes.pl trees.pl matriz.pl sort.pl |
| 21 | 29/5 | Entrada e saída. Negação por falha. Estruturas de diferenças: diferença de listas. Manipulação simbólica: funções de uma variável; derivação; simplifição algébrica. Resolução de problemas por geração e teste. Resolução de Puzzles. | YAP | I/O,
Dif. Listas Man. algégrica T. Hanoi Puz. Einstein Puz. Arit |
| 22 | 31/5 | Nondeterminismo: geração e teste. Problema das n rainhas. Coloração de mapas. Predicados sobre conjuntos: findall e all. Modificação da base de dados de cláusulas: assert, retract e abolish. Aplicações: programa para um jogo de "MasterMind". | YAP | n queens, Mapa Master mind |