Lógica computacional

• Processo: 06/52389-5
• Modalidade de apoio: Bolsas no Brasil - Iniciação Científica
• Data de Início da vigência: 01 de julho de 2006
• Data de Término da vigência: 31 de dezembro de 2006
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Teoria da Computação
• Pesquisador responsável: Arnaldo Vieira Moura
• Beneficiário: Davi de Melo Jorge Barbosa
• Instituição Sede: Instituto de Computação (IC). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil
• Assunto(s): Programação lógica Lógica computacional
• Palavra(s)-Chave do Pesquisador: Bdd | Logica | Logica Computacional | Model Checking

Resumo

O projeto visa um estudo sobre lógica computacional, abrangendo toda a base de lógica matemática necessária (lógica proposicional, lógica de predicados e equações e lógica de primeira ordem), os modelos de lógica com aplicações na computação (LTL, CTL, CTL') e a aplicação desses modelos para a verificação de sistemas. O projeto visa, ainda, a redação e disponibilização de uma monografia sobre esse material. A monografia deverá ser rica em exercícios resolvidos e será redigida com o objetivo de ser utilizada como material didático em disciplinas que serão criadas pelo Instituto de Computação da Unicamp, mas poderá ser utilizada por qualquer aluno de computação ou qualquer entusiasta da lógica. (AU)