En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios con el TAD de los polinomios presentados en la clase del día 11.
Los ejercicios y sus soluciones son
Read More “1M2104: Ejercicios con el TAD de los polinomios en Haskell”
Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Machine-checked proofs for realizability checking algorithms.
Sus autores son
Su resumen es
We have recently proposed a contract-based realizability checking algorithm involving the use of theories, to provide an auxiliary procedure to consistency checking of “leaf-level” components in complex embedded systems. To prove the soundness of our approach on realizability, we formalized the necessary definitions and theorems of Towards realizability checking of contracts using theories, in the Coq proof and specification language.
El código de las correspondientes teorías en Coq se encuentra [aquí](.https://github.com/andrewkatis/Coq/
blob/master/realizability/Realizability.v).
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado la sintaxis y la semántica de la lógica proposicional.
Se ha presentado la sintaxis de la lógica proposicional. Concretamente,
En la semántica, los conceptos definidos son los valores de verdad, las funciones de verdad, las interpretaciones, el valor de verdad de las fórmulas respectos de las interpretaciones, los modelos de fórmulas, la clasificación semántica de fórmulas (satisfacibles, insatisfacibles, tautologías, contradictorias y contingentes), los problemas SAT y TAUT. Finalmente, se han visto dos algoritmos para la solución de los problemas SAT y TAUT: tablas de verdad y método de Quine.
Otros conceptos definidos son equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y consecuencia lógica.
Se ha demostrado la equivalencia de los siguientes problemas
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabezas se ha explicado el uso del Gateway to Logic.
Las transparencias de estas clases son las del tema 1
Read More “LMF2015: Sintaxis y semántica de la lógica proposicional”
En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de la sintaxis y la semántica de la lógica proposicional
Las soluciones de los ejercicios se muestran a continuación.
Read More “LMF2015: Sintaxis y semántica de la lógica proposicional en Haskell”
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los polinomios y su implementación en Haskell.
Comenzamos la clase analizando las posibles representaciones de los polinomios y, como consecuencia, establecer la signatura y las propiedades del TAD de los polinomios.
A continuación, estudiamos tres prosibles representaciones del TAD de los polinomios mediante tipos algebraicos, mediantes listas dispersas y mediante listas densas y sus implementaciones en Haskell
Finalmente, hemos estudiado las operaciones con los polinomios usando el TAD de los polinomios.
Las transparencias usadas en la clase son las del tema 21
El código del TAD de polinomios mediante tipo algebraico es
Read More “I1M2014: El TAD de los polinomios en Haskell”