LMF2015: Sintaxis y semántica de la lógica proposicional

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,

  • el lenguaje de la lógica proposicional,
  • la definición recursiva de las fórmulas proposicionales,
  • árboles de análisis de fórmulas,
  • definiciones por recursión sobre fórmulas y
  • demostraciones por inducción sobre fórmulas.

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

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

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”

LMF2015: Sintaxis y semántica de la lógica proposicional en Haskell

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”

I1M2014: El TAD de los polinomios 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”

Reseña: Verifying fast and sparse SSA-based optimizations in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre
compiladores titulado Verifying fast and sparse SSA-based optimizations in Coq .

Sus autores son Delphine Demange, David Pichardie y Léo Stefanesco (del grupo Celtique en el INRIA Rennes, Francia).

Su resumen es

The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro- duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail- ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.

El trabajo se presentará en CC 2015 (24th International Conference on Compiler Construction).

El código de las correspondientes teorías en Coq se encuentra aquí.