RA2012: Verificación de propiedades de la sustitución en Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha resuelto de manera colaborativa ejercicios sobre la demostración de propiedades de la función de sustitución con Isabelle/HOL. Su objetivo es ilustrar el uso del razonamiento por inducción y por casos en Isabelle. Para ca propiedad se presentan distintas demostraciones desde las automáticas a las detalladas.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Verificación de propiedades de la sustitución en Isabelle/HOL”

I1M2012: División y factorización de polinomios mediante la regla de Ruffini en Haskell (2)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 25. El objetivo de la relación es implementar la regla de Ruffini y sus aplicaciones utilizando las implementaciones del TAD de polinomio estudiadas en el tema 21.

En los ejercicios se usan las siguientes librerías:

  • PolRepTDA: Implementación de los polinomios mediante tipos de datos algebraicos.
  • PolRepDispersa: Implementación de los polinomios mediante listas dispersas.
  • PolRepDensa: Implementación de los polinomios mediante listas densas.
  • PolOperaciones: Operaciones con el TAD de los polinomios.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: División y factorización de polinomios mediante la regla de Ruffini en Haskell (2)”

Reseña: Graph theory

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL titulado Graph theory.

Su autor es Lars Noschinski (de la Univrsidad Técnica de Munich).

Su resumen es

This development provides a formalization of directed graphs, supporting (labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multi-edges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.

This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.

Definitions and nomenclature are based on Digraphs: Theory, algorithms and applications (by J. Bang-Jensen and G. Gutin).

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