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

• Main Author: Pellegrini, Jerônimo
• Other Authors: UNIVERSIDADE ESTADUAL DE CAMPINAS
• Format: Others
• Language: Portuguese
• Published: [s.n.] 1997
• Subjects: Demonstração automática de teoremas; Lógica simbólica e matemática; Inteligência artificial
• Online Access: PELLEGRINI, Jerônimo. Um estudo do sistema Oyster-Clam, implementação de reescrita de tipos e uma formalização parcial da teoria dos grafos. 1997. 65f. Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação, Campinas, SP. Disponível em: <http://www.repositorio.unicamp.br/handle/REPOSIP/275884>. Acesso em: 25 jul. 2018.; http://repositorio.unicamp.br/jspui/handle/REPOSIP/275884

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