Plano de ensino
Lógica Computacional 1 - 2020-2

O objetivo geral do curso de Lógica Computacional 1 é compreender como a lógica de primeira ordem é importante para a resolução de problemas computacionais.

Os objetivos específicos são:

• Compreender os fundamentos da lógica proposicional (intuicionista e clássica);
• Compreender os fundamentos da lógica de predicados (intuicionista e clássica);
• Compreender diferentes métodos de validação de teoremas e programas.

• Noções básicas
  • Linguagem natural vs linguagens formais
  • Verdade, validade e satisfatibilidade
  • Lógica proposicional
    • Sintaxe e semântica
    • Propriedades e relações semânticas
    • Consequência lógica
    • Simplificação de fórmulas
  • Lógica de Primeira Ordem
    • Sintaxe e semântica
    • Propriedades e relações semânticas
  • Formas normais
• Métodos de validação
  • Métodos diretos de prova
  • Métodos de prova por contradição
• Linguagens para experimentação
  • Aplicações básicas

O conteúdo será abordado por meio de atividades:

1. Leituras dirigidas que serão disponibilizadas na página web da disciplina¹ e/ou na plataforma Microsoft Teams institucional;
2. Assíncronas (videoaulas) que ficarão disponíveis na plataforma Youtube, e cujos links serão disponibilizados na página web da disciplina¹ e/ou na plataforma Microsoft Teams institucional;
3. Síncronas (aulas virtuais) via a plataforma Microsoft Teams institucional.

O curso é dividido em dois grandes blocos:

1. Lógica proposicional (LP);
2. Lógica de Primeira Ordem (LPO) (ou Lógica de Predicados).

Cada um destes blocos é dividido em vários tópicos compostos de:

• Material de leitura sobre o tópico;
• Uma videoaulas e/ou aula virtual sobre o tópico;
• Atividades sobre o tópico.

A plataforma institucional Microsoft Teams será utilizada para troca de mensagens e discussão de dúvidas.

A avaliação será composta das seguintes partes:

1. Atividades individuais a serem enviadas em prazo determinado.
   1. Serão 29 atividades, cada uma valendo 2 pontos, perfazendo um total de 58 pontos.
   2. Cada atividade individual será contabilizada como uma frequência, se enviada no prazo determinado, e contabilizada como falta da aula correspondente, se enviada com atraso ou se não for enviada.
   3. A pontuação de cada uma das 29 atividades será contabilizada como a seguir:
      • até 2 pontos, se enviada no prazo determinado;
      • até 1 ponto, se enviada até 24 horas depois do prazo determinado;
      • 0, nas outras situações.
   4. As atividades individuais que não tenham sido realizadas por alguma razão amparada por lei poderão ser repostas no final do semestre por meio de uma avaliação envolvendo todo o conteúdo do semestre.
2. Uma monografia (a ser feita individualmente ou em dupla) a ser enviada em formato pdf em prazo determinado, perfazendo um total de 12 pontos.
3. Uma formalização (a ser feita individualmente ou em dupla) a ser feita no assistente de provas Coq, com prazo determinado, perfazendo um total de 30 pontos. Esta formalização será composta de duas etapas a serem descritas posteriormente.

Para ser aprovado o aluno deve cumprir simultaneamente os seguintes itens:

• Frequência maior ou igual a 75%;
• Obter pelo menos 50 pontos considerando as três partes da avaliação do curso como descrito acima.

A menção final é definida como a seguir:

O texto principal da leitura dirigida será disponibilizado na página web da disciplina¹ e/ou na plataforma Microsoft Teams institucional, assim como os links para outras referências que estiverem livremente disponíveis na internet.

A referência principal do curso é o livro: cite:ayala-rinconAppliedLogicComputer2017

As referências complementares são: cite:huthLogicComputerScience2004,silvaLogicaParaComputacao2006,smullyanLogicalLabyrinths2009,schoningLogicComputerScientists2008,nederpeltLogicalReasoningFirst2004,dalenLogicStructure2013,ebbinghausMathematicalLogic1984,caicedoElementosLogicaCalculabilidad1983,boolosdComputabilityLogic4th2002,burrisLogicMathematicsComputer1998.

bibliographystyle:unsrt bibliography:/Users/flaviomoura/Dropbox/org/zotLib.bib