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: WHAT IS SKELETON OF A PROOF Autor: EDUARDO NAHUM OCHS
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
NICOLAU CORCAO SALDANHA - ADVISOR
Nº do Conteudo: 4645
Catalogação: 12/03/2004 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=4645@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4645@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.4645
Resumo:
Título: WHAT IS SKELETON OF A PROOF Autor: EDUARDO NAHUM OCHS
Nº do Conteudo: 4645
Catalogação: 12/03/2004 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=4645@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4645@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.4645
Resumo:
Consider the following two kinds of transformation on
proofs; the first is to make a a proof more incomplete, by
erasing a lemma or a construction from it and replacing it
by a tag saying this is obvious; the second kind of
transformation takes a step that is proved by a this is
obvious tag, applies some kind of prof-search algorithm to
it, and replaces the tag by a real proof for that step. We
will consider that the first operation goes toward the
skeleton towards a more complete proof that had that
skeleton as a projection. We are only interested in
skeletons can be lifted back to full proofs using some
known algorithm. In this thesis we can describe a language -
DNC - that lets us prove several categorical facts using
skeletons. The method for lifting these skeletons goes like
this: from the name of a DNC term we can obtain its type;
by a kind of Curry-Howard isomorphism a such type can be
seen as a proposition in a certain logic; proof-search for
that proposition will obtain a proof-tree for it in a
certain system of Natural Deduction, and that proof-tree
can be read as a lambda-term of given type - the proof-tree
gives a natural construction for an object of the given
type, that very often is exactly the object that we were
looking for. Derivations in DNC can be translated into
derivations in a Pure Type System with Dictionaries (PTSD),
and derivations in PTSDs can be translated into derivations
in Pure Type Systems (PTSs); so questions about the proof-
theory of DNC become questions about the proof-theory of
PTSs, whose properties are quite well-known. Also, not only
we can lift names of terms in DNC to full proofs in
different settings; for example, some proofs that
apparently are happening over the category of sets can be
reinterpreted as proofs over an arbitrary topos. We use
that idea to give a simple presentation (in which the
omitted obvious steps are obvious in a very precise sense)
of the categorical semantics for some PTSs - and that
includes PTSs into which the DNC derivations are translated.
Descrição | Arquivo |
COVER, ACKNOWLEDGEMENTS, RESUMO, ABSTRACT AND SUMMARY | |
INTRODUCTION | |
CHAPTER 1 | |
CHAPTER 2 | |
CHAPTER 3 | |
REFERENCES |