LMF2015: Deducción natural proposicional en Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la formalización en Isabelle/HOL de las demostraciones por deducción natural estudiadas en el tema 2.

Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2015: Deducción natural proposicional en Isabelle/HOL”

I1M2014: Resolución de una ecuación con factoriales en Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 21, cuyo objetivo es resolver la ecuación a! * b! = a! + b! + c!, donde a, b y c son números naturales.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2014: Resolución de una ecuación con factoriales en Haskell”

Reseña: A formalisation of finite automata using hereditarily finite sets

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado A formalisation of finite automata using hereditarily finite sets

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

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