15 diciembre 2015 – Vestigium

RA2015: Razonamiento estructurado sobre programas con Isabelle/HOL

PorJosé A. Alonso 15 diciembre 201518 diciembre 2015

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:
Read More “RA2015: Razonamiento estructurado sobre programas con Isabelle/HOL”

RA2015: Ejercicios de razonamiento automático sobre programas con Isabelle/HOL

PorJosé A. Alonso 15 diciembre 201518 diciembre 2015

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 2ª relación de ejercicios cuyo objetivo es demostrar automáticamente con Isabelle/HOL propiedades de programas.

Los ejercicios y sus soluciones se muestran a continuación

header {* R2: Razonamiento automático sobre programas *}

theory R2
imports Main 
begin

text {* --------------------------------------------------------------- 
  Ejercicio 1. Definir la función
     sumaImpares :: nat ⇒ nat
  tal que (sumaImpares n) es la suma de los n primeros números
  impares. Por ejemplo,
     sumaImpares 5  =  25
  ------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
  "sumaImpares 0 = 0"
| "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"

value "sumaImpares 5" -- "= 25"

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar que 
     sumaImpares n = n*n
  ------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"
by (induct n) auto

text {* --------------------------------------------------------------- 
  Ejercicio 3. Definir la función
     sumaPotenciasDeDosMasUno :: nat ⇒ nat
  tal que 
     (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. 
  Por ejemplo, 
     sumaPotenciasDeDosMasUno 3  =  16
  ------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
  "sumaPotenciasDeDosMasUno 0 = 2"
| "sumaPotenciasDeDosMasUno (Suc n) = 
      sumaPotenciasDeDosMasUno n + 2^(n+1)"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar que 
     sumaPotenciasDeDosMasUno n = 2^(n+1)
  ------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) auto

text {* --------------------------------------------------------------- 
  Ejercicio 5. Definir la función
     copia :: nat ⇒ 'a ⇒ 'a list
  tal que (copia n x) es la lista formado por n copias del elemento
  x. Por ejemplo, 
     copia 3 x = [x,x,x]
  ------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
  "copia 0 x       = []"
| "copia (Suc n) x = x # copia n x"

value "copia 3 x" -- "= [x,x,x]"

text {* --------------------------------------------------------------- 
  Ejercicio 6. Definir la función
     todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (todos p xs) se verifica si todos los elementos de xs cumplen
  la propiedad p. Por ejemplo,
     todos (λx. x>(1::nat)) [2,6,4] = True
     todos (λx. x>(2::nat)) [2,6,4] = False
  ------------------------------------------------------------------ *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p []     = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
  iguales a x. 
  ------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"
by (induct n) auto

text {* --------------------------------------------------------------- 
  Ejercicio 8. Definir la función
    factR :: nat ⇒ nat
  tal que (factR n) es el factorial de n. Por ejemplo,
    factR 4 = 24
  ------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
  "factR 0       = 1"
| "factR (Suc n) = Suc n * factR n"

value "factR 4" -- "= 24"

text {* --------------------------------------------------------------- 
  Ejercicio 9. Se considera la siguiente definición iterativa de la
  función factorial 
     factI :: "nat ⇒ nat" where
     factI n = factI' n 1
     
     factI' :: nat ⇒ nat ⇒ nat" where
     factI' 0       x = x
     factI' (Suc n) x = factI' n (Suc n)*x
  Demostrar que, para todo n y todo x, se tiene 
     factI' n x = x * factR n
  ------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
  "factI' 0       x = x"
| "factI' (Suc n) x = factI' n (x * Suc n)"

fun factI :: "nat ⇒ nat" where
  "factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact: 
  "factI' n x = x * factR n"
by (induct n arbitrary: x) 
   (auto simp del: mult_Suc)

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar que
     factI n = factR n
  ------------------------------------------------------------------- *}

corollary "factI n = factR n"
by (simp add: fact)

text {* --------------------------------------------------------------- 
  Ejercicio 11. Definir, recursivamente y sin usar (@), la función
     amplia :: 'a list ⇒ 'a ⇒ 'a list
  tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
  final de la lista xs. Por ejemplo,
     amplia [d,a] t = [d,a,t]
  ------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia []     y = [y]"
| "amplia (x#xs) y = x # amplia xs y"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar que 
     amplia xs y = xs @ [y]
  ------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"
by (induct xs) auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

header {* R2: Razonamiento automático sobre programas *}

theory R2

imports Main

begin

text {* ---------------------------------------------------------------

Ejercicio 1. Definir la función

sumaImpares :: nat ⇒ nat

tal que (sumaImpares n) es la suma de los n primeros números

impares. Por ejemplo,

sumaImpares 5 = 25

------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where

"sumaImpares 0 = 0"

| "sumaImpares (Suc n) = sumaImpares n + (2*n+1)"

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------

Ejercicio 2. Demostrar que

sumaImpares n = n*n

------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"

by (induct n) auto

text {* ---------------------------------------------------------------

Ejercicio 3. Definir la función

sumaPotenciasDeDosMasUno :: nat ⇒ nat

tal que

(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.

Por ejemplo,

sumaPotenciasDeDosMasUno 3 = 16

------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where

"sumaPotenciasDeDosMasUno 0 = 2"

| "sumaPotenciasDeDosMasUno (Suc n) =

sumaPotenciasDeDosMasUno n + 2^(n+1)"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------

Ejercicio 4. Demostrar que

sumaPotenciasDeDosMasUno n = 2^(n+1)

------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"

by (induct n) auto

text {* ---------------------------------------------------------------

Ejercicio 5. Definir la función

copia :: nat ⇒ 'a ⇒ 'a list

tal que (copia n x) es la lista formado por n copias del elemento

x. Por ejemplo,

copia 3 x = [x,x,x]

------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where

"copia 0 x = []"

| "copia (Suc n) x = x # copia n x"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------

Ejercicio 6. Definir la función

todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool

tal que (todos p xs) se verifica si todos los elementos de xs cumplen

la propiedad p. Por ejemplo,

todos (λx. x>(1::nat)) [2,6,4] = True

todos (λx. x>(2::nat)) [2,6,4] = False

------------------------------------------------------------------ *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where

"todos p [] = True"

| "todos p (x#xs) = (p x ∧ todos p xs)"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"

value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------

Ejercicio 7. Demostrar que todos los elementos de (copia n x) son

iguales a x.

------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"

by (induct n) auto

text {* ---------------------------------------------------------------

Ejercicio 8. Definir la función

factR :: nat ⇒ nat

tal que (factR n) es el factorial de n. Por ejemplo,

factR 4 = 24

------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where

"factR 0 = 1"

| "factR (Suc n) = Suc n * factR n"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------

Ejercicio 9. Se considera la siguiente definición iterativa de la

función factorial

factI :: "nat ⇒ nat" where

factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where

factI' 0 x = x

factI' (Suc n) x = factI' n (Suc n)*x

Demostrar que, para todo n y todo x, se tiene

factI' n x = x * factR n

------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where

"factI' 0 x = x"

| "factI' (Suc n) x = factI' n (x * Suc n)"

fun factI :: "nat ⇒ nat" where

"factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact:

"factI' n x = x * factR n"

by (induct n arbitrary: x)

(auto simp del: mult_Suc)

text {* ---------------------------------------------------------------

Ejercicio 10. Demostrar que

factI n = factR n

------------------------------------------------------------------- *}

corollary "factI n = factR n"

by (simp add: fact)

text {* ---------------------------------------------------------------

Ejercicio 11. Definir, recursivamente y sin usar (@), la función

amplia :: 'a list ⇒ 'a ⇒ 'a list

tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al

final de la lista xs. Por ejemplo,

amplia [d,a] t = [d,a,t]

------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where

"amplia [] y = [y]"

| "amplia (x#xs) y = x # amplia xs y"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------

Ejercicio 12. Demostrar que

amplia xs y = xs @ [y]

------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"

by (induct xs) auto

end

LI2015: Formas normales de Skolem y cláusulas

PorJosé A. Alonso 15 diciembre 201518 diciembre 2015

En la primera parte de la clase de hoy del curso de Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que sólo tenga cuantificadores al principio, que su cuerpo esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.

En la segunda parte se han comentado las soluciones de los ejercicios 8.5.1 y 8.5.5 del libro de ejercicios. Se han realizado las demostraciones por deducción natural y también por tableros semánticos. Además, se ha comprobado con tableros semánticos la validez de sus recíprocos.

Las transparencias de esta clase son las del tema 10