Menu Close

Etiqueta: Isabelle/HOL

Proyecto ForMatUS (Formalización de las Matemáticas de la US)

El proyecto ForMatUS tiene como objetivo la formalización de las matemáticas enseñadas en la Universidad de Sevilla, fundamentalmente las asignaturas del Grado en Matemáticas.

Los sistemas elegidos, inicialmente, para la formalización son Isabelle/HOL y Lean.

El primero, Isabelle/HOL, se ha usado en la asignatura de Lógica matemática y fundamentos (de 3º del Grado en Matemáticas) y en la de Razonamiento automático (del Máster Universitario en Lógica, Computación e Inteligencia Artificial). Además, este curso los vídeos de las clases con Isabelle/HOL se han subido a YouTube en la lista Razonamiento con Isabelle/HOL que puede servir como introducción al uso del sistema.

El segundo, Lean, no se ha usado aún en ninguna de las asignaturas de la Universidad de Sevilla; pero sí he elaborado durante este curso algunos apuntes sobre el mismo:

  • Resúmenes de Lean es una recopilación de enlaces con resúmenes sobre sintaxis y tácticas de Lean

El desarrollo del proyecto lo iré anunciando en Twitter con la etiqueta #ForMatUS.

Reseña: A comprehensive framework for saturation theorem proving

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre lógica titulado A comprehensive framework for saturation theorem proving.

Sus autores son

Su resumen es

One of the indispensable operations of realistic saturation theorem provers is (backward and forward) deletion of subsumed formu- las. In presentations of proof calculi, however, this is usually discussed only informally, and in the rare cases where there is a formal exposition, it is typically clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but using a standard notion of redundancy, a clause C does not make an instance Cσ redundant.

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle/HOL.

El trabajo es parte del proyecto Matryoshka (Fast interactive verification through strong higher-order automation)

El código está incluido en el repositorio IsaFoL (Isabelle Formalization of Logic).

RA2019: Programación funcional con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado la programación funcional en Isabelle/HOL.

La teoría con los ejemplos presentados en la clase es T1_Programacion_funcional_en_Isabelle.thy.

chapter ‹ Tema 1: Programación funcional en Isabelle ›
 
theory T1_Programacion_funcional_en_Isabelle
imports Main 
begin
 
section ‹ Introducción ›
 
text ‹ En este tema se presenta el lenguaje funcional que está
  incluido en Isabelle. El lenguaje funcional es muy parecido a
  Haskell. ›
 
section ‹ Números naturales, enteros y booleanos ›
 
text ‹ En Isabelle están definidos los número naturales con la sintaxis
  de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).
 
  Los números como el 1 son abreviaturas de los correspondientes en la
  notación de Peano, en este caso "Suc 0". 
 
  El tipo de los números naturales es nat. 
 
  Por ejemplo, el siguiente del 0 es el 1. ›
 
value "Suc 0"  
(* ↝ "1" :: "nat"*)
 
text ‹ En Isabelle está definida la suma de los números naturales:
  (x + y) es la suma de x e y.
 
  Por ejemplo, la suma de los números naturales 1 y 2 es el número
  natural 3. ›
 
value "(1::nat) + 2" 
(* ↝ "3" :: "nat" *)
 
value "(1::nat) + 2 = 3"
(* ↝ "True" :: "bool" *) 
 
text ‹ La notación del par de dos puntos se usa para asignar un tipo a
  un término (por ejemplo, (1::nat) significa que se considera que 1 es
  un número natural).   
 
  En Isabelle está definida el producto de los números naturales:
  (x * y) es el producto de x e y.
 
  Por ejemplo, el producto de los números naturales 2 y 3 es el número
  natural 6. ›
 
value "(2::nat) * 3" 
(* ↝ "6" :: "nat"*)
 
value "(2::nat) * 3 = 6"
(* ↝ "True" :: "bool" *) 
 
text ‹ En Isabelle está definida la división de números naturales: 
  (n div m) es el cociente entero de x entre y.
 
  Por ejemplo, la división natural de 7 entre 3 es 2. ›
 
value "(7::nat) div 3"
(* ↝ "2" :: "nat" *)
 
value "(7::nat) div 3 = 2"
(* ↝ "True" :: "bool" *)
 
text ‹ En Isabelle está definida el resto de división de números
  naturales: (n mod m) es el resto de dividir n entre m.
 
  Por ejemplo, el resto de dividir 7 entre 3 es 1. ›
 
value "(7::nat) mod 3"
(* ↝ "1" :: "nat" *)
 
text ‹ En Isabelle también están definidos los números enteros. El tipo
  de los enteros se representa por int.
 
  Por ejemplo, la suma de 1 y -2 es el número entero -1. ›
 
value "(1::int) + -2"  
(* ↝ "- 1" :: "int"*)
 
text ‹ Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
  un natural o un entero, dependiendo del contexto. 
 
  Isabelle resuelve ambigüedades mediante inferencia de tipos.
 
  A veces, es necesario usar declaraciones de tipo para resolver la
  ambigüedad.
 
  En Isabelle están definidos los valores booleanos (True y False), las
  conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃). 
 
  El tipo de los booleanos es bool. ›
 
text ‹ La conjunción de dos fórmulas verdaderas es verdadera. ›
value "True ∧ True"  
(* ↝ "True" :: "bool" *)
 
text ‹ La conjunción de un fórmula verdadera y una falsa es falsa. › 
value "True ∧ False"  
(* ↝ "False" :: "bool" *)
 
text ‹ La disyunción de una fórmula verdadera y una falsa es
  verdadera. › 
value "True ∨ False" 
(* ↝ "True" :: "bool" *)
 
text ‹ La disyunción de dos fórmulas falsas es falsa. ›
value "False ∨ False" 
(* ↝ "False" :: "bool"*)
 
text ‹ La negación de una fórmula verdadera es falsa. ›
value "¬True" 
(* ↝ "False" :: "bool"*)
 
text ‹ Una fórmula falsa implica una fórmula verdadera. ›
value "False ⟶ True" 
(* ↝ "True" :: "bool"*)
 
text ‹ Un lema introduce una proposición seguida de una demostración. 
 
  Isabelle dispone de varios procedimientos automáticos para generar
  demostraciones, uno de los cuales es el de simplificación (llamado
  simp). 
 
  El procedimiento simp aplica un conjunto de reglas de reescritura, que
  inicialmente contiene un gran número de reglas relativas a los objetos
  definidos. ›
 
text ‹ Ej. de simp: Todo elemento es igual a sí mismo. ›
lemma "∀x. x = x" 
by simp
 
text ‹ Ej. de simp: Existe un elemento igual a 1. ›
lemma "∃x. x = 1" 
by simp
 
section ‹ Definiciones no recursivas ›
 
text ‹ La disyunción exclusiva de A y B se verifica si una es verdadera
  y la otra no lo es. ›
 
definition xor :: "bool ⇒ bool ⇒ bool" where
  "xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"
 
text ‹ Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
  falsa. 
 
  Dem.: Por simplificación, usando la definición de la disyunción
  exclusiva. 
›
 
lemma "xor True True = False"
by (simp add: xor_def)
 
text ‹ Se añade la definición de la disyunción exclusiva al conjunto de
  reglas de simplificación automáticas. ›
 
declare xor_def [simp]
 
lemma "xor True False = True"
by simp
 
section ‹ Definiciones locales ›
 
text ‹ Se puede asignar valores a variables locales mediante 'let' y
  usarlo en las expresiones dentro de 'in'. 
 
  Por ejemplo, si x es el número natural 3, entonces "x*x = 9". ›
 
value "let x = 3::nat in x * x" 
(* ↝ "9" :: "nat" *)
 
section ‹ Pares ›
 
text ‹ Un par se representa escribiendo los elementos entre paréntesis
  y separados por coma.
 
  El tipo de los pares es el producto de los tipos.
 
  La función fst devuelve el primer elemento de un par y la snd el
  segundo. 
 
  Por ejemplo, si p es el par de números naturales (2,3), entonces la
  suma del primer elemento de p y 1 es igual al segundo elemento de
  p. › 
 
value "let p = (2,3)::nat × nat in fst p + 1 = snd p" 
(* ↝ "True" :: "bool" *)
 
section ‹ Listas ›
 
text ‹ Una lista se representa escribiendo los elementos entre
  corchetes y separados por comas.
 
  La lista vacía se representa por [].
 
  Todos los elementos de una lista tienen que ser del mismo tipo.
 
  El tipo de las listas de elementos del tipo a es (a list).
 
  El término (x#xs) representa la lista obtenida añadiendo el elemento x
  al principio de la lista xs. 
 
  Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
  vacía los elementos z, y y x a es [x,y,z]. ›
 
value "x#(y#(z#[]))" 
(* ↝ "[x, y, z]" :: "'a list" *)
 
value "(1::int)#(2#(3#[]))"
(* ↝ "[1, 2, 3]" :: "int list" *)
 
text ‹ Funciones de descomposición de listas:
  · (hd xs) es el primer elemento de la lista xs.
  · (tl xs) es el resto de la lista xs.
 
  Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
  y el resto de xs es [b,c]. › 
 
value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" 
(* ↝ "True" :: "bool" *)
 
text ‹ (length xs) es la longitud de la lista xs. Por ejemplo, la
  longitud de la lista [1,2,5] es 3. ›
 
value "length [1::nat,2,5]" 
(* ↝ "3" :: "nat" *)
 
text ‹ En la página 10 de "What's in Main" 
  https://isabelle.in.tum.de/dist/Isabelle2018/doc/main.pdf
  y en la sesión 66 de "Isabelle/HOL — Higher-Order Logic"
  https://isabelle.in.tum.de/dist/library/HOL/HOL/document.pdf
  se encuentran más definiciones y propiedades de las listas. ›
 
section ‹ Funciones anónimas ›
 
text ‹ En Isabelle pueden definirse funciones anónimas.  
 
  Por ejemplo, el valor de la función que a un número le asigna su doble
  aplicada a 1 es 2. ›
 
value "(λx. x + x) 1::nat" 
(* ↝ "2" :: "nat" *)
 
section ‹ Condicionales ›
 
text ‹ El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso 
  contrario. ›
 
definition absoluto :: "int ⇒ int" where
  "absoluto x ≡ (if x ≥ 0 then x else -x)"
 
text ‹ Ejemplo, el valor absoluto de -3 es 3. ›
 
value "absoluto(-3)" 
(* ↝ "3" :: "int" *)
 
text ‹ Def.: Un número natural n es un sucesor si es de la forma 
  (Suc m). ›
 
definition es_sucesor :: "nat ⇒ bool" where
  "es_sucesor n ≡ (case n of 
    0     ⇒ False 
  | Suc m ⇒ True)"
 
text ‹ Ejemplo, el número 3 es sucesor. ›
 
value "es_sucesor 3" 
(* ↝ "True" :: "bool" *)
 
section ‹ Tipos de datos y definiciones recursivas ›
 
text ‹ Una lista de elementos de tipo a es la lista Vacia o se obtiene
  añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
  tipo a. › 
 
datatype 'a Lista = Vacia | Cons 'a "'a Lista"
 
text ‹ (conc xs ys) es la concatenación de las lista xs e ys. Por
  ejemplo, 
     conc (Cons a (Cons b Vacia)) (Cons c Vacia)
     = Cons a (Cons b (Cons c Vacia))
›
 
fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
  "conc Vacia ys       = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"
 
value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
(* ↝ Lista.Cons a (Lista.Cons b (Lista.Cons c Vacia)) *)
 
text ‹ Se puede declarar que acorte los nombres. ›
 
declare [[names_short]]
 
value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
(* ↝ Cons a (Cons b (Cons c Vacia) *)
 
text ‹ (suma n) es la suma de los primeros n números naturales. Por
  ejemplo,
     suma 3 = 6
›
 
fun suma :: "nat ⇒ nat" where
  "suma 0       = 0"
| "suma (Suc m) = (Suc m) + suma m"
 
value "suma 3" 
(* ↝ "6" :: nat *)
 
text ‹ (sumaImpares n) es la suma de los n primeros números impares. 
  Por ejemplo, 
     sumaImpares 3 = 9
›
 
fun sumaImpares :: "nat ⇒ nat" where
  "sumaImpares 0       = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"
 
value "sumaImpares 3" 
(* ↝ "9" :: nat *)
 
end

Como tarea se propuso la resolución de los ejercicios de la 1ª relación.

RA2018: Definiciones inductivas en IsabelleHOL

En la primera 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 11: Definiciones inductivas *}
 
theory T11_Definiciones_inductivas
imports Main
begin
 
section {* El conjunto de los números pares *}
 
text {* 
  · El conjunto de los números pares se define inductivamente como el
    menor conjunto que contiene al 0 y es cerrado por la operación (+2).
 
  · El conjunto de los números pares también puede definirse como los 
    naturales divisible por 2.
 
  · Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
    se demuestra su equivalencia.
*}
 
subsection {* Definición inductiva del conjunto de los pares *}
 
inductive_set par :: "nat set" where
  cero [intro!]: "0 ∈ par" 
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
 
text {*
  · Una definición inductiva está formada con reglas de introducción.
 
  · La definición inductiva genera varios teoremas:
    · par.cero:   0 ∈ par
    · par.paso:   n ∈ par ⟹ Suc (Suc n) ∈ par
    · par.simps:  (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))
*}
 
subsection {* Uso de las reglas de introducción *}
 
text {*
  Lema: Los números de la forma 2*k son pares.
*}
 
― ‹La demostración automática es›
lemma dobles_son_pares [intro!]: 
  "2*k ∈ par"
by (induct k) auto
 
― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
  "2*k ∈ par"
proof (induct k)
  show "2 * 0 ∈ par" by auto
next
  show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
qed
 
text {*
  · Nota: Nuestro objetivo es demostrar la equivalencia de la definición
    anterior y la definición mediante divisibilidad (even).
 
  · Lema: Si n es divisible por 2, entonces es par.
*}
 
lemma even_imp_par: "even n ⟹ n ∈ par"
by auto
 
subsection {* Regla de inducción *} 
 
text {*
  Entre las reglas generadas por la definión de par está la de
  inducción:
  · par.induct: ⟦ x ∈ par; 
                 P 0; 
                 ⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧ 
                ⟹ P x
*}
 
text {*
  Lema: Los números pares son divisibles por 2.
*} 
 
― ‹1ª demostración (detallada)lemma par_imp_even: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
― ‹2ª demostración (con arith)lemma par_imp_even_2: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed
 
― ‹3ª demostración (automática)lemma par_imp_even_3: 
  "n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)
 
text {*
  Lema: Un número n es par syss es divisible por 2. 
*}
 
theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)
 
subsection{* Generalización y regla de inducción *}
 
text {*
  · Antes de aplicar inducción se debe de generalizar la fórmula a
    probar.
 
  · Vamos a ilustrar el principio anterior en el caso de los conjuntos
    inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
    entonces n también lo es.
 
  · El siguiente intento falla:
*}
 
lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
  apply (erule par.induct) 
oops
 
text {*
  En el intento anterior, los subobjetivos generados son
     1. n ∈ par
     2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
  que no se pueden demostrar.
 
  Se ha perdido la información sobre Suc (Suc n).
*}
 
text {*
  Reformulación del lema: Si n es par, entonces n-2 también lo es.
*}
 
― ‹La demostración automática es›
lemma par_imp_par_menos_2: 
  "n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto
 
― ‹La demostración estructurada es›
lemma "n ∈  par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
  show "0 - 2 ∈ par" by auto
next
  show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed
 
text {* 
  Con el lema anterior se puede demostrar el original.
*}
 
― ‹La demostración estructurada es›
lemma
  assumes "Suc (Suc n) ∈ par" 
  shows   "n ∈ par"
proof -
  have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)
  then show "n ∈ par" by simp 
qed
 
― ‹La demostración aplicativa es›
lemma 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2) 
apply simp
done
 
(* Comentar el uso de drule *)
 
― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par: 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
by (drule par_imp_par_menos_2, simp)
 
text {*
  Lemma. Un número natural n es par syss n+2 es par.
*}
 
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)
 
text {*
  Se usa el atributo "iff" porque sirve como regla de simplificación.
*}
 
subsection {* Definiciones mutuamente inductivas *}
 
text {*
  Definición cruzada de los conjuntos inductivos de los pares y de los 
  impares:
*}
 
inductive_set
  Pares    :: "nat set" and
  Impares  :: "nat set"
where
  ceroP:    "0 ∈ Pares"
| ParesI:   "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares   ⟹ Suc n ∈ Impares"
 
text {*
  El esquema de inducción generado por la definición anterior es
  · Pares_Impares.induct:
    ⟦P1 0; 
     ⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
     ⋀n. ⟦n ∈ Pares;   P1 n⟧ ⟹ P2 (Suc n)⟧
    ⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)
*}
 
text {*
  Ejemplo de demostración usando el esquema anterior.
*}
 
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
  show "even (0::nat)" by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Impares" and
         H2: "even (Suc n)"
  show "even (Suc n)" using H2 by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Pares" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
subsection {* Definición inductiva de predicados *}
 
text {*
  Definición inductiva del predicado es_par tal que (es_par n) se
  verifica si n es par.
*}
 
inductive es_par :: "nat ⇒ bool" where
  "es_par 0" 
| "es_par n ⟹ es_par (Suc(Suc n))"
 
text {*
  Heurística para elegir entre definir conjuntos o predicados:
  · si se va a combinar con operaciones conjuntistas, definir conjunto;
  · en caso contrario, definir predicado.
*}
 
end

Como ejercicio se propuso la relación 8 sobre gramáticas libres de contexto.

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

En la primera parte de 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:

RA2018: Deducción natural proposicional con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha completado la presentación de la deducción natural con Isabelle/HOL que se empezó en la clase anterior.

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: