Reseña – A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem
El día 21 se publicó en el Journal of Automated Reasoning el artículo A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem/a> escrito por André L. Galdino y Mauricio Ayala Rincón. En el trabajo se presenta una formalización en PVS del teorema de pares críticos. También es pública la teoría PVS con la formalización.
Este trabajo es la continuación de anteriores trabajos de los autores
- A Theory for Abstract Reduction Systems in PVS
- Verification of Newman’s and Yokouchi Lemmas in PVS
- A PVS theory for Term Rewriting Systems
Todos estos trabajos son extensiones de la tesis de André L. Galdino Uma formalização da teoria de reescrita em linguagem de ordem superior dirigida por Mauricio Ayala Rincón. En la tesis se realiza una formalización en PVS de los sistemas de reescritura semejante a la realizada en ACL2 por José Luis Ruiz Reina en su tesis Una teoría computacional acerca de la lógica ecuacional (formalización ACL2 de la lógica ecuacional y demostración automática de sus propiedades).