Uma formalização da teoria de reescrita em linguagem de ordem superior
Wedi'i Gadw mewn:
| Prif Awdur: | |
|---|---|
| Dyddiad Cyhoeddi: | 2008 |
| Fformat: | Doctoral thesis |
| Iaith: | por |
| Ffynhonnell: | Repositório Institucional da UnB |
| Download full: | http://repositorio.unb.br/handle/10482/1343 |
Crynodeb: | Tese(doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2008. |
| _version_ | 1871442600238514176 |
|---|---|
| author | Galdino, André Luiz |
| author_browse | Galdino, André Luiz |
| author_facet | Galdino, André Luiz |
| author_role | author |
| bitstream.checksum.fl_str_mv | ea02527f0563d16fc5b1df77c3f6f722 4b42614877acda4ce615b4cc029292a8 ff06cb235a3616a0c2e8a878e1c6da3d |
| bitstream.checksumAlgorithm.fl_str_mv | MD5 MD5 MD5 |
| bitstream.url.fl_str_mv | http://repositorio.unb.br/bitstream/10482/1343/1/2008_AndreLuizGaldino.pdf http://repositorio.unb.br/bitstream/10482/1343/2/license.txt http://repositorio.unb.br/bitstream/10482/1343/3/2008_AndreLuizGaldino.pdf.txt |
| collection | Repositório Institucional da UnB |
| contributor_str_mv | Ayala-Rincón, Mauricio |
| dc.contributor.advisor1.fl_str_mv | Ayala-Rincón, Mauricio |
| dc.contributor.author.fl_str_mv | Galdino, André Luiz |
| dc.date.accessioned.fl_str_mv | 2009-02-26T15:02:00Z |
| dc.date.available.fl_str_mv | 2009-02-26T15:02:00Z |
| dc.date.issued.fl_str_mv | 2008 |
| dc.date.submitted.none.fl_str_mv | 2008 |
| dc.identifier.citation.fl_str_mv | GALDINO, André Luiz. Uma formalização da teoria de reescrita em linguagem de ordem superior. 2008. 143 f. Tese (Doutorado em Matemática)-Universidade de Brasília, Brasília, 2008. |
| dc.identifier.uri.fl_str_mv | http://repositorio.unb.br/handle/10482/1343 |
| dc.language.iso.fl_str_mv | por |
| dc.rights.driver.fl_str_mv | info:eu-repo/semantics/openAccess |
| dc.source.none.fl_str_mv | reponame:Repositório Institucional da UnB instname:Universidade de Brasília (UnB) instacron:UNB |
| dc.subject.keyword.pt_BR.fl_str_mv | Algoritmos Teoria de Reescrita de Termos Análise matemática |
| dc.title.pt_BR.fl_str_mv | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| dc.type.driver.fl_str_mv | info:eu-repo/semantics/doctoralThesis |
| dc.type.status.fl_str_mv | info:eu-repo/semantics/publishedVersion |
| description | Tese(doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2008. |
| eu_rights_str_mv | openAccess |
| format | doctoralThesis |
| id | UNB_ee44ebc5c8d3c7af2b85e5d39f75c388 |
| identifier_str_mv | GALDINO, André Luiz. Uma formalização da teoria de reescrita em linguagem de ordem superior. 2008. 143 f. Tese (Doutorado em Matemática)-Universidade de Brasília, Brasília, 2008. |
| instacron_str | UNB |
| institution | UNB |
| instname_str | Universidade de Brasília (UnB) |
| language | por |
| network_acronym_str | UNB |
| network_name_str | Repositório Institucional da UnB |
| oai_identifier_str | oai:repositorio.unb.br:10482/1343 |
| publishDate | 2008 |
| publishDateSort | 2008 |
| reponame_str | Repositório Institucional da UnB |
| repository.mail.fl_str_mv | repositorio@unb.br |
| repository.name.fl_str_mv | Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| repository_id_str | |
| spelling | Galdino, André LuizAyala-Rincón, Mauricio2009-02-26T15:02:00Z2009-02-26T15:02:00Z20082008GALDINO, André Luiz. Uma formalização da teoria de reescrita em linguagem de ordem superior. 2008. 143 f. Tese (Doutorado em Matemática)-Universidade de Brasília, Brasília, 2008.http://repositorio.unb.br/handle/10482/1343Tese(doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2008.Teorias para Sistemas Abstratos de Redução (ARS) e Sistemas de Reescrita de Termos (TRS) no assistente de provas PVS (Prototype Verification System) chamadas ars e trs, respectivamente, foram desenvolvidas. A teoria ars, construída com base na teoria para relações binárias do PVS, contém especificações de noções tais como redução, confluência, formas normais, e conceitos não básicos como por exemplo noeterianidade. Por outro lado, a teoria trs, construída com base na teoria ars e a teoria para seqüências finitas encontrada na biblioteca do PVS, contém uma formalização para lidar com a estrutura dos termos, assim como, formalizações de noções não triviais de TRS. As teorias ars e trs foram desenvolvidas com o objetivo de agregar os conceitos e as definições necessários para lidar com a Teoria de Reescrita, em geral. Em outras palavras, ars e trs contém elementos que formam uma base sólida para formalizar propriedades da Teoria de Reescrita em PVS. Para certificar-se de que o objetivo foi alcançado vários resultados bem conhecidos e não triviais foram formalizados; dentre estes, destacam-se a correção do princípio de indução Noeteriana, o Lema de Newman, os Lemas de Comutação e o Teorema dos Pares Críticos de Knuth-Bendix. Além de constituir uma base para formalização de propriedades da Teoria de Reescrita, em geral, a formalização apresentada se destaca por: 1. utilizar uma linguagem de orderm superior, a qual permite expressar naturalmente propriedades de ordem superior; 2. por seu alto grau de abstração, que permite expressar propriedades numa forma quasi-geométrica, como desejável em Teoria de Reescrita; e, 3. pelo alto grau de controle, permitido pelo PVS, no desenvolvimento das provas. _______________________________________________________________________________________ ABSTRACTTheories for Abstract Reduction Systems (ARS) and Term Rewriting Systems (TRS) in the proof assistant PVS (Prototype Verification System) called ars and trs, respectively, we developed. The ars theory built on the PVS library for binary relations, contains specifications of notions such as reduction, confluence, normal forms, and non basic concepts such as Noetherianity. On the other hand, the trs theory built on the ars theory and the PVS library for finite sequences, contains a formalization to deal with the structure of terms as well as formalizations of non-trivial notions of TRS. Theories ars and trs were developed with the main goal of providing the necessary concepts and definitions to deal with the Theory of Rewriting in general. In other words, ars and trs contain elements that conform a solid basis to formalize properties of the Theory of Rewriting in PVS. To make sure that the goal was achieved well-known and non-trivial results were formalised; among these, the correctness of the principle of noetherian induction, the Newman’s Lemma, the Commutation Lemma and the Knuth-Bendix Critical Pair Theorem. Apart from being a basis for formalization of properties of the Theory of Rewriting, in general, the formalization presented is highlighted by: 1. the use a higherorder language, which allows for the specification of high-order properties naturally, 2. for their high-level of abstraction, which allows for the specification properties in an almost geometric style, as desirable in Rewriting Theory, and 3. the high degree of control allowed by PVS in the development of proofs.Programa de Pós-Graduação em InformáticaUma formalização da teoria de reescrita em linguagem de ordem superiorinfo:eu-repo/semantics/publishedVersioninfo:eu-repo/semantics/doctoralThesisAlgoritmosTeoria de Reescrita de TermosAnálise matemáticaBRAinfo:eu-repo/semantics/openAccessporreponame:Repositório Institucional da UnBinstname:Universidade de Brasília (UnB)instacron:UNBORIGINAL2008_AndreLuizGaldino.pdf2008_AndreLuizGaldino.pdfapplication/pdf873327http://repositorio.unb.br/bitstream/10482/1343/1/2008_AndreLuizGaldino.pdfea02527f0563d16fc5b1df77c3f6f722MD51open accessLICENSElicense.txtlicense.txttext/plain1860http://repositorio.unb.br/bitstream/10482/1343/2/license.txt4b42614877acda4ce615b4cc029292a8MD52open accessTEXT2008_AndreLuizGaldino.pdf.txt2008_AndreLuizGaldino.pdf.txtExtracted texttext/plain226164http://repositorio.unb.br/bitstream/10482/1343/3/2008_AndreLuizGaldino.pdf.txtff06cb235a3616a0c2e8a878e1c6da3dMD53open access10482/13432025-02-28 15:19:13.538open accessoai:repositorio.unb.br:10482/1343TGljZW5zZSBncmFudGVkIGJ5IFJ1dGhsw6lhIE5hc2NpbWVudG8gKHJ1dGhsZWFAYmNlLnVuYi5icikgb24gMjAwOC0xMC0zMFQxNjoxMjo1MFogKEdNVCk6CgrDiSBuZWNlc3PDoXJpbyBjb25jb3JkYXIgY29tIGEgbGljZW7Dp2EgZGUgZGlzdHJpYnVpw6fDo28gbsOjby1leGNsdXNpdmEsCmFudGVzIHF1ZSBvIGRvY3VtZW50byBwb3NzYSBhcGFyZWNlciBubyBSZXBvc2l0w7NyaW8uIFBvciBmYXZvciwgbGVpYSBhCmxpY2Vuw6dhIGF0ZW50YW1lbnRlLiBDYXNvIG5lY2Vzc2l0ZSBkZSBhbGd1bSBlc2NsYXJlY2ltZW50byBlbnRyZSBlbQpjb250YXRvIGF0cmF2w6lzIGRlOiByZXBvc2l0b3Jpb0BiY2UudW5iLmJyIG91IDMzMDctMjQxMS4KCkxJQ0VOw4dBIERFIERJU1RSSUJVScOHw4NPIE7Dg08tRVhDTFVTSVZBCgpBbyBhc3NpbmFyIGUgZW50cmVnYXIgZXN0YSBsaWNlbsOnYSwgby9hIFNyLi9TcmEuIChhdXRvciBvdSBkZXRlbnRvciBkb3MKZGlyZWl0b3MgZGUgYXV0b3IpOgoKYSkgQ29uY2VkZSDDoCBVbml2ZXJzaWRhZGUgZGUgQnJhc8OtbGlhIG8gZGlyZWl0byBuw6NvLWV4Y2x1c2l2byBkZQpyZXByb2R1emlyLCBjb252ZXJ0ZXIgKGNvbW8gZGVmaW5pZG8gZW0gYmFpeG8pLCBjb211bmljYXIgZS9vdQpkaXN0cmlidWlyIG8gZG9jdW1lbnRvIGVudHJlZ3VlIChpbmNsdWluZG8gbyByZXN1bW8vYWJzdHJhY3QpIGVtCmZvcm1hdG8gZGlnaXRhbCBvdSBpbXByZXNzbyBlIGVtIHF1YWxxdWVyIG1laW8uCgpiKSBEZWNsYXJhIHF1ZSBvIGRvY3VtZW50byBlbnRyZWd1ZSDDqSBzZXUgdHJhYmFsaG8gb3JpZ2luYWwsIGUgcXVlCmRldMOpbSBvIGRpcmVpdG8gZGUgY29uY2VkZXIgb3MgZGlyZWl0b3MgY29udGlkb3MgbmVzdGEgbGljZW7Dp2EuIERlY2xhcmEKdGFtYsOpbSBxdWUgYSBlbnRyZWdhIGRvIGRvY3VtZW50byBuw6NvIGluZnJpbmdlLCB0YW50byBxdWFudG8gbGhlIMOpCnBvc3PDrXZlbCBzYWJlciwgb3MgZGlyZWl0b3MgZGUgcXVhbHF1ZXIgb3V0cmEgcGVzc29hIG91IGVudGlkYWRlLgoKYykgU2UgbyBkb2N1bWVudG8gZW50cmVndWUgY29udMOpbSBtYXRlcmlhbCBkbyBxdWFsIG7Do28gZGV0w6ltIG9zCmRpcmVpdG9zIGRlIGF1dG9yLCBkZWNsYXJhIHF1ZSBvYnRldmUgYXV0b3JpemHDp8OjbyBkbyBkZXRlbnRvciBkb3MKZGlyZWl0b3MgZGUgYXV0b3IgcGFyYSBjb25jZWRlciDDoCBVbml2ZXJzaWRhZGUgZGUgQnJhc8OtbGlhIG9zIGRpcmVpdG9zCnJlcXVlcmlkb3MgcG9yIGVzdGEgbGljZW7Dp2EsIGUgcXVlIGVzc2UgbWF0ZXJpYWwgY3Vqb3MgZGlyZWl0b3Mgc8OjbyBkZQp0ZXJjZWlyb3MgZXN0w6EgY2xhcmFtZW50ZSBpZGVudGlmaWNhZG8gZSByZWNvbmhlY2lkbyBubyB0ZXh0byBvdQpjb250ZcO6ZG8gZG8gZG9jdW1lbnRvIGVudHJlZ3VlLgoKU2UgbyBkb2N1bWVudG8gZW50cmVndWUgw6kgYmFzZWFkbyBlbSB0cmFiYWxobyBmaW5hbmNpYWRvIG91IGFwb2lhZG8KcG9yIG91dHJhIGluc3RpdHVpw6fDo28gcXVlIG7Do28gYSBVbml2ZXJzaWRhZGUgZGUgQnJhc8OtbGlhLCBkZWNsYXJhIHF1ZQpjdW1wcml1IHF1YWlzcXVlciBvYnJpZ2HDp8O1ZXMgZXhpZ2lkYXMgcGVsbyByZXNwZWN0aXZvIGNvbnRyYXRvIG91CmFjb3Jkby4KCkEgVW5pdmVyc2lkYWRlIGRlIEJyYXPDrWxpYSBpZGVudGlmaWNhcsOhIGNsYXJhbWVudGUgbyhzKSBzZXUgKHMpIG5vbWUgKHMpCmNvbW8gbyAocykgYXV0b3IgKGVzKSBvdSBkZXRlbnRvciAoZXMpIGRvcyBkaXJlaXRvcyBkbyBkb2N1bWVudG8KZW50cmVndWUsIGUgbsOjbyBmYXLDoSBxdWFscXVlciBhbHRlcmHDp8OjbywgcGFyYSBhbMOpbSBkYXMgcGVybWl0aWRhcyBwb3IKZXN0YSBsaWNlbsOnYS4KRepositório InstitucionalPUBhttps://repositorio.unb.br/oai/requestrepositorio@unb.bropendoar:2025-02-28T18:19:13Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| spellingShingle | Uma formalização da teoria de reescrita em linguagem de ordem superior Galdino, André Luiz Algoritmos Teoria de Reescrita de Termos Análise matemática |
| status_str | publishedVersion |
| title | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| title_full | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| title_fullStr | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| title_full_unstemmed | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| title_short | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| title_sort | Uma formalização da teoria de reescrita em linguagem de ordem superior |
| topic | Algoritmos Teoria de Reescrita de Termos Análise matemática |
| url | http://repositorio.unb.br/handle/10482/1343 |