Logo PUC-Rio Logo Maxwell
ETDs @PUC-Rio
Estatística
Título: INFRASTRUCTURE FOR WEB-BASED INTERACTIVE THEOREM PROVERS
Autor: JEFFERSON DE BARROS SANTOS
Colaborador(es): EDWARD HERMANN HAEUSLER - Orientador
Catalogação: 27/SET/2010 Língua(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
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=16318&idi=1
[en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=16318&idi=2
DOI: https://doi.org/10.17771/PUCRio.acad.16318
Resumo:
Automatic theorem proving consists of proving mathematical theorems by means of computer programs. Depending on the logic used, the process of proving a formula is not computable. Moreover, depending of the deductive system applied to, the search for a proof can involve the application of long sequences of axioms and inference rules, reinforcing the need of human intervention in the proof process. Such systems are known as interactive theorem provers or proof assistants. In a typical scenario, the user interacts with the prover through a graphical interface, usually a desktop application. Recently, however, applications like those started to be delivered to users through the web. This way of software deployment avoids that final users have to deal with complex activities like prover installation and configuration and allows this user to access the system from different machines with a simple Internet connection. In this research we study the use of web as a platform for interactive theorem proving environments construction. Our purpose is to study some interaction models between user and automated proof environments and verify how these models can be adapted to work as a web application. As a result we show a graphical tool for visualization and direct manipulation of formal proofs on web to work as an alternative interface between user and proving machines.
Descrição: Arquivo:   
COVER, ACKNOWLEDGEMENTS, RESUMO, ABSTRACT, SUMMARY AND LISTS PDF    
CHAPTER 1 PDF    
CHAPTER 2 PDF    
CHAPTER 3 PDF    
CHAPTER 4 PDF    
CHAPTER 5 PDF    
CHAPTER 6 PDF    
REFERENCES PDF