Razonamiento Ecuacional sobre Estructuras de Datos.

Ponente(s): Pilar Selene Linares Arevalo

En nuestros cursos de Álgebra, hemos aprendido a demostrar propiedades sobre números a partir de axiomas y, en algunos casos, otras propiedades. Por ejemplo, únicamente a partir de las ecuaciones: \[ \begin{array}{rcl} x + y & = &y + x \\ x + (y + z) & = & (x + y) + z \\ \end{array} \] podemos concluir que x + (y + z) = (z + y) + x , pero no podemos afirmar que x + x = x + y.\\ De forma general podríamos preguntamos: ¿cuándo una igualdad es consecuencia lógica de un conjunto dado de ecuaciones?. La Lógica ecuacional es una restricción de la Lógica de Primer Orden que trabaja con expresiones en forma de igualdades. En esta presentación hablaremos del razonamiento en la lógica ecuacional, su uso en la demostración de propiedades de estructuras de datos - como listas, árboles y pilas -, así como su aplicación al razonamiento en programación funcional. Este trabajo se realiza con el apoyo del proyecto UNAM PAPIME PE102117.