En la clase de hoy del curso de Razonamiento automático se han presentado las técnicas de demostración en Isabelle por inducción sobre tipos recursivos. En concreto se han estudiado los esquemas de inducción para las listas y para los árboles binarios.
Las transparencias usadas en clase son las páginas 31-34 del tema 3 (Distinción decasos e inducción). El código correspondiente se encuentra en Cap_3.thy.
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la resolución de ejercicios de la 12ª relación y de ka 13ª relación.
Los ejercicios de la relación 12 y su solución se muestran a continuación
Read More “I1M2010: Ejercicios de Haskell (relaciones 12 y 13)”
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).
La primera vez que uno se encuentra con los siguientes cálculos aritméticos en Haskell puede sorprenderse.
|
1 2 3 4 5 6 7 8 9 10 |
~> ghci GHCi, version 6.12.1: http://www.haskell.org/ghc/ ghci> 1.1 == 1.1 True ghci> 1.1+1.1 == 2.2 True ghci> 1.1+1.1+1.1 == 3.3 False ghci> 2.2+1.1 == 3.3 False |
El mismo comportamiento se da en Common Lisp
|
1 2 3 4 5 6 7 8 9 10 11 |
~> clisp Welcome to GNU CLISP 2.44.1 (2008-02-23) <http://clisp.cons.org/> [1]> (= 1.1 1.1) T [2]> (= (+ 1.1 1.1) 2.2) T [3]> (= (+ 1.1 1.1 1.1) 3.3) NIL [4]> (= (+ 1.1 2.2) 3.3) NIL |
Para comprender estos cálculos es aconsejable leer What Every Computer Scientist Should Know About Floating-Point Arithmetic.
Cada comienzo de año se suelen buscar propiedades numéricas del número del año. En el 2011 se han buscado propiedades que relacionan el 2011 y los números primos.
En este ejercicio (para la asignatura Informática (de 1º del Grado en Matemáticas)) vamos a realizar la búsqueda de dichas propiedades con Haskell.
Read More “El 2011 y los números primos (en Haskell)”