I1M2012: Combinatoria en Haskell (2)

PorJosé A. Alonso

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha completado las soluciones de los ejercicios de la relación 22 que se empezó en la clase de la semana pasada.

El objetivo de esta relación es estudiar la generación y el número de
las principales operaciones de la combinatoria. En concreto, se
estudia

  • Permutaciones.
  • Combinaciones sin repetición..
  • Combinaciones con repetición
  • Variaciones sin repetición.
  • Variaciones con repetición.

Además, se estudia dos temas relacionados:

  • Reconocimiento y generación de subconjuntos y
  • El triángulo de Pascal

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Combinatoria en Haskell (2)”

Reseña: ForMaRE – formal mathematical reasoning in economics

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado a la economía titulado ForMaRE – formal mathematical reasoning in economics.

Sus autores son Manfred Kerber, Christoph Lange y Colin Rowat (de la Universidad de Birmingham) y lo presentarán hoy en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

We present the ForMaRE project which applies FORmal MAthematical REasoning to economics. Theoretical economics makes use of mathematical proof and we seek to increase confidence in these theoretical results by applying formal mathematical reasoning. This will lead on the one hand to new challenge problems in formal reasoning. On the other hand we are conducting research that connects economics and formal methods. We will discuss some areas of interest such as game theory and auctions, where we are currently building a toolbox of formalizations.

LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (1)

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 10, 11, 12, 13 y 16 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.

Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (1)”

Reseña: AI over large formal knowledge bases: The first decade

PorJosé A. Alonso

Se ha publicado un artículo sobre aplicaciones de la inteligencia artificial a la demostración automática de teoremas titulado AI over large formal knowledge bases: The first decade.

Su autor es Josef Urban (de la Univ. de Nimega, Países Bajos) y lo presentará mañana en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

In March 2003, the first version of the Mizar Problems for Theorem Proving (MpTP) was released. In the past ten years, such large formal knowledge bases have started to provide an interesting playground for combining deductive and inductive AI methods. The talk will discuss three related areas of application in which machine learning and general AI have been recently experimented with: (i) premise selection for theorem proving over large formal libraries built with systems like Mizar, HOL Light, and Isabelle (ii) advising and tuning first-order automated theorem provers such as E and leanCoP, and (iii) building larger inductive/deductive AI systems such as MaLARea. Here I focus on the wider motivation for this work.

I1M2012: Ejercicios de cálculo numérico en Haskell

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 22ª relación, en la que se definen funciones para resolver los siguientes problemas de cálculo numérico:

  • diferenciación numérica,
  • cálculo de la raíz cuadrada mediante el método de Herón,
  • cálculo de los ceros de una función por el método de Newton y
  • cálculo de funciones inversas.

Un aspecto a destacar desde el punto de vista de la programación es el uso de la abstracción de procedimientos.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Ejercicios de cálculo numérico en Haskell”