Deducción natural en lógica de primer orden con Isabelle/Isar

En esta teoría se presenta la formalización en Isabelle/Isar de los ejemplos del tema de deducción natural en la lógica de primer orde siguiendo la presentación de Huth y Ryan en su libro Logic in Computer Science y, más concretamente, a la forma como se explica en la asignatura de Lógica informática y que puede verse en las transparencias del tema 7.

La páginas en los teorema indican la página de las anteriores transparencias donde se encuentra la demostración.
Read More “Deducción natural en lógica de primer orden con Isabelle/Isar”

Deducción natural en lógica proposicional con Isabelle/Isar

En esta teoría se presentan los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro Logic in Computer Science y, más concretamente, a la forma como se explica en la asignatura de Lógica informática y que puede verse en
las transparencias del tema 2.

La página al lado de cada teorema indica la página de las anteriores transparencias donde se encuentra la demostración.
Read More “Deducción natural en lógica proposicional con Isabelle/Isar”

RA2010: Wiki de ejercicios de razonamiento formalizado en Isabelle/Isar

En la clase de hoy del curso de Razonamiento automáticohemos comentado las novedades de la última versión de Isabelle ( Isabelle2011) que se ha publicado esta semana. Especialmente, el entorno de desarrollo jEdit.

También se ha presentado la wiki de ejercicios del curso y se ha comentado la forma registrase, obtener enunciados y actualizar las soluciones.

Se ha comenzado a escribir las soluciones de la relación 1 (sobre deducción natural en lógica proposicional), de la ewlación 2 (sobre deducción natural en lógica de primer orden) y de la relación 3 (sobre razonamiento por inducción).

El tipo abstracto de datos de las colas en Haskell

En este artículo continúo la serie dedicada a los tipos de datos abstractos (TAD) en Haskell presentando el TAD de las colas.

Al igual que hice en los anteriores TAD, usaré módulos, funciones de escritura y QuickCheck para conseguir la abstracción, independencia y certificación de los resultados de las implementaciones.

Una cola es una estructura de datos, caracterizada por ser una secuencia de elementos en la que la operación de inserción se realiza por un extremo (el posterior o final) y la operación de extracción por el otro (el anterior o frente). Las colas también se llaman estructuras FIFO (del inglés First In First Out), debido a que el primer elemento en entrar será también el primero en salir. Este comportamiento es análogo a las colas del cine.

El contenido del resto del artículo es el siguiente:

  • la signatura del TAD de las colas;
  • las propiedades del TAD de las colas;
  • la implementación, en Haskell, de las colas mediante listas;
  • la implementación, en Haskell, de las colas mediante pares de listas y
  • la comprobación con QuickCheck de sus propiedades.

Read More “El tipo abstracto de datos de las colas en Haskell”