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: O QUE É O ESQUELETO DE UMA DEMONSTRAÇÃO Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO Autor: EDUARDO NAHUM OCHS
Colaborador(es): NICOLAU CORCAO SALDANHA - Orientador
Número do Conteúdo: 4645
Catalogação: 12/03/2004 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
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: O QUE É O ESQUELETO DE UMA DEMONSTRAÇÃO Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO Autor: EDUARDO NAHUM OCHS
Colaborador(es): NICOLAU CORCAO SALDANHA - Orientador
Número do Conteúdo: 4645
Catalogação: 12/03/2004 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
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:
Considere os seguintes dois tipos de transformções em
demonstrações: 1) tornar uma prova mais incompleta,
apagando um lema ou uma construção que sejam parte da prova
e pondo no lugar um aviso dizendo isso é óbvio; 2) pegar um
passo que foi provado por um isso é óbvio, aplicar algum
algoritmo que encontre uma demonstração para esse passo, e
trocar o aviso pela demonstração de verdade. Nós vamos
considerar que a primeira operação vai em direção ao
esqueleto da demonstração, e que ela é como uma projeção;
a segunda operação é um levantamento de um esqueleto para
uma demonstração um pouco mais completa com aquele
esqueleto. Nós só estamos interessados em esqueletos que
possam ser levantados até provas completas usando algum
algoritmo conhecido. Nesta tese descrevemos uma linguagem -
o sistema DNC - que permite provar vários fatos sobre
categorias usando esqueletos. O método para o levantamento
é, a grosso modo, o seguinte: a partir do nome de um termo
em DNC nós podemos obter o seu tipo; por uma espécie de
Isomorfismo de Curry-Howard um tipo desses pode ser visto
como uma preposição numa certa lógica; um algoritmo que
obtenha uma demonstração para essa proposição retorna uma
árvore de demonstração (uma derivação) num certo sistema de
Dedução Natural, e essa árvore pode ser lida como um lambda-
termo do tipo dado - ela dá uma construção natural para um
objeto daquele tipo, e esse objeto muito frequentemente é
exatamente o objeto que esperávamos obter. Derivações em
DNC podem ser traduzidas para derivações num Pure Type
System com Dicionários (PTSD), e derivações em PTSDs podem
ser traduzidas para derivações em Pure Type Systems (PTSs);
daí, questões sobre a teoria da prova de DNC se tornam
questões sobre a teoria da prova de PTSs, que é bastante
bem-conhecida. Não só temos um levantamento de nomes de
termos em DNC para provas completas, mas também temos um
modo formal de levantar diagramas categóricos expressos na
linguagem do DNC para termos em DNC e daí para provas
completas; e se mudamos o dicionário embutido num PTSD
podemos fazer com que o mesmo esqueleto em DNC represente
provas em contextos diferentes; por exemplo, algumas provas
que aparentemente estão sendo feitas sobre a categoria dos
conjuntos podem ser reinterpretados como provas sobre um
topos arbitrário. Usamos essa idéia para apresentar de uma
forma simples - em que os passos óbvios omitidos são óbvios
num sentido muito preciso - a semântica categárica para
alguns PTSs, incluindo PTSs com polimorfismo e tipos
dependentes, e os PTSs para quais as derivações em DNC são
traduzidas.
Descrição | Arquivo |
CAPA, AGRADECIMENTOS, RESUMO, ABSTRACT E SUMÁRIO |
PDF ![]() |
INTRODUÇÃO |
PDF ![]() |
CAPÍTULO 1 |
PDF ![]() |
CAPÍTULO 2 |
PDF ![]() |
CAPÍTULO 3 |
PDF ![]() |
REFERÊNCIAS BIBLIOGRÁFICAS |
PDF ![]() |