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.

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; validade, satisfazibilidade e contradição. Consequência e equivalência semântica.

Funções de verdade (ou Booleanas). 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.

Fórmulas de Horn. Satisfazibilidade. Cláusulas e
conjuntos de cláusulas. Algoritmo de Davis-Putnam para a
satisfazibilidade de cláusulas.

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.

Sistema de dedução natural. Regras de inferência: negação e falso. Exemplos.

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.

Integridade e Completute de sistemas de dedução: integridade do sistema DN de dedução natural.

Integridade e Completute de sistemas de dedução: completude do sistema DN de dedução natural. Decidibilidade da lógica proposicional.

Outros sistemas dedutivos. Sistemas dedutivos analíticos (automáticos). Tableaux semânticos: regras, expansão e tabieaux fechados. Integridade e Completude dos tableaux semânticos. Resolução: integridade.

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.

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 (cont.). Exemplos.

Satisfabilidade, validade, e consequência semântica. Modelos para proposições. Caracterização de estruturas por fórmulas da lógica de primeira ordem. Digrafos e Autómatos finitos como estruturas.

Equivalência Semântica. 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.

Sistema de dedução natural para lógica de primeira ordem: regras de introdução e eliminação da igualdade e quantificadores universal e existencial. Exemplos.

Sistema de dedução natural para lógica de primeira ordem (cont.). Equivalência dedutiva.Exemplos. Integridade do sistema de dedução natural para lógica de primeira ordem.

Completude do sistema de dedução natural para lógica de primeira ordem.

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. Axiomatizações.

Axiomatizações. Axiomas para a teoria dos conjuntos. Axiomas de Peano para a aritmética. Breve referência à incompletude dos axiomas de Peano e à indecidibilidade da Lógica de primeira ordem.

Breve referencia a teorias recidiveis da LPO e resolutores.
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.

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.

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. Satisfaziibilidade de Cláusulas. Modelos de Herbrand. Modelo mínimo de Herbrand.

Resolução SLD para cláusulas de Horn. Árvores de derivação SLD. Exemplo de um programa em Prolog.