MATA47

Lógica para a Computação

MATA47 faz parte da lista de disciplinas da área de Fundamentos e Teoria da Computação que aborda os aspectos teóricos fundamentais para a Ciência da Computação. Nesta disciplina, abordamos alguns resultados fundamentais sobre representabildiade de conjuntos e funções através de sistemas formais finitários e suas conexões com a Álgebra, a Combinatória, a Lógica, entre outros. São tópicos concernentes a essa disciplina: linguagens formais, autômatos, Expressões RegularesDeseja-se com essa disciplina desenvolver as seguintes habilidades:

  • Manipular as linguagens e ferramentais da Matemática Discreta
  • Manipular representações formais de objetos através de procedimentos computacionais
  • Representar procedimentos computacionais através de manipulação formal de símbolos
  • Estabelecer conexões entre a teoria dos algoritmos e complexidade computacional e suas representações teóricas na Teoria das Linguagens Formais

Programa

Ementa

Técnicas de demonstração. Conceito de Lógica: sintaxe, semântica. Propriedades da lógica clássica. Lógica Proposicional e de Primeira Ordem. Métodos dedutivos como: axiomático, dedução natural, cálculo de seqüentes, tableaux, resolução. Conceito de correção e completeza. Aplicações da lógica.

Objetivos

Ao final da disciplina, os estudantes possuem conhecimento sólido de conceitos centrais da Lógica Proposicional e da Lógica de Predicados com enfoque em algumas das aplicações de lógica na área de Ciência da Computação. Os alunos estarão aptos a desenvolver demonstrações formais, a usar lógica para a formalização de fatos e de raciocínio, e a lidar com sistemas dedutivos.

Conteúdo Programático

  1. Lógica Proposicional
    1. Princípios fundamentais da lógica clássica
    2. A hierarquia de Chomsky
    3. Sintaxe: alfabeto e fórmulas, prova por indução nas fórmulas
    4. Semântica: valores verdade, valorações, tabelas verdade
    5. Noções semânticas básicas: modelo, satisfatibilidade, contradição e validez, consequência lógica, equivalência lógica
    6. Bases de conectivos
    7. Formas normais: forma normal disjuntiva, forma normal conjuntiva, fórmulas de Horn
    8. Sistemas dedutivos
      1. Cálculo de Hilbert (ou cálculo de sequentes ou Dedução Natural ou método de tableaux ou ...)
      2. A noção da dedução (derivação, prova) no cálculo, corretude do cálculo
      3. Consistência, inconsistência, conjuntos maximalmente consistentes, teorema de Lindenbaum
      4. Teorema da completude, teorema da compacidade
    9. Resolução: a regra da resolução, o cálculo da resolução, corretude e completude (teorema da resolução)
  2. Lógica de Predicados
    1. Alfabeto, assinaturas e linguagens.
    2. Estruturas sobre uma dada assinatura, (homomorfismos e isomorfismos, subestruturas, expansões)
    3. Sintaxe da Lógica de Predicados: termos, fórmulas, prova por indução em termos e fórmulas, substituições
    4. Semântica: interpretações, modelos, lema da coincidência, (lema de subestruturas), substituições, teoremasubstituição
    5. Consequência lógica, equivalência lógica, formalizações, axiomatizações e teorias
    6. Formas normais: forma prenexa e de Skolem, forma normal conjuntiva e disjuntiva
    7. Teoria de Herbrand: universos e modelos de Herbrand, teorema de Goedel-Herbrand-Skolem, teorema Herbrand, algoritmo de Gilmore e semi-decidibilidade da Lógica de Predicados, (indecidibilidade da Lógica Predicados)
    8. Sistemas dedutivos na lógica de predicados (p.ex.: cálculo de Hilbert, cálculo de sequentes, ...), corretude cálculo
    9. Teorema da completude (ideias principais da demonstração)
    10. Introdução à resolução na Lógica de Predicados

Bibliografia

  1. INTRODUÇÃO À TEORIA DA COMPUTAÇÃO. MICHAEL SIPSER. 2a EDIÇÃO NORTE AMERICANA. THOMSON
  2. Linguagens Formais: Teoria, Modelagem e Implementação. Marcus Vinícius Midena Ramos, João José Neto, Ítalo Santiago Vega. Editora Bookman. 2009
  3. Compiladores : princípios e práticas. LOUDEN, Kenneth C. São Paulo: Thomson Pioneira, 2004.
  4. Introdução à Teoria de Autômatos, Linguagens e Computação. John E. Hopcroft, Jeffery D. Ullman; Rajeev Motwani. Tradução da segunda edição americana. Editora Campus. 2003.
  5. Linguagens Formais e Autômatos. Paulo Blauth Menezes. Editora Sagra Luzzatto. Série Livros Didáticos – Instituto de Informática da UFRGS.
  6. ELEMENTOS DE TEORIA DA COMPUTAÇÃO (ORIGINAL: ELEMENTS OF THE THEORY OF COMPUTATION. PRENTICE-HALL, INC., 1998). HARRY R. LEWIS, CHRISTOS H. PAPADIMITRIOU. EDITORA BOOKMAN.
  7. Machines, Languages and Computation. Peter J. Denning; Jack B. Dennis; Joseph E. Qualitz. Prentice-Hall. 1978.
  8. Compilers: Principles, Techniques, and Tools. Alfred V., Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman. Addison Wesley; 2nd edition, 2008.