Título: Matemática feita no computador: Estudos sobre uma coleção de sistemas formais, com uma investigação sobre estruturas indutivas, e a separação entre lógica e automação em assistentes de prova.

Data: 24/05/2018 Horário: 13:00h Local: Sala de Reuniões – Bloco 910

Resumo:

A ciência da computação possui forte ligação com a lógica, a área da matemática responsável por tratar da prova de teoremas em toda sua generalidade e formalidade. Como fruto moderno dessa ligação, nós destacamos em particular os assistentes de provas, programas de computador que disponibilizam a seus usuários diversas ferramentas para o auxílio na confecção de provas e teoremas, desde a verificação sintática de afirmações, a buscas automáticas por demonstrações de teoremas. No entanto, poucas são as áreas da matemática que fazem uso destes assistentes. Na matemática, o computador ainda é em grande parte usado apenas pela sua capacidade de calcular. Tais assistentes de prova hoje encontram público na comunidade de cientistas da computação que precisam de maior confiança em seus programas. Nesse contexto, a questão natural que se coloca é: O que falta para que os assistentes de prova se tornem mais atraentes para os matemáticos? Ou, em outras palavras, de que maneira os recursos computacionas podem ser colocados a serviço da construção de provas matemáticas? Este é um problema nada trivial. Mesmo a discussão de possíveis soluções requer um conhecimento técnico extensivo sobre como tais recursos computacionais são introduzidos nos assistentes de provas atuais. Nesse sentido, a maior parte do corpo deste trabalho consiste na revisão de uma sequência de sistemas formais, com o objetivo de observar o crescimento da matemática que pode ser expressa nesses sistemas, e o crescimento da automação embutida neles. Como contribuição nossa, esboçamos um sistema formal onde computação fica separada dos aspectos lógicos, e dedicada exclusivamente à tarefa de automação. Nós utilizamos este esboço para expressar um recurso computacional inovador, baseado em estruturas indutivas, derivado do estudo anterior feito sobre a sequência de sistemas formais.

Banca:

• Prof. Dr. Carlos Eduardo Fisch de Brito (MDCC/UFC - Orientador)
• Prof. Dr. Ruy José Guerra Barretto de Queiroz (UFPE)
• Prof. Dr. Pablo Mayckon Silva Farias (UFC)
• Prof. Dr. João Fernando Lima Alcântara (MDCC/UFC)