Título
[en] EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS
Título
[pt] EXTRAÇÃO DE CONTEÚDO COMPUTACIONAL DE PROVAS INTUICIONISTAS
Autor
[pt] GEIZA MARIA HAMAZAKI DA SILVA
Vocabulário
[pt] SINTESE DE PROGRAMAS
Vocabulário
[pt] DEDUCAO NATURAL
Vocabulário
[pt] LOGICA INTUICIONISTA
Vocabulário
[en] PROGRAM SYNTHESIS
Vocabulário
[en] NATURAL DEDUCTION
Vocabulário
[en] INTUITIONISTIC LOGIC
Resumo
[pt] Garantir que programas são implementados de forma a
cumprir uma especificação é uma questão fundamental em
computação, por isso, têm sido propostos vários métodos
que almejam provar a correção dos programas. Este
trabalho apresenta um método, baseado no isomorfismo de
Curry-Howard, que extrai conteúdos computacionais de
provas intuicionistas, conhecido como síntese construtiva
ou proofs-as-programs. É proposto um processo de síntese
construtiva de programas, onde a extração do conteúdo
computacional gera um programa em linguagem imperativa a
partir de uma prova em lógica intuicionista poli-sortida,
cujos axiomas definem os tipos abstratos de dados, sendo
utilizado como sistema dedutivo a Dedução Natural. Também
é apresentada uma prova de correção, bem como uma prova
de completude do método atráves do uso de um sistema com
regra ômega (computacional) para a aritmética de Heyting,
concluindo com uma demonstração da relação entre o uso da
indução finita no lugar da regra ômega computacional no
processo de síntese.
Resumo
[en] One of the main problems in computer science is to assure
that programs are implemented in such a way that they
satisfy a given specification. There are many studies about
methods to prove correctness of programs. This work
presents a method, belonging to the constructive synthesis
or proofs-as-programs paradigm, that comes from the Curry-
Howard isomorphism and extracts the computational contents
of intuitionist proofs. The synthesis process proposed
produces a program in an imperative language from a proof
in many-sorted intuitionist logic, where the axioms define
the abstract data types using Natural Deduction as
deductive system. It is proved the correctness, as well as
the completeness of the method regarding the Heyting
arithmetic with ômega-rule(in its computational version). A
discussion about the use of the finitary induction instead
of computational ômega-rule concludes the work.
Orientador(es)
EDWARD HERMANN HAEUSLER
Banca
EDWARD HERMANN HAEUSLER
Banca
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
PAULO AUGUSTO SILVA VELOSO
Banca
MARCELO ESTEBAN CONIGLIO
Banca
MAURICIO AYALA RINCON
Catalogação
2004-09-10
Apresentação
2004-03-26
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
PORTUGUÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.5443
Arquivos do conteúdo
CAPA, AGRADECIMENTOS, RESUMO, ABSTRACT, SUMÁRIO E LISTAS PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF CAPÍTULO 5 PDF CAPÍTULO 6 PDF BIBLIOGRAFIA E APÊNDICES PDF