En la clase de hoy del curso de Razonamiento automático hemos comentados las soluciones de los ejercicios de la relación 1 (sobre deducción natural en lógica proposicional) y de la ewlación 2 (sobre deducción natural en lógica de primer orden) y hemos resueltos esjercicios de la relación 3 (sobre razonamiento por inducción sobre listas).
En este artículo continúo la serie dedicada a los tipos de datos abstractos (TAD) en Haskell presentando el TAD de las colas de prioridad.
Una cola de prioridad (en inglés, priority queue) es una cola en la que cada elemento tiene asociada una prioridad y la operación de extracción siempre elige el elemento de menor prioridad. Un ejemplo de cola de prioridad es el formado por una lista de ciudades ordenadas por su distancia a un destino final.
El contenido del resto del artículo es el siguiente:
Posteriormente, cuando se estudien los montículos, se presentará otra implementación de las colas de prioridad mediante montículos.
Read More “El tipo abstracto de datos de las colas de prioridad en Haskell”
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”
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”
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).