15 mayo 2013 – Vestigium

LMF2013: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)

PorJosé A. Alonso 15 mayo 201319 mayo 2013

En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland).

Además, se ha comentado la propuesta del 4º ejercicio evaluable consistente en la implementación en Haskell del algoritmo de DPLL y de refinamientos de resolución.

Las transparencias utilizadas son las del tema 6
Read More “LMF2013: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)”

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)))