Menu Close

Mes: mayo 2020

I1M2019: El tipo abstracto de datos de grafos en Haskell

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de datos de los grafos y dos de sus implementaciones en Haskell: mediante vectores y matrices de adyacencia.

La clase se ha dado mediante videoconferencia los correspondientes vídeos son

  • El TAD de grafos mediante vectores

  • El TAD de grafos mediante matricess

Los apuntes correspondientes a la clase es la sección 1 del tema 22

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

I1M2019: El patrón de búsqueda en escalada en Haskell

En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda en escalada en espacios de estados.

En primer lugar se explicó la idea de la búsqueda en escalada y cómo, usando dicha idea, se puede transformar el patrón de búsqueda por primero el mejor en el de búsqueda en escalada. Finalmente, se aplicó el patrón de búsqueda en escalada a la resolución del problema del cambio de monedas.

La clase se ha dado mediante videoconferencia y el correspondiente vídeo es

Los apuntes correspondientes a la clase es la sección 3 del tema 23

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

El código del problema del cambio de monedas usado en la clase es

LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo desarrollar en Isabelle/HOL teorías axiomáticas usando entornos locales (“locales”) y clases de tipos (“class”). Se ha aplicado al desarrollo de las teorías de grupos y a las de órdenes. videoconferencia.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte:

  • Segunda parte:

La teoría con los ejemplos presentados en la clase es la siguiente:

I1M2019: El patrón de búsqueda por primero el mejor en Haskell

En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda informada en espacios de estados.

En primer lugar se estudiaron los algoritmos búsqueda con información (coste, heurística y A*). A continuación se estudió cómo adaptar el patrón de búsqueda ciega a búsqueda informada usando las colas de prioridad. Finalmente, se aplicó el patrón de búsqueda por primero el mejor a la resolución del problema del 8 puzzle.

La clase se ha dado mediante videoconferencia los correspondientes vídeos son

  • Algoritmos de búsqueda informada en espacios de estados

  • El patrón de búsqueda por primero el mejor en Haskell

Los apuntes correspondientes a la clase es la sección 3 del tema 23

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

El código de la primera solución del problema del 8 puzzle usado en la clase es

Vídeos de las clases de razonamiento automático con Isabelle/HOL

Vídeos de las clases de algorítmica con Haskell

Con motivo de la pandemia hemos tenido que pasar la docencia al formato no presencial.

En la asignatura de Informática de 1º de Matemáticas el cambio ha tenido lugar al principio de la segunda parte del curso en el que aplica la programación funcional con Haskell, estudiada en la primera parte, a problemas de algorítmica.

Todas las clases no presenciales las he dado por videoconferencia y he subido sus vídeos a YouTube. En este momento hay 16 vídeos correspondientes a las 9 clases no presenciales impartidas:

I1M2019: El patrón de búsqueda en espacios de estados en Haskell

En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado cómo programar en Haskell los algoritmos de búsqueda en espacios de estados que vimos en la clase anterior y su aplicación al problema de las N reinas.

La clase se ha dado mediante videoconferencia y el correspondiente vídeo es

Los apuntes correspondientes a la clase son la segunda sección de

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte: Razonamiento sobre árboles binarios

  • Segunda parte: Árboles y bosques: Recursión mutua e inducción

La teoría utilizada es la siguiente

chapter ‹Tema 8: Razonamiento sobre árboles›
 
theory T8_Razonamiento_sobre_arboles
imports Main 
begin
 
text ‹En este tema se estudia razonamiento sobre otras estructuras
  recursivas como árboles binarios, árboles generales y bosques.
 
  También se muestra cómo definir tipos de datos por recursión cruzada y
  la demostración de sus propiedades por inducción.›
 
section ‹Razonamiento sobre árboles binarios›
 
text ‹Ejemplo de definición de tipos recursivos:
  Definir un tipo de dato para los árboles binarios.›
 
datatype 'a arbolB = Hoja "'a" 
                   | Nodo "'a" "'a arbolB" "'a arbolB"
 
text ‹Regla de inducción correspondiente a los árboles binarios:
  La regla de inducción sobre árboles binarios es arbolB.induct:
  ⟦ ⋀x. P (Hoja x);
    ⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧ 
  ⟹ P a
›
 
thm arbolB.induct
 
text ‹Ejemplo de definición sobre árboles binarios:
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.›
 
fun espejo :: "'a arbolB ⇒ 'a arbolB" where
  "espejo (Hoja x)     = Hoja x"
| "espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)"
 
value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"
 
text ‹Ejemplo de demostración sobre árboles binarios:
  Demostrar que la función "espejo" es involutiva; es decir, para
  cualquier árbol a, se tiene que 
     espejo (espejo a) = a.›
 
― ‹La demostración declarativa es›
lemma 
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)"  
    by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo (espejo (Nodo x i d)) = 
          espejo (Nodo x (espejo d) (espejo i))" 
      by simp
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by simp
    also have "… = Nodo x i d" 
      using h1 h2 by simp 
    finally show "?P (Nodo x i d)" 
      by this
  qed
qed
 
― ‹La demostración declarativa detallada es›
lemma 
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)"  
    by (simp only: espejo.simps(1)) 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo (espejo (Nodo x i d)) = 
          espejo (Nodo x (espejo d) (espejo i))" 
      by (simp only: espejo.simps(2))
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by (simp only: espejo.simps(2))
    also have "… = Nodo x i d" 
      using h1 h2
      by (simp only:) 
    finally show ?thesis 
      by this
  qed
qed
 
text ‹Comentarios sobre la demostración anterior:
  · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
    cuyos elementos son de tipo b". 
  · (induct a) indica que el método de demostración es por inducción
    en el árbol binario a.
  · Se generan dos casos:
    1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
    2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; 
                   espejo (espejo a3) = a3⟧
                  ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3›
 
― ‹La demostración aplicativa es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply (simp only: espejo.simps(1))
  apply (simp only: espejo.simps(2))
  done
 
― ‹La demostración automática es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) simp+ 
 
― ‹La demostración automática detallada es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) (simp only: espejo.simps)+  
 
text ‹Ejemplo. [Aplanamiento de árboles]
  Definir la función "aplana" que aplane los árboles recorriéndolos en
  orden infijo.›
 
fun aplana :: "'a arbolB ⇒ 'a list" where
  "aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = aplana i @ [x] @ aplana d"
 
value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      [c, b, d, a, e]"
 
text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo a) = rev (aplana a)›
 
― ‹La demostración declarativa es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (Hoja x)" 
    by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" 
      by simp
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by simp
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      using h1 h2 by simp
    also have "… = rev ((aplana i) @ [x] @ (aplana d))" 
      by simp
    also have "… = rev (aplana (Nodo x i d))" 
      by simp
    finally show "?P (Nodo x i d)" 
      by this
  qed
qed
 
― ‹Lema auxiliar para la demostración declarativa detallada›
lemma rev_unit: "rev [x] = [x]"
proof -
  have "rev [x] = rev [] @ [x]" 
    by (simp only: rev.simps(2))
  also have "… = [] @ [x]"
    by (simp only: rev.simps(1))
  also have "… = [x]"
    by (simp only: append.simps(1))
  finally show ?thesis
    by this
qed
 
― ‹La demostración estructurada y detallada es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x :: 'b
  have "aplana (espejo (Hoja x)) = aplana (Hoja x)"
    by (simp only: espejo.simps(1))
  also have "… = [x]"
    by (simp only: aplana.simps(1))
  also have "… = rev [x]"
    by (simp only: rev_unit)
  also have "… = rev (aplana (Hoja x))"
    by (simp only: aplana.simps(1))
  finally show "?P (Hoja x)" 
    by this 
next
  fix x :: 'b
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" 
      by (simp only: espejo.simps(2))
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by (simp only: aplana.simps(2))
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      by (simp only: h1 h2)
    also have "… = rev ((aplana i) @ [x] @ (aplana d))"
      (* find_theorems "rev (_ @ _)" *)
      by (simp only: rev_append rev_unit append_assoc)
    also have "… = rev (aplana (Nodo x i d))" 
      by (simp only: aplana.simps(2))
    finally show ?thesis 
      by this
  qed
qed
 
― ‹La demostración aplicativa es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: espejo.simps(1) aplana.simps(1))
   apply (simp only: rev_unit)
  apply (simp only: espejo.simps(2) aplana.simps(2))
  apply (simp only: rev_append)
  apply (simp only: rev_unit)
  apply (simp only: append_assoc)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps(1) 
      aplana.simps(1)
      rev_unit
      espejo.simps(2) 
      aplana.simps(2)
      rev_append
      append_assoc)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
  done
 
― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a) simp_all
 
― ‹La demostración automática detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a)
     (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
 
section ‹Árboles y bosques. Recursión mutua e inducción›
 
text ‹Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
  · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
    bosque de tipo a.
  · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
    un árbol de tipo a a un bosque de tipo a.›
 
datatype 'a arbol = Nodo "'a" "'a bosque"
     and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"
 
text ‹Regla de inducción correspondiente a la recursión cruzada:
  La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
     ⟦⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b›
 
thm arbol_bosque.induct
 
text ‹Ejemplos de definición por recursión cruzada:
  · aplana_arbol a) es la lista obtenida aplanando el árbol a.   
  · (aplana_bosque b) es la lista obtenida aplanando el bosque b.   
  · (map_arbol f a) es el árbol obtenido aplicando la función f a
    todos los nodos del árbol a.   
  · (map_bosque f b) es el bosque obtenido aplicando la función f a
    todos los nodos del bosque b. ›
 
fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "aplana_arbol (Nodo x b)   = x # (aplana_bosque b)"
| "aplana_bosque Vacio       = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"
 
fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
    map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
  "map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"
 
text ‹Ejemplo de demostración por inducción cruzada:
  Demostrar que:
  · aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
  · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)›
 
declare [[names_short]] 
 
― ‹La demostración declarativa es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" 
    by simp
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" 
    by simp
  also have "… = (f x) # (map f (aplana_bosque b))" 
    using HI by simp
  also have "… = map f (aplana_arbol (Nodo x b))" 
    by simp
  finally show "aplana_arbol (map_arbol f (Nodo x b)) =
                map f (aplana_arbol (Nodo x b))" 
    by this
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by simp
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by simp
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    using HI1 HI2 by simp
  also have "… = map f (aplana_bosque (ConsB a b))" by simp
  finally show "aplana_bosque (map_bosque f (ConsB a b)) =
                map f (aplana_bosque (ConsB a b))" 
    by this
qed
 
― ‹La demostración declarativa detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" 
    by (simp only: map_arbol.simps(1))
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" 
    by (simp only: aplana_arbol.simps(1))
  also have "… = (f x) # (map f (aplana_bosque b))"
    using HI
    by (simp only:)
  also have "… = map f (aplana_arbol (Nodo x b))" 
    (* find_theorems "map _ (_ # _)" *)
    by (simp only: list.map aplana_arbol.simps(1))
  finally show "aplana_arbol (map_arbol f (Nodo x b)) =
                map f (aplana_arbol (Nodo x b))" 
    by this
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by (simp only: aplana_bosque.simps(1)
                   map_bosque.simps(1)
                   list.map)
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" 
    by (simp only: map_bosque.simps(2))
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by (simp only: aplana_bosque.simps(2))
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    by (simp only: HI1 HI2)
  also have "… = map f (aplana_arbol a @ aplana_bosque b)"
    (* find_theorems "map _ (_ @ _)" *)
    by (simp only: map_append)
  also have "… = map f (aplana_bosque (ConsB a b))" 
    by (simp only: aplana_bosque.simps(2))
  finally show "aplana_bosque (map_bosque f (ConsB a b)) =
                map f (aplana_bosque (ConsB a b))" 
    by this
qed
 
text ‹Comentarios sobre la demostración anterior:
  · (induct_tac a and b) indica que el método de demostración es por
    inducción cruzada sobre a y b.
  · Se generan 3 casos:
    1. ⋀a bosque.
          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
          map h (aplana_arbol (arbol.Nodo a bosque))
    2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    3. ⋀arbol bosque.
          ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
          ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
             map h (aplana_bosque (ConsB arbol bosque))›
 
― ‹La demostración aplicativa es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply simp+
  done
 
― ‹La demostración aplicativa detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: map_arbol.simps aplana_arbol.simps)
    apply (simp only: list.map(2))
   apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))
   apply (simp only: list.map(1))
  apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))
  apply (simp only: map_append)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      aplana_arbol.simps
      list.map(2)
      map_bosque.simps(1) 
      aplana_bosque.simps(1)
      list.map(1)
      map_bosque.simps(2) 
      aplana_bosque.simps(2)
      map_append)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
  done
 
― ‹La demostración automática es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  by (induct_tac a and b) simp+
 
― ‹La demostración automática detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  by (induct_tac a and b) 
     (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
 
end

I1M2019: Resolución de problemas mediante búsqueda en espacios de estados

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda en espacios de estados.

En primer lugar se ha visto cómo se describen los problemas mediante el estado inicial, los sucesores de los estados y los estados finales. Aplicándola a los problemas del 8-puzzle, del granjero, de las jarras y del viaje.

A continuación se han explicado los procedimientos básicos de búsquedas: en anchura, en profundidad, en profundidad acotada y en profundidad iterativa.

La clase se ha dado mediante videoconferencia y los correspondientes vídeos son

  • Representación de problemas mediante espacios de estados:

  • Algoritmos de búsqueda en espacios de estados:

Los apuntes correspondientes son las 53 primeras transparencias del tema 23a.