LMF2013 – Página 2

LMF2013: Resolución proposicional en Haskell

PorJosé A. Alonso 15 mayo 201319 mayo 2013

En la primera parte de la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de la resolución proposicional.

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa los módulos

desaroolado en clases anteriores.

La implementación de resolución comentada es

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes                                                        --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    resolvente :: Clausula -> Clausula -> Literal -> Clausula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
--    resolvente [no p,q] [no q,r] q  ==>  [no p,r]
--    resolvente [no p,no q] [q,r] (no q)  ==>  [no p,r]
--    resolvente [no p,q] [no p,no q] q  ==>  [no p]
-- ---------------------------------------------------------------------

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 l =
    union (delete l c1) (delete (complementario l) c2) 

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    resolventes :: Clausula -> Clausula -> [Clausula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
--    resolventes [no p,q] [p,no q]  ==>  [[q,no q],[no p,p]]
--    resolventes [no p,q] [p,q]     ==>  [[q]]
-- ---------------------------------------------------------------------

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 =
    [resolvente c1 c2 l | l <- c1, (complementario l) `elem` c2]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo, 
--    resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
--    ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s =
    unionGeneral [resolventes c c1 | c1 <- s]

-- ---------------------------------------------------------------------
-- Eliminación de tautologías                                         --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    esTautologia :: Cláusula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo, 
--    esTautologia [p, q, no p]  ==>  True
--    esTautologia [p, q, no r]  ==>  False
--    esTautologia []            ==>  False
-- ---------------------------------------------------------------------

esTautologia :: Clausula -> Bool
esTautologia c = 
    [f | f <- c, elem (complementario f) c] /= []

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    eliminaTautologias :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
--    eliminaTautologias [[p, q], [p, q, no p]]  ==>  [[p,q]]
-- ---------------------------------------------------------------------

eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias s =
    [c | c <- s, not (esTautologia c)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
--    esInconsistentePorResolucion :: [Clausula] -> Bool
-- tal que (esInconsistentePorResolucion s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
--    esInconsistentePorResolucion [[p],[no p,q],[no q]]
--    ==> True
--    esInconsistentePorResolucion [[p],[no p,q]]
--    ==> False
--    esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]
--    ==> True
--    esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]
--    ==> True
-- ---------------------------------------------------------------------

esInconsistentePorResolucion :: [Clausula] -> Bool
esInconsistentePorResolucion s =
    esInconsistentePorResolucion' s []

esInconsistentePorResolucion' :: [Clausula] -> [Clausula] -> Bool
esInconsistentePorResolucion' soporte usables 
    | null soporte    = False
    | elem [] soporte = True
    | otherwise       =
        esInconsistentePorResolucion' soporte' usables'
        where actual   = head soporte
              usables' = union [actual] usables
              soporte' = union (tail soporte)
                               [c 
                                | c <- resolventesClausulaConjunto
                                       actual 
                                       usables'
                                , not (esTautologia c)
                                , notElem c soporte
                                , notElem c usables']

-- ---------------------------------------------------------------------
-- Validez mediante resolución                                        --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
--    esValidaPorResolución :: Prop -> Bool
-- tal que (esValidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo, 
--    esValidaPorResolución (p --> p)                 ==>  True
--    esValidaPorResolución ((p --> q) \/ (q --> p))  ==>  True
--    esValidaPorResolución (p --> q)                 ==>  False
-- ---------------------------------------------------------------------

esValidaPorResolución :: Prop -> Bool
esValidaPorResolución f =
    esInconsistentePorResolucion 
    (eliminaTautologias (clausulas (Neg f)))

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución                                   --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
--    esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
--    esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)  
--    ==> True
--    esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)
--    ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolucion s f =
    esInconsistentePorResolucion 
    (eliminaTautologias (clausulasConjunto ((Neg f):s)))

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

module ResolucionProposicional where

import SintaxisSemantica

import FormasNormales

import Clausulas

import Data.List

-- ---------------------------------------------------------------------

-- Resolventes --

-- ---------------------------------------------------------------------

-- Ejercicio 1: Definir la función

-- resolvente :: Clausula -> Clausula -> Literal -> Clausula

-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del

-- literal l. Por ejemplo,

-- resolvente [no p,q] [no q,r] q ==> [no p,r]

-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]

-- resolvente [no p,q] [no p,no q] q ==> [no p]

-- ---------------------------------------------------------------------

resolvente :: Clausula -> Clausula -> Literal -> Clausula

resolvente c1 c2 l =

union (delete l c1) (delete (complementario l) c2)

-- ---------------------------------------------------------------------

-- Ejercicio 2: Definir la función

-- resolventes :: Clausula -> Clausula -> [Clausula]

-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y

-- c2. Por ejemplo,

-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]

-- resolventes [no p,q] [p,q] ==> [[q]]

-- ---------------------------------------------------------------------

resolventes :: Clausula -> Clausula -> [Clausula]

resolventes c1 c2 =

[resolvente c1 c2 l | l <- c1, (complementario l) `elem` c2]

-- ---------------------------------------------------------------------

-- Ejercicio 3: Definir la función

-- resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]

-- tal que (resolventes c s) es el conjunto de las resolventes de c y

-- s. Por ejemplo,

-- resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]

-- ==> [[q],[q,r],[no p,s]]

-- ---------------------------------------------------------------------

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]

resolventesClausulaConjunto c s =

unionGeneral [resolventes c c1 | c1 <- s]

-- ---------------------------------------------------------------------

-- Eliminación de tautologías --

-- ---------------------------------------------------------------------

-- Ejercicio 1: Definir la función

-- esTautologia :: Cláusula -> Bool

-- tal que (esTautologia c) se verifica si c es una tautología. Por

-- ejemplo,

-- esTautologia [p, q, no p] ==> True

-- esTautologia [p, q, no r] ==> False

-- esTautologia [] ==> False

-- ---------------------------------------------------------------------

esTautologia :: Clausula -> Bool

esTautologia c =

[f | f <- c, elem (complementario f) c] /= []

-- ---------------------------------------------------------------------

-- Ejercicio 2: Definir la función

-- eliminaTautologias :: [Cláusula] -> [Cláusula]

-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las

-- tautologías de s. Por ejemplo,

-- eliminaTautologias [[p, q], [p, q, no p]] ==> [[p,q]]

-- ---------------------------------------------------------------------

eliminaTautologias :: [Clausula] -> [Clausula]

eliminaTautologias s =

[c | c <- s, not (esTautologia c)]

-- ---------------------------------------------------------------------

-- Decisión de inconsistencia por resolución --

-- ---------------------------------------------------------------------

-- Ejercicio 4: Definir la función

-- esInconsistentePorResolucion :: [Clausula] -> Bool

-- tal que (esInconsistentePorResolucion s) se verifica si s es

-- inconsistente mediante resolución. Por ejemplo,

-- esInconsistentePorResolucion [[p],[no p,q],[no q]]

-- ==> True

-- esInconsistentePorResolucion [[p],[no p,q]]

-- ==> False

-- esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]

-- ==> True

-- esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]

-- ==> True

-- ---------------------------------------------------------------------

esInconsistentePorResolucion :: [Clausula] -> Bool

esInconsistentePorResolucion s =

esInconsistentePorResolucion' s []

esInconsistentePorResolucion' :: [Clausula] -> [Clausula] -> Bool

esInconsistentePorResolucion' soporte usables

| null soporte = False

| elem [] soporte = True

| otherwise =

esInconsistentePorResolucion' soporte' usables'

where actual = head soporte

usables' = union [actual] usables

soporte' = union (tail soporte)

| c <- resolventesClausulaConjunto

actual

usables'

, not (esTautologia c)

, notElem c soporte

, notElem c usables']

-- ---------------------------------------------------------------------

-- Validez mediante resolución --

-- ---------------------------------------------------------------------

-- Ejercicio 5: Definir la función

-- esValidaPorResolución :: Prop -> Bool

-- tal que (esValidaPorResolución f) se verifica si f es válida por

-- resolución. Por ejemplo,

-- esValidaPorResolución (p --> p) ==> True

-- esValidaPorResolución ((p --> q) \/ (q --> p)) ==> True

-- esValidaPorResolución (p --> q) ==> False

-- ---------------------------------------------------------------------

esValidaPorResolución :: Prop -> Bool

esValidaPorResolución f =

esInconsistentePorResolucion

(eliminaTautologias (clausulas (Neg f)))

-- ---------------------------------------------------------------------

-- Consecuencia mediante resolución --

-- ---------------------------------------------------------------------

-- Ejercicio 6: Definir la función

-- esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool

-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es

-- consecuencia de s mediante el método de resolución. Por ejemplo,

-- esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)

-- ==> True

-- esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)

-- ==> False

-- ---------------------------------------------------------------------

esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool

esConsecuenciaPorResolucion s f =

esInconsistentePorResolucion

(eliminaTautologias (clausulasConjunto ((Neg f):s)))

LMF2013: Modelos de Herbrand

PorJosé A. Alonso 14 mayo 201319 mayo 2013

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado cómo puede puede reducirse la consistencia de conjuntos de cláusulas de primer orden a la consistencia de conjuntos de cláusulas proposicionales.

En primer lugar, se ha observado que la reducción es inmediata en el caso de fórmulas sin variables.

A continuación se han presentado procedimientos para construir los universos de Herbrand, las bases de Herbrand y las interpretaciones de Herbrand. Así como un procedimiento que transforma modelos de conjuntos de cláusulas en modelos de Herbrand. Por tanto, la consistencia de un conjunto de cláusulas se reduce a la búsqueda de modelos de Herbrand.

Finalmente, se ha explicado el teorema de Herbrand y su aplicación para decidir la consistencia de un conjunto de cláusulas buscando un subconjunto finito de su extensión de Herbrand que sea consistente (en el sentido proposicional).

Las transparencias de la clase son las del tema 11.

LMF013: Formas normales de Skolem y cláusulas

PorJosé A. Alonso 14 mayo 201319 mayo 2013

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que 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.

Las transparencias de esta clase son las del tema 10
Read More “LMF013: Formas normales de Skolem y cláusulas”

LMF2013: Cláusulas en Haskell

PorJosé A. Alonso 10 mayo 2013

En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de las cláusulas.

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa el módulo SintaxisSemantica desarrollado en la clase del día 27 de febrero y el módulo FormasNormales desarrollado en la clase del día 8 de mayo.
Read More “LMF2013: Cláusulas en Haskell”

LMF2013: Formas normales conjuntivas y disyuntivas en Haskell

PorJosé A. Alonso 8 mayo 201310 mayo 2013

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa el módulo SintaxisSemantica desarrollado en la clase del día 27 de febrero.
Read More “LMF2013: Formas normales conjuntivas y disyuntivas en Haskell”