RA2017 | Vestigium

RA2017: Demostración en Isabelle de la corrección de un compilador

José A. Alonso-8 febrero 2018

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.

La clase se ha basado en la siguiente teoría Isabelle

chapter {* Tema 9: Caso de estudio: Compilación de expresiones *}
 
theory T9
imports Main
begin
 
text {*
  El objetivo de este tema es contruir un compilador de expresiones
  genéricas (construidas con variables, constantes y operaciones
  binarias) a una máquina de pila y demostrar su corrección.
*}
 
section {* Las expresiones y el intérprete *}
 
text {*
  Definición. Las expresiones son las constantes, las variables
  (representadas por números naturales) y las aplicaciones de operadores
  binarios a dos expresiones. 
*}
 
type_synonym 'v binop = "'v ⇒ 'v ⇒ 'v"
 
datatype 'v expr = 
  Const 'v 
| Var nat 
| App "'v binop" "'v expr" "'v expr" 
 
text {*
  Definición. [Intérprete] 
  La función "valor" toma como argumentos una expresión y un entorno
  (i.e. una aplicación de las variables en elementos del lenguaje) y
  devuelve el valor de la expresión en el entorno.
*}
 
fun valor :: "'v expr ⇒ (nat ⇒ 'v) ⇒ 'v" where
  "valor (Const b) ent = b"
| "valor (Var x) ent = ent x"
| "valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))"
 
text {*
  Ejemplo. A continuación mostramos algunos ejemplos de evaluación con
  el intérprete. 
*}
 
lemma 
  "valor (Const 3) id = 3 ∧
   valor (Var 2) id = 2 ∧
   valor (Var 2) (λx. x+1) = 3 ∧ 
   valor (App (op +) (Const 3) (Var 2)) (λx. x+1) = 6 ∧
   valor (App (op +) (Const 3) (Var 2)) (λx. x+4) = 9" 
by simp
 
section {* La máquina de pila *}
 
text {*
  Nota. La máquina de pila tiene tres clases de intrucciones:
  · cargar en la pila una constante,
  · cargar en la pila el contenido de una dirección y
  · aplicar un operador binario a los dos elementos superiores de la pila.
*}
 
datatype 'v instr = 
  IConst 'v 
| ILoad nat 
| IApp "'v binop"
 
text {*
  Definición. [Ejecución]
  La ejecución de la máquina de pila se modeliza mediante la función 
  "ejec" que toma una lista de intrucciones, una memoria (representada 
  como una función de las direcciones a los valores, análogamente a los 
  entornos) y una pila (representada como una lista) y devuelve la pila
  al final de la ejecución.
*}
 
fun ejec :: "'v instr list ⇒ (nat⇒'v) ⇒ 'v list ⇒ 'v list" where
  "ejec [] ent vs = vs"
| "ejec (i#is) ent vs = 
     (case i of
        IConst v ⇒ ejec is ent (v#vs)
      | ILoad x ⇒ ejec is ent ((ent x)#vs)
      | IApp f ⇒ ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))"
 
text {* 
  A continuación se muestran ejemplos de ejecución.
*}
 
lemma
  "ejec [IConst 3] id [7] = [3,7] ∧
   ejec [ILoad 2, IConst 3] id [7] = [3,2,7] ∧
   ejec [ILoad 2, IConst 3] (λx. x+4) [7] = [3,6,7] ∧
   ejec [ILoad 2, IConst 3, IApp (op +)] (λx. x+4) [7] = [9,7]"
by simp
 
section {* El compilador *}
 
text {*
  Definición. El compilador "comp" traduce una expresión en una lista de
  instrucciones. 
*}
 
fun comp :: "'v expr ⇒ 'v instr list" where
  "comp (Const v) = [IConst v]"
| "comp (Var x) = [ILoad x]"
| "comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]"
 
text {*
  A continuación se muestran ejemplos de compilación.
*}
 
lemma
  "comp (Const 3) = [IConst 3] ∧
   comp (Var 2) = [ILoad 2] ∧
   comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]"
by simp
 
section {* Corrección del compilador *}
 
text {*
  Para demostrar que el compilador es correcto, probamos que el
  resultado de compilar una expresión y a continuación ejecutarla es lo
  mismo que interpretarla; es decir, 
*}
 
theorem "ejec (comp e) ent [] = [valor e ent]" 
oops
 
text {*
  El teorema anterior no puede demostrarse por inducción en e. Para
  demostrarlo, lo generalizamos a
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
oops
 
text {*
  En la demostración del teorema anterior usaremos el siguiente lema.
*}
 
lemma ejec_append:
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume "?P xs"
  thus "?P (a#xs)" by (cases "a", auto)
qed
 
-- "La demostración detallada es" 
lemma ejec_append_1:
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  thus "?P (a#xs)"
  proof (cases "a")
    case IConst thus ?thesis using HI by simp
  next
    case ILoad thus ?thesis using HI by simp
  next
    case IApp thus ?thesis using HI by simp
  qed
qed
 
text {*
  Una demostración más detallada del lema es la siguiente:
*}
 
lemma ejec_append_2:
  "∀vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  thus "?P (a#xs)"
  proof (cases "a")
    fix v assume C1: "a=IConst v"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs"
        using C1 by simp
      also have "… = ejec (xs@ys) ent (v#vs)" by simp
      also have "… = ejec ys ent (ejec xs ent (v#vs))" using HI by simp
      also have "… = ejec ys ent (ejec ((IConst v)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C1 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix n assume C2: "a=ILoad n"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs"
        using C2 by simp
      also have "… = ejec (xs@ys) ent ((ent n)#vs)" by simp
      also have "… = ejec ys ent (ejec xs ent ((ent n)#vs))" using HI by simp
      also have "… = ejec ys ent (ejec ((ILoad n)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C2 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix f assume C3: "a=IApp f"
    show "∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs"
        using C3 by simp
      also have "… = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))" 
        by simp
      also have "… = ejec ys 
                          ent 
                          (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" 
        using HI by simp
      also have "… = ejec ys ent (ejec ((IApp f)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C3 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  qed
qed
 
text {*
  La demostración automática del teorema es
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
by (induct e) (auto simp add:ejec_append)
 
text {*
  La demostración estructurada del teorema es
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
proof (induct e)
  fix v
  show "∀vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs" by simp
next
  fix x
  show "∀vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs" by simp
next
  fix f e1 e2
  assume HI1: "∀vs. ejec (comp e1) ent vs = (valor e1 ent) # vs"
    and HI2: "∀vs. ejec (comp e2) ent vs = (valor e2 ent) # vs"
  show "∀vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs"
  proof
    fix vs
    have "ejec (comp (App f e1 e2)) ent vs
          = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs" by simp
    also have "… = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)"
      using ejec_append by blast
    also have "… = ejec [IApp f] 
                         ent 
                         (ejec (comp e1) ent (ejec (comp e2) ent vs))" 
      using ejec_append by blast
    also have "… =  ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))"
      using HI2 by simp
    also have "… = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))"
      using HI1 by simp
    also have "… = (f (valor e1 ent) (valor e2 ent))#vs" by simp
    also have "… = (valor (App f e1 e2) ent) # vs" by simp
    finally 
    show "ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" 
      by blast
  qed
qed
 
end

chapter {* Tema 9: Caso de estudio: Compilación de expresiones *} theory T9 imports Main begin text {* El objetivo de este tema es contruir un compilador de expresiones genéricas (construidas con variables, constantes y operaciones binarias) a una máquina de pila y demostrar su corrección. *} section {* Las expresiones y el intérprete *} text {* Definición. Las expresiones son las constantes, las variables (representadas por números naturales) y las aplicaciones de operadores binarios a dos expresiones. *} type_synonym 'v binop = "'v ⇒ 'v ⇒ 'v" datatype 'v expr = Const 'v | Var nat | App "'v binop" "'v expr" "'v expr" text {* Definición. [Intérprete] La función "valor" toma como argumentos una expresión y un entorno (i.e. una aplicación de las variables en elementos del lenguaje) y devuelve el valor de la expresión en el entorno. *} fun valor :: "'v expr ⇒ (nat ⇒ 'v) ⇒ 'v" where "valor (Const b) ent = b" | "valor (Var x) ent = ent x" | "valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))" text {* Ejemplo. A continuación mostramos algunos ejemplos de evaluación con el intérprete. *} lemma "valor (Const 3) id = 3 ∧ valor (Var 2) id = 2 ∧ valor (Var 2) (λx. x+1) = 3 ∧ valor (App (op +) (Const 3) (Var 2)) (λx. x+1) = 6 ∧ valor (App (op +) (Const 3) (Var 2)) (λx. x+4) = 9" by simp section {* La máquina de pila *} text {* Nota. La máquina de pila tiene tres clases de intrucciones: · cargar en la pila una constante, · cargar en la pila el contenido de una dirección y · aplicar un operador binario a los dos elementos superiores de la pila. *} datatype 'v instr = IConst 'v | ILoad nat | IApp "'v binop" text {* Definición. [Ejecución] La ejecución de la máquina de pila se modeliza mediante la función "ejec" que toma una lista de intrucciones, una memoria (representada como una función de las direcciones a los valores, análogamente a los entornos) y una pila (representada como una lista) y devuelve la pila al final de la ejecución. *} fun ejec :: "'v instr list ⇒ (nat⇒'v) ⇒ 'v list ⇒ 'v list" where "ejec [] ent vs = vs" | "ejec (i#is) ent vs = (case i of IConst v ⇒ ejec is ent (v#vs) | ILoad x ⇒ ejec is ent ((ent x)#vs) | IApp f ⇒ ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" text {* A continuación se muestran ejemplos de ejecución. *} lemma "ejec [IConst 3] id [7] = [3,7] ∧ ejec [ILoad 2, IConst 3] id [7] = [3,2,7] ∧ ejec [ILoad 2, IConst 3] (λx. x+4) [7] = [3,6,7] ∧ ejec [ILoad 2, IConst 3, IApp (op +)] (λx. x+4) [7] = [9,7]" by simp section {* El compilador *} text {* Definición. El compilador "comp" traduce una expresión en una lista de instrucciones. *} fun comp :: "'v expr ⇒ 'v instr list" where "comp (Const v) = [IConst v]" | "comp (Var x) = [ILoad x]" | "comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]" text {* A continuación se muestran ejemplos de compilación. *} lemma "comp (Const 3) = [IConst 3] ∧ comp (Var 2) = [ILoad 2] ∧ comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]" by simp section {* Corrección del compilador *} text {* Para demostrar que el compilador es correcto, probamos que el resultado de compilar una expresión y a continuación ejecutarla es lo mismo que interpretarla; es decir, *} theorem "ejec (comp e) ent [] = [valor e ent]" oops text {* El teorema anterior no puede demostrarse por inducción en e. Para demostrarlo, lo generalizamos a *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" oops text {* En la demostración del teorema anterior usaremos el siguiente lema. *} lemma ejec_append: "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume "?P xs" thus "?P (a#xs)" by (cases "a", auto) qed -- "La demostración detallada es" lemma ejec_append_1: "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume HI: "?P xs" thus "?P (a#xs)" proof (cases "a") case IConst thus ?thesis using HI by simp next case ILoad thus ?thesis using HI by simp next case IApp thus ?thesis using HI by simp qed qed text {* Una demostración más detallada del lema es la siguiente: *} lemma ejec_append_2: "∀vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume HI: "?P xs" thus "?P (a#xs)" proof (cases "a") fix v assume C1: "a=IConst v" show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs" using C1 by simp also have "… = ejec (xs@ys) ent (v#vs)" by simp also have "… = ejec ys ent (ejec xs ent (v#vs))" using HI by simp also have "… = ejec ys ent (ejec ((IConst v)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C1 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed next fix n assume C2: "a=ILoad n" show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs" using C2 by simp also have "… = ejec (xs@ys) ent ((ent n)#vs)" by simp also have "… = ejec ys ent (ejec xs ent ((ent n)#vs))" using HI by simp also have "… = ejec ys ent (ejec ((ILoad n)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C2 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed next fix f assume C3: "a=IApp f" show "∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs" using C3 by simp also have "… = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))" by simp also have "… = ejec ys ent (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" using HI by simp also have "… = ejec ys ent (ejec ((IApp f)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C3 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed qed qed text {* La demostración automática del teorema es *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" by (induct e) (auto simp add:ejec_append) text {* La demostración estructurada del teorema es *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" proof (induct e) fix v show "∀vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs" by simp next fix x show "∀vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs" by simp next fix f e1 e2 assume HI1: "∀vs. ejec (comp e1) ent vs = (valor e1 ent) # vs" and HI2: "∀vs. ejec (comp e2) ent vs = (valor e2 ent) # vs" show "∀vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" proof fix vs have "ejec (comp (App f e1 e2)) ent vs = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs" by simp also have "… = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)" using ejec_append by blast also have "… = ejec [IApp f] ent (ejec (comp e1) ent (ejec (comp e2) ent vs))" using ejec_append by blast also have "… = ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))" using HI2 by simp also have "… = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))" using HI1 by simp also have "… = (f (valor e1 ent) (valor e2 ent))#vs" by simp also have "… = (valor (App f e1 e2) ent) # vs" by simp finally show "ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" by blast qed qed end

Seguir leyendo →

RA2017: Deducción natural de primer orden con Isabelle/HOL

José A. Alonso-8 febrero 2018

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural de primer orden Isabelle/HOL. La presentación se basa en los ejemplos del tema 8 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

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

Seguir leyendo →

RA2017: Deducción natural proposicional con Isabelle/HOL

José A. Alonso-1 febrero 2018

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción naturalcon Isabelle/HOL. La presentación se basa en los ejemplos del tema 2 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

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

Seguir leyendo →

RA2017: Panorama de la demostración asistida por ordenador

José A. Alonso-21 diciembre 2017

En la clase de hoy del curso de Razonamiento automático se ha presentado un panorama del razonamiento automático a través de 4 sistemas:
Prover9, ACL2, PVS e Isabelle/HOL.

De cada sistema se ha mostrado ejemplos que resaltan sus objetivos y las aplicaciones construidas con cada uno.

Las transparencias usadas son las del tema 6.

Seguir leyendo →

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

José A. Alonso-14 diciembre 2017

En la primera parte de la clase de hoy del curso de Razonamiento automático 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 teoría utilizada es la siguiente

Seguir leyendo →

RA2017: Ejercicios de cuantificadores sobre listas en Isabelle/HOL

José A. Alonso-14 diciembre 2017

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios sobre cuantificadores sobre listas en Isabelle/HOL.

La teoría con las soluciones de los ejercicios es la siguiente

Seguir leyendo →

RA2017: Razonamiento por casos y por inducción en Isabelle/HOL

José A. Alonso-30 noviembre 2017

En la segunda parte de la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

el razonamiento por casos booleanos,
el razonamiento por casos booleanos sobre una variable,
el razonamiento por casos sobre listas,
el razonamiento por inducción sobre números naturales con patrones,
el razonamiento sobre definiciones con existenciales,
el uso de librerías auxiliares (como Parity) y
el uso de otros métodos de demostración (como presburg).

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

Seguir leyendo →

RA2017: Ejercicios de razonamiento detallado sobre programas en Isabelle/HOL

José A. Alonso-30 noviembre 2017

En la primera parte de la clase de hoy del curso de
Razonamiento automático se han comentado las soluciones de la 3ª relación de ejercicios sobre razonamiento detallado sobre programas en Isabelle/HOL

La teoría con las soluciones de los ejercicios es la siguiente

Seguir leyendo →

RA2017: Razonamiento estructurado sobre programas con Isabelle/HOL

José A. Alonso-23 noviembre 2017

En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.

Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.

Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

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

Seguir leyendo →

RA2017: Ejercicios de programación funcional con Isabelle/HOL

José A. Alonso-2 noviembre 2017

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la primera relación de ejercicios sobre programación funcional en Isabelle/HOL.

La teoría con las soluciones de los ejercicios es la siguiente

Seguir leyendo →

L	M	X	J	V	S	D
« May
			1	2	3	4
5	6	7	8	9	10	11
12	13	14	15	16	17	18
19	20	21	22	23	24	25
26	27	28	29	30

Etiqueta: RA2017