I1M2013: Ejercicios de definiciones por recursión y comprensión (1)

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se han comentado las soluciones de los ejercicios 4 a 8 de la 8ª relación y los 5 primeros de la 10ª. En la relación 8 se proponen ejercicios por recursión de exámenes del curso anterior. En la relación 10 se proponen ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios 4 a 8 de la relación 8 y soluciones se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por recursión y comprensión (1)”

LI2013: Deducción natural en lógica de primer orden (2)

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se ha continuado el estudio de la deducción natural en lógica de primer orden. Se han comentado distintas equivalencias lógicas y se han demostrado por deducción natural y mediante tableros semánticos las siguientes equivalencias:

  • ¬∀xP(x) ≡ ∃x¬P(x)
  • ∀x(P(x) ∧ Q(x)) ≡ ∀xP(x) ∧ ∀xQ(x)

Las transparencias de esta clase son las páginas 14 a 20 del tema 8 que se muestran a continuación
Read More “LI2013: Deducción natural en lógica de primer orden (2)”

Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre
teoría de grafos titulado Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chro- matic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.

El trabajo se presentó en el ITP 2012 (Interactive Theorem Proving).

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

RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL (2)

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático hemos continuado la presentación de cómo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle/HOL.

Para ello, se visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 2a (que se corresponden con el capítulo 13 del libro de G. Hutton Programming in Haskell).

Las demostraciones estudiadas son las correspondientes a las páginas 38 a 50 del tema 2a. Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL (2)”