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

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

A continuación se ha estudiado la semántica de la lógica proposicional definiendo los booleanos, las interpretaciones, las funciones de verdad de las conectivas y mostrando cómo a partir de dichos conceptos se puede calcular el valor de verdad de una fórmula respecto de una interpretación.

A partir de lo anterior se han estudiado 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. También se ha estudiado la equivalencia de fórmulas.

Seguidamente, se ha extendido las definiciones semáticas de fórmulas a conjuntos de fórmulas estudiando los conceptos de 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.

Las transparencias de esta clase son las del tema 1.

Descargar (PDF, 230KB)

Se han propuesto como ejercios los de la 1ª relación.

I1M2019: Matrices en Haskell

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array.

Se han estudiado las funciones sobre índices (range, index, inRange, rangeSize) y sobre tablas (array, (!), bounds, indices, elems, assocs, (//), listArray y accumArray). También se han estudiado ejemplos de definiciones con dichas funciones.

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

LMF2019: Presentación del curso de “Lógica matemática y fundamentos”

En la clase de hoy, se ha presentado el curso Lógica matemática y fundamentos siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:

También se ha comentado el sistema de demostración que se usará a lo largo del curso: Isabelle/HOL y su bibliografía fundamental.

Finalmente, se han comentado las listas de teoremas enormes y de teoremas incompletos.

Resumen de lecturas compartidas del 1 al 8 de febrero de 2020

Esta entrada es una recopilación de lecturas compartidas, del 1 al 8 de febrero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

Read More “Resumen de lecturas compartidas del 1 al 8 de febrero de 2020”

Reseña: A comprehensive framework for saturation theorem proving

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre lógica titulado A comprehensive framework for saturation theorem proving.

Sus autores son

Su resumen es

One of the indispensable operations of realistic saturation theorem provers is (backward and forward) deletion of subsumed formu- las. In presentations of proof calculi, however, this is usually discussed only informally, and in the rare cases where there is a formal exposition, it is typically clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but using a standard notion of redundancy, a clause C does not make an instance Cσ redundant.

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle/HOL.

El trabajo es parte del proyecto Matryoshka (Fast interactive verification through strong higher-order automation)

El código está incluido en el repositorio IsaFoL (Isabelle Formalization of Logic).