En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado los métodos de demostración por casos y por inducción iniciados en Isabelle/HOL.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Razonamiento por casos y por inducción en Isabelle/HOL (1)”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha continuado la presentación (iniciada en la clase anterior) de cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
En la presentación se han usado los ejemplos del tema 8 del curso de Informática (de 1º del Grado en Matemáticas).
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Razonamiento sobre programas con Isabelle/HOL (2)”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los 6 primeros ejercicios de la relación 25. El objetivo de la relación es implementar la regla de Ruffini y sus aplicaciones utilizando las implementaciones del TAD de polinomio estudiadas en el tema 21.
En los ejercicios se usan las siguientes librerías:
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: División y factorización de polinomios mediante la regla de Ruffini en Haskell”
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha continuado la resolución de los ejercicios de la relación 24. El objetivo de esta relación es ampliar el conjunto de operaciones
sobre polinomios definidas utilizando las implementaciones del TAD de
polinomio estudiadas en el tema 21. Además, en algunos ejemplos de usan polinomios con coeficientes racionales. En Haskell, el número racional x/y se representa por x%y. El TAD de los números racionales está definido en el módulo Data.Ratio.
En los ejercicios se usan las siguientes librerías, estudiadas en el tema 21,
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Operaciones con el TAD de los polinomios en Haskell (2)”
Se ha publicado un artículo de razonamiento formalizado en Coq titulado A constructive theory of regular languages in Coq.
Sus autores son Christian Doczkal, Jan-Oliver Kaiser y Gert Smolka (de la Univ. de Sarre (en alemán: Saarland), Alemania).
Su resumen es
We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect’s support for finite types and graphs.
El código de las correspondientes teorías en Coq se encuentra aquí.