Tese(doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2008. / Submitted by Ruthléa Nascimento (ruthlea@bce.unb.br) on 2008-10-30T16:12:50Z
No. of bitstreams: 1
2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / Approved for entry into archive by Luanna Maia(luanna@bce.unb.br) on 2009-02-26T15:02:00Z (GMT) No. of bitstreams: 1
2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / Made available in DSpace on 2009-02-26T15:02:00Z (GMT). No. of bitstreams: 1
2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / 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.
_______________________________________________________________________________________ ABSTRACT / Theories 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/1343 |
| Date | January 2008 |
| Creators | Galdino, André Luiz |
| Contributors | Ayala-Rincón, Mauricio |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0022 seconds