Mostrar registro simples

[pt] EXTRAÇÃO DE CONTEÚDO COMPUTACIONAL DE PROVAS INTUICIONISTAS

dc.contributorEDWARD HERMANN HAEUSLER
dc.creatorGEIZA MARIA HAMAZAKI DA SILVA
dc.date2004-09-10
dc.date.accessioned2022-09-21T21:44:05Z
dc.date.available2022-09-21T21:44:05Z
dc.identifierhttps://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@1
dc.identifierhttps://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@2
dc.identifierhttp://doi.org/10.17771/PUCRio.acad.5443
dc.identifier.urihttps://hdl.handle.net/20.500.12032/42875
dc.description[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.
dc.description[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.
dc.languagept
dc.publisherMAXWELL
dc.subject[pt] SINTESE DE PROGRAMAS
dc.subject[pt] DEDUCAO NATURAL
dc.subject[pt] LOGICA INTUICIONISTA
dc.subject[en] PROGRAM SYNTHESIS
dc.subject[en] NATURAL DEDUCTION
dc.subject[en] INTUITIONISTIC LOGIC
dc.title[en] EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS
dc.title[pt] EXTRAÇÃO DE CONTEÚDO COMPUTACIONAL DE PROVAS INTUICIONISTAS
dc.typeTEXTO


Arquivos deste item

ArquivosTamanhoFormatoVisualização

Não existem arquivos associados a este item.

Este item aparece na(s) seguinte(s) coleção(s)

Mostrar registro simples


© AUSJAL 2022

Asociación de Universidades Confiadas a la Compañía de Jesús en América Latina, AUSJAL
Av. Santa Teresa de Jesús Edif. Cerpe, Piso 2, Oficina AUSJAL Urb.
La Castellana, Chacao (1060) Caracas - Venezuela
Tel/Fax (+58-212)-266-13-41 /(+58-212)-266-85-62

Nuestras redes sociales

facebook Facebook

twitter Twitter

youtube Youtube

Asociaciones Jesuitas en el mundo
Ausjal en el mundo AJCU AUSJAL JESAM JCEP JCS JCAP