ETDs @PUC-Rio
| Título: | FORMALIZAÇÃO DE ALGORITMOS DE CRIPTOGRAFIA EM UM ASSISTENTE DE PROVAS INTERATIVO | ||||||||||||
| Autor: |
GUILHERME GOMES FELIX DA SILVA |
||||||||||||
| Colaborador(es): |
EDWARD HERMANN HAEUSLER - Orientador |
||||||||||||
| Catalogação: | 13/DEZ/2018 | Língua(s): | PORTUGUÊS - BRASIL |
||||||||||
| Tipo: | TEXTO | Subtipo: | TESE | ||||||||||
| Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||
| Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=35851&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=35851&idi=2 |
||||||||||||
| DOI: | https://doi.org/10.17771/PUCRio.acad.35851 | ||||||||||||
| Resumo: | |||||||||||||
|
Ao descrever-se a prova de um teorema, é fundamental que haja cautela para que esta não contenha erros ou inconsistências. Para provas muito longas, no entanto, a detecção de erros pode tornar-se uma tarefa humanamente inviável. Um assistente de provas é um programa cuja finalidade é realizar esta detecção de erros para um usuário de forma eficiente, bem como facilitar a construção e compreensão de provas complexas a partir de outras já existentes. O Lean Theorem Prover, desenvolvido em 2012 por Leonardo de Moura, é um assistente de provas que trabalha com descrição de provas através de uma linguagem computacional compilável. Propomos aqui uma descrição no Lean Theorem Prover das provas de funcionamento de diversos algoritmos pertinentes à área de criptografia.
|
|||||||||||||
|
|||||||||||||