Uma formalização da teoria de reescrita em linguagem de ordem superior

AUTOR(ES)

André Luiz Galdino

DATA DE PUBLICAÇÃO

2008

RESUMO

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 Newmans 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.

ASSUNTO(S)

matematica teoria de reescrita formalização pvs: pares críticos

Documentos Relacionados

• Um estudo do sistema Oyster-Clam, implementação de reescrita de tipos e uma formalização parcial da teoria dos grafos
• A instauração da criança na linguagem : princípios para uma teoria enunciativa em aquisição da linguagem
• Contribuições do marxismo para uma teoria crítica da linguagem
• Uma possibilidade para a superação das dificuldades na aprendizagem da linguagem escrita : o texto e sua reescrita
• Uma formalização da mão invisível