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

PorJosé A. Alonso

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

PorJosé A. Alonso

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

ProofWiki y la verificación de las demostraciones matemáticas

PorJosé A. Alonso

ProofWiki es un compendio de demostraciones matemáticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matemáticos.

El proyecto empezó en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categorías. Una de las categorías particularmente interesante es la de teoremas con nombres en la que aparecen 247 teoremas. También es interesante la página de los teoremas más populares según el número de visitas.

ProofWiki podría servir de base para otro proyecto cuyo objetivo final fuese la verificación formal de las demostraciones matemáticas. Para ello se podría crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como Isabelle/HOL/Isar, PVS, ACL2, Coq, HOL, HOL Light o Mizar).

RA2010: Razonamiento por inducción sobre los naturales

PorJosé A. Alonso

La clase de hoy del curso de Razonamiento automático ha tenido dos partes. En la primera parte se ha comentado la historia del razonamiento automático y algunos de sus logros. En la segunda parte se ha continuado la introducción de técnicas de demostración en Isabelle estudiando la demostración por inducción sobre los números naturales.

Las transparencias y apuntes usados en clase son los siguientes:

La tarea pendiente para la próxima clase consiste en escribir, y publicar en el portafolio digital, las soluciones de los ejercicios de la relación 1 y de la relación 2. Los códigos se encuentran el la página de ejercicios.

RA2010: Razonamiento con cuantificadores, ecuacional y por casos en Isabelle

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede escribir en Isabelle/Isar demostraciones de la lógica de primer orden, el razonamiento ecuacional y las demostraciones por casos.

En la clase se ha presentado el tema 2 (desde la página 21 a la 26) y el tema 3 (desde la página 26 a la 28)

El código correspondiente se encuentra en Cap_2.thy y Cap_3.thy–