[pt] INFRAESTRUTURA PARA PROVADORES INTERATIVOS DE TEOREMAS NA WEB

• Ano de defesa: 2010
• Autor(a) principal: JEFFERSON DE BARROS SANTOS
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] WEB; [pt] INTERFACE GRAFICA; [pt] PROVA DE TEOREMAS; [en] WEB; [en] GRAPHIC INTERFACE; [en] THEOREM PROVING
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318&idi=2; http://doi.org/10.17771/PUCRio.acad.16318

[pt] Prova automática de teoremas consiste na prova de teoremas matemáticos por intermédio de programas de computador. Dependendo da linguagem lógica em uso, o processo de provar uma determinada fórmula pode não ser computável. Além disso, dependendo do cálculo dedutivo empregado, a busca por uma prova envolve lidar com a possibilidade de aplicação de longas sequências de axiomas e regras de inferência. Tudo isso reforça a necessidade da intervenção humana no processo de prova em sistemas denominados provadores interativos de teoremas ou assistentes de prova. Em um cenário típico, um usuário interage com a máquina de prova através de uma interface gráfica, normalmente implementada como um aplicativo desktop. Recentemente, porém, muitos aplicativos deste tipo passaram a ser oferecidos para seus usuários através da web. Esta forma de disponibilizar software evita que o usuário final se preocupe com questões de instalação e configuração e possibilita o acesso ao sistema de qualquer computador, com qualquer sistema operacional, bastando ter disponível uma conexão com a Internet. Nesta dissertação, estudamos possibilidades de uso da web como plataforma para a construção de ambientes interativos para prova de teoremas. Nossa proposta é estudar os diferentes modelos de interação entre usuário e ambientes de prova automatizados e verificar como estes modelos podem ser adaptados para a web. Como resultado, apresentamos uma ferramenta gráfica para visualização e manipulação direta de provas formais na web como uma interface alternativa entre usuários e provadores.