MAC0435  Métodos Formais para Especificação e Construção de Programas

OBJETIVOS:  Apresentar os fundamentos lógicos e preparar os alunos para o estudo, uso e desenvolvimento de técnicas formais para especificação, construção e análise de programas.

PROGRAMA:  Serão abordados tópicos dentre os seguintes: Lógica Clássica: conceitos fundamentais; teoria de demonstrações; métodos de formalização de provas; sistemas de Hilbert, Gentzen, Smullyan, etc.  Lógicas Não-Clássicas: lógicas sub-estruturais; lógicas lineares; semântica de processos computacionais via lógicas lineares; lógicas modais clássicas; lógicas modais temporais; especificação, construção e análise de programas via lógicas temporais; lógicas multimodais; especificação e análise de sistemas distribuídos via lógicas multimodais.

PRÉ-REQUISITO NÃO-OFICIAL:  MAT0359.

CARGA HORÁRIA SEMANAL E NÚMERO DE CRÉDITOS:  4 horas, 4 créditos-aula.

CRITÉRIO DE AVALIAÇÃO DA APRENDIZAGEM:  Média ponderada de notas de provas, exercícios e programas.

BIBLIOGRAFIA BÁSICA: 

• E. Mendelson, Introduction to Mathematical Logic, Editora?, 19??.
• N. Wansing, The Logic on Information Structures, Editora?, 19??.
• Z. Manna, A. Pavelli, The Temporal Logic of Reactive and Concurrent Systems, Editora?, 19??.
• R. Fagin et alii, Reasoning about Knowledge, Editora?, 19??.

OBSERVAÇÃO:  Disciplina optativa eletiva no currículo do BCC.

[Veja dados da disciplina no JúpiterWeb]