MAT 2 02 - Lógica Computacional

Regente

Professor Doutor Eduardo Fermé

Objectivos

Introdução à problemática dos sistemas formais (lógicos) e principais conceitos associados. Cálculo proposicional e do cálculo de predicados: linguagem, semântica, sistemas dedutivos à Hilbert, Tableaux, dedução natural e cálculo de sequentes. Resolução e sua aplicação a programação em Logica. Breve introducção a Logica Modal.

Sinopse

Módulo 1: Cálculo proposicional A noção de sistema formal: linguagem, semântica e axiomatização. Definições indutivas. O caso do cálculo proposicional. Tabelas de verdade. Tautologias. Formas normais. Conjuntos adequados de conectivos. A noção de inferência semântica. Uma axiomatização (à Hilbert) para o cálculo proposicional. Provas e derivações. O metateorema da dedução. Correcção, coerência e adequação/completude da axiomatização. "Tableaux", Dedução Natural e Cálculo de Sequentes para o cálculo proposicional. Módulo 2: Cálculo de predicados Linguagens de 1ª ordem e sua semântica. A noção de de termo livre para uma variável numa fórmula; a noção de instância de uma tautologia. Interpretação, valoração e validade. Cálculo de predicados: uma axiomatização (à Hilbert), sua correcção e coerência. Metateorema da dedução. Metateoremas da equivalência e substituição. Adequação/completude da axiomatização proposta. Modelos. Teorema de Lowenheim-Skolem e teorema da compacidade. "Tableaux", Dedução Natural e Cálculo de Sequentes para o cálculo de predicados. Modulo 3: Introdução à lógica clausal. Semântica declarativa: estruturas de interpretação, pontos fixos, modelos de Herbrand. Semântica operacional: resolução SLD, correcção e adequação. Procedimentos de refutação. Programação em lógica: PROLOG. Modulo 4: Introdução a Lógica modal normal proposicional. Introdução a Lógica modal normal de 1ra Ordem. Axiomas, fórmulas de Barcan.