Return to search

Um estudo do sistema Oyster-Clam, implementação de reescrita de tipos e uma formalização parcial da teoria dos grafos

Orientador: Jacques Wainer / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-07-25T14:49:11Z (GMT). No. of bitstreams: 1
Pellegrini_Jeronimo_M.pdf: 6805368 bytes, checksum: 59cb8230ad8b2216cb3006f776de3d8c (MD5)
Previous issue date: 1997 / Resumo: Nesta tese, mostramos uma implementação do processo de diagonalização de Cantor no sistema de prova de teoremas Oyster-Clam. Para isto, tivemos que estender o Oyster com comparação e indução em tipos, e desenvolvemos um método e algumas regras de reescrita. As regras de reescrita lidam com tipos, o que não era suportado ainda no sistema Oyster-Clam; algumas modificações foram feitas para que isto se tornasse possível. Também desenvolvemos esquemas de indução para grafos neste sistema, e provamos alguns teoremas. / Abstract: In this thesis, we show an implementation of Cantor's digitalization process in the Oyster-Clam theorem proving system. To achieve that, we have extended the Oyster logic with comparison and induction on types, and developed a method and some rewrite rules. The rewrite rules deal with types, what was not supported yet in the Oyster-Clam system, and some modifications were done to make that possible. We have also developed induction schemes for graphs in that system, and some theorems were proven. / Mestrado / Mestre em Ciência da Computação

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.unicamp.br:REPOSIP/275884
Date25 July 2018
CreatorsPellegrini, Jerônimo
ContributorsUNIVERSIDADE ESTADUAL DE CAMPINAS, Wainer, Jacques, 1958-, Silva, Flávio Soares Corrêa da, Moura, Arnaldo Vieira
Publisher[s.n.], Universidade Estadual de Campinas. Instituto de Computação, Programa de Pós-Graduação em Ciência da Computação
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Format65f., application/octet-stream
Sourcereponame:Repositório Institucional da Unicamp, instname:Universidade Estadual de Campinas, instacron:UNICAMP
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0019 seconds