En la clase de hoy del curso Lógica Informática se ha realizado el primer examen de la evaluación continua. Las soluciones se muestran a continuación
Read More “LI2013: 1º examen de la evaluación continua”
Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL sobre metalógica titulado Gödel’s incompleteness theorems.
Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).
Su resumen es
Gödel’s two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.
El trabajo se ha publicado en The Archive of Formal Proofs
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL sobre la teoría de conjuntos titulado The hereditarily finite sets.
Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).
Su resumen es
The theory of hereditarily finite (HF) sets is formalised, following the development of Swierczkowski. An HF set is a finite collection of other HF sets; they enjoy an induction principle and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated. All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers, functions) without using infinite sets are possible here. The definition of addition for the HF sets follows Kirby.
This development forms the foundation for the Isabelle proof of Gödel’s incompleteness theorems, which has been formalised separately.
El trabajo se ha publicado en The Archive of Formal Proofs.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar automáticamente propiedades de programas funcionales con Isabelle/HOL.
En primer lugar, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 7 del curso de Programación declarativa (de 3º del Grado en Informática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.
A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.
El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,
|
1 |
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
|
1 2 |
lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" |
La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Razonamiento automático sobre programas con Isabelle/HOL”
Uno de los problemas de las Olimpiadas matemáticas de este año es el siguiente
Dada la sucesión, definida por
,
calcular el término 2013 de la misma.
A partir del problema he elaborado, con la colaboración de María J. Hidalgo, la siguiente relación de ejercicios en Haskell para la asignatura de Informática (de 1º del Grado en Matemáticas).
En la relación se presenta 5 definiciones distintas de la sucesión:
Se observa que las dos primeras definiciones son incorrectas (debido a errores de redondeo), la tercera es correcta pero basada en propiedades no evidentes y además es ineficiente, la cuarta es más eficiente y la quinta es correcta, elemental y eficiente.
La relación de ejercicios, y sus soluciones, es la siguiente
Read More “Sucesión con radicales en Haskell”
