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)”

I1M2013: Verificación de la ordenación por mezcla con QuickCheck

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la verificación de propiedades con QuickCheck y, como aplicación, se ha estudiado la verificación de la ordenación por mezcla siguiendo los ejercicios de la relación 9.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2013: Verificación de la ordenación por mezcla con QuickCheck”