En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se han comentado las soluciones de los 15 primeros ejercicios de la 3ª relación sobre definiciones con condicionales, guardas y patrones.
Los ejercicios y sus soluciones se muestran a continuación
Read More “I1M2012: Ejercicios de definiciones con condicionales, guardas y patrones”
En la clase de hoy del curso Lógica Informática se han resuelto los ejercios propuestos de la sintaxis y semántica proposicional.
Concretamente, desde el ejercicio 22 al 32 del capítulo 1 del libro de ejercicios. Quedan pendientes para la próxima clase desde el 33 al 37.
Se ha publicado un trabajo de formalización de sistemas de reescritura en Isabelle/HOL titulado Confluence by decreasing diagrams – formalized.
Su autor es Harald Zankl (de la Universidad de Insbruck, Austria).
Su resumen es
Decreasing diagrams are a complete characterization of confluence for abstract rewrite systems whose convertibility classes are countable. In this paper we present a formalization of decreasing diagrams in the theorem prover Isabelle. The main contribution is a formal proof that any locally decreasing abstract rewrite system is confluent.
Las teorías Isabelle/HOL correspondiente al trabajo se encuentran aquí.