LMF2013: Aplicaciones de la lógica proposicional con Prover9 y Haskell

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos
hemos estudiado cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 o Haskell para su solución.

Los problemas que se han visto son

  • El problema de los veraces y los mentirosos.
  • El problema de los animales.
  • El problema del coloreado del pentágono.
  • El problema del palomar.
  • El problema de los rectángulos.
  • El problema de las 4 reinas.
  • El problema de Ramsey.

Las transparencias utilizadas son las páginas 13 a 49 del tema 6
Read More “LMF2013: Aplicaciones de la lógica proposicional con Prover9 y Haskell”

Reseña: Type classes and filters for mathematical analysis in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre análisis matemático titulado Type classes and filters for mathematical analysis in Isabelle/HOL.

Sus autores son Johannes Hölzl, Fabian Immler y Brian Huffman.

El trabajo se presentará en julio en la ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, C and ℝⁿ. Isabelle’s new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.