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

En la clase de hoy del curso 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 “LMF2014: Sintaxis y semántica de la lógica proposicional”

Proof-by-instance for embedded network design

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Proof-by-instance for embedded network design.

Sus autores son

  • Marc Boyer (de ONERA – The French Aerospace Lab, Toulouse, France),
  • Loïc Fejoz (de RealTime-at-Work, Nancy, France) y
  • Stephan Merz (Inria & LORIA, Nancy, France).

Su resumen es

Proof-by-instance is a technique that ensures the correctness of the results of a computation rather than proving correct the tool carrying out the computation. We report here on the application of this idea to check the computations relevant for analyzing time bounds for AFDX networks. We have demonstrated the feasibility of the approach by applying a proof-of-concept implementation to an AFDX network of realistic size, and we outline the roadmap towards a mature industrial toolset. This approach should lead to a reduction of the time and cost of developing analysis tools used in the design of embedded networks where certification is mandatory.

El trabajo se presentó el 6 de febrero en el ERTS² 2014 Embedded Real Time Software And Systems.

I1M2013: Los problemas de las N reinas y de Hamming en Haskell

En la tercera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos vistos dos aplicaciones de la programación funcional en Haskell: el problema de las reinas (consistente en colocar N reinas en un tablero de dimensiones N por N de forma que no se encuentren más de una en la misma línea: horizontal, vertical o diagonal) y el problema de Hamming (consistente definir una sucesión estrictamente creciente de números tales que el número 1 está en la sucesión y que, si x está en la sucesión, entonces 2*x, 3*x y 5*x también están).

El código del problema de las N reinas es
Read More “I1M2013: Los problemas de las N reinas y de Hamming en Haskell”

I1M2013: Problema del concurso “Cifras y letras” en Haskell

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos desarrollado un programa en Haskell para resolver los problemas aritméticos del concurso Cifras y letras que consisten en dada una sucesión de números naturales y un número objetivo, intentar construir una expresión cuyo valor es el objetivo combinando los números de la sucesión usando suma, resta, multiplicación, división y paréntesis. Además, cada número de la sucesión puede usarse como máximo una vez y todos los números, incluyendo los resultados intermedios tienen que ser enteros positivos (1,2,3,…).

Por ejemplo, dada la sucesión 1, 3, 7, 10, 25, 50 y el objetivo 765, una solución es (1+50)*(25−10). Para el problema anterior existen 780 soluciones. En cambio, con la sucesión anterior y el objetivo 831, no hay solución.

Se empieza formalizando el problema y definiendo una función para reconcer las soluciones. A continuación, se presentan tres soluciones: la primera por fuerza bruta, la segunda mediante generación y evaluación y la tercera con simplificaciones algebraicas. Se termina con una comparación de las tres soluciones.

El código del programa es
Read More “I1M2013: Problema del concurso “Cifras y letras” en Haskell”