XINFORMAÇÕES SOBRE DIREITOS AUTORAIS
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital
Título: INFRASTRUCTURE FOR WEB-BASED INTERACTIVE THEOREM PROVERS Autor: JEFFERSON DE BARROS SANTOS
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ADVISOR
Nº do Conteudo: 16318
Catalogação: 27/09/2010 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: 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.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.16318
Resumo:
Título: INFRASTRUCTURE FOR WEB-BASED INTERACTIVE THEOREM PROVERS Autor: JEFFERSON DE BARROS SANTOS
Nº do Conteudo: 16318
Catalogação: 27/09/2010 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: 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.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@2
Referência 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 | |
CHAPTER 1 | |
CHAPTER 2 | |
CHAPTER 3 | |
CHAPTER 4 | |
CHAPTER 5 | |
CHAPTER 6 | |
REFERENCES |