Relación 9 - Historial de revisiones

Fracarmol1 en 17:53 25 abr 2015

2015-04-25T17:53:00Z

Fracarmol1 en 12:17 22 abr 2015

2015-04-22T12:17:48Z

Fracarmol1 en 12:08 22 abr 2015

2015-04-22T12:08:15Z

Fracarmol1 en 17:31 20 abr 2015

2015-04-20T17:31:47Z

Mjoseh: Página creada con ' -- FormasNormales.hs -- Formas normales. -- --------------------------------------------------------------------- module FormasNormales where -- ----...'

2015-04-17T08:03:11Z

Página creada con '<source lang = "haskell"> -- FormasNormales.hs -- Formas normales. -- --------------------------------------------------------------------- module FormasNormales where -- ----...'

Página nueva

<source lang = "haskell">
-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------

module FormasNormales where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import Data.List

-- ---------------------------------------------------------------------
-- Equivalencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
-- esEquivalente (p <--> q) ((p --> q) /\ (q --> p)) ==> True
-- esEquivalente (p --> q) ((no p) \/ q) ==> True
-- esEquivalente (p /\ q) (no ((no p) \/ (no q))) ==> True
-- esEquivalente (p \/ q) (no ((no p) /\ (no q))) ==> True
-- ---------------------------------------------------------------------

esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
-- eliminaEquivalencias (p <--> q)
-- ==> ((p --> q) /\ (q --> p))
-- eliminaEquivalencias ((p <--> q) /\ (q <--> r))
-- ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------

eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
-- eliminaImplicaciones (p --> q)
-- ==> (no p \/ q)
-- eliminaImplicaciones (eliminaEquivalencias (p <--> q))
-- ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------

eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- interiorizaNegación :: Prop -> Prop
-- tal que (interiorizaNegación f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
-- interiorizaNegación (no (no p)) ==> p
-- interiorizaNegación (no (p /\ q)) ==> (no p \/ no q)
-- interiorizaNegación (no (p \/ q)) ==> (no p /\ no q)
-- interiorizaNegación (no (no (p \/ q))) ==> (p \/ q)
-- interiorizaNegación (no ((no p) \/ q)) ==> (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones.
-- ---------------------------------------------------------------------

interiorizaNegación :: Prop -> Prop
interiorizaNegación = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
-- formaNormalNegativa (p <--> q)
-- ==> ((no p \/ q) /\ (no q \/ p))
-- formaNormalNegativa ((p \/ (no q)) --> r)
-- ==> ((no p /\ q) \/ r)
-- formaNormalNegativa ((p /\ (q --> r)) --> s)
-- ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------

formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f = undefined

-- ---------------------------------------------------------------------
-- Literales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo,
-- literal p ==> True
-- literal (no p) ==> True
-- literal (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula.
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
-- complementario p ==> no p
-- complementario (no p) ==> p
-- ---------------------------------------------------------------------

complementario :: Literal -> Literal
complementario = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- literalesFórmulaFNN :: Prop -> [Literal]
-- tal que (literalesFórmulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
-- literalesFórmulaFNN (p \/ ((no q) \/ r)) ==> [p,no q,r]
-- literalesFórmulaFNN p ==> [p]
-- literalesFórmulaFNN (no p) ==> [no p]
-- ---------------------------------------------------------------------

literalesFórmulaFNN :: Prop -> [Literal]
literalesFórmulaFNN = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- interiorizaDisyunción :: Prop -> Prop
-- tal que (interiorizaDisyunción f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,
-- interiorizaDisyunción (p \/ (q /\ r)) ==> ((p \/ q) /\ (p \/ r))
-- interiorizaDisyunción ((p /\ q) \/ r) ==> ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaDisyunción :: Prop -> Prop
interiorizaDisyunción = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
-- formaNormalConjuntiva (p /\ (q --> r))
-- ==> (p /\ (no q \/ r))
-- formaNormalConjuntiva (no (p /\ (q --> r)))
-- ==> ((no p \/ q) /\ (no p \/ no r))
-- formaNormalConjuntiva (no(p <--> r))
-- ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------

formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f = undefined

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

-- Ejercicio 11.2: Definir la función
-- validaPorFNC:: Prop -> Bool
-- tal que (validaPorFNC f) comprueba si f es válida. Por ejemplo,
-- validaPorFNC ((p --> q) \/ (q --> p)) == True
-- validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
-- validaPorFNC (p --> p) == True

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

validaPorFNC:: Prop -> Bool
validaPorFNC = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- interiorizaConjunción :: Prop -> Prop
-- tal que (interiorizaConjunción f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,
-- interiorizaConjunción (p /\ (q \/ r)) ==> ((p /\ q) \/ (p /\ r))
-- interiorizaConjunción ((p \/ q) /\ r) ==> ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaConjunción :: Prop -> Prop
interiorizaConjunción = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
-- formaNormalDisyuntiva (p /\ (q --> r))
-- ==> ((p /\ no q) \/ (p /\ r))
-- formaNormalDisyuntiva (no (p /\ (q --> r)))
-- ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------

formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- satisfaciblePorFND:: Prop -> Bool
-- tal que (satisfaciblePorFND f) comprueba si f es satisfacible. Por
-- ejemplo,
-- satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
-- satisfaciblePorFND (p /\ (no p)) == False
-- satisfaciblePorFND ((p --> q) \/ (q --> p)) == True

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

satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = undefined

</source>

@@ Línea 31: / Línea 31: @@
 esEquivalente :: Prop -> Prop -> Bool
-esEquivalente f g = modelosFormula f == modelosFormula g
+esEquivalente f g = esValida (Equi f g)
 -- ---------------------------------------------------------------------
@@ Línea 51: / Línea 51: @@
 eliminaEquivalencias :: Prop -> Prop
-eliminaEquivalencias (Equi h g) = Conj (Impl h g) (Impl g h)
+eliminaEquivalencias (Equi h g) = Conj (Impl (eliminaEquivalencias h) (eliminaEquivalencias g))
 eliminaEquivalencias (Impl h g) = Impl (eliminaEquivalencias h)
                                         (eliminaEquivalencias g)
@@ Línea 77: / Línea 79: @@
 eliminaImplicaciones :: Prop -> Prop
-eliminaImplicaciones (Impl h g) = Disj (Neg h) g
+eliminaImplicaciones (Impl h g) = Disj (Neg (eliminaImplicaciones h)) (eliminaImplicaciones g)
 eliminaImplicaciones (Conj h g) = Conj (eliminaImplicaciones h)
                                         (eliminaImplicaciones g)

@@ Línea 255: / Línea 255: @@
 comprobacion f = or [elem (complementario (head x)) (drop 1 x)
                                           | x <- ordenaEnPares f]
 -- ---------------------------------------------------------------------

@@ Línea 171: / Línea 171: @@
 -- Francisco Javier Carmona
-literalesFórmulaFNN :: Prop -> [Literal]
+literalesFormulaFNN :: Prop -> [Literal]
-literalesFormulaFNN (Disj f g) =
+literalesFormulaFNN (Atom f) = [Atom f]
-         (literalesFormulaFNN f) `union` (literalesFormulaFNN g)
+literalesFormulaFNN (Neg f) | literal (Neg f) = [(Neg f)]
-literalesFormulaFNN (Conj f g) =
+                            | otherwise = literalesFormulaFNN f
-         (literalesFormulaFNN f) `union` (literalesFormulaFNN g)
+literalesFormulaFNN (Disj f g) = nub (aux f g)
-literalesFormulaFNN f = [f]
+literalesFormulaFNN (Conj f g) = nub (aux f g)
 -- ---------------------------------------------------------------------
@@ Línea 194: / Línea 200: @@
 interiorizaDisyunción :: Prop -> Prop
 interiorizaDisyunción = undefined
 -- ---------------------------------------------------------------------
@@ Línea 208: / Línea 214: @@
 --    ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
 -- ---------------------------------------------------------------------
 formaNormalConjuntiva :: Prop -> Prop
-formaNormalConjuntiva f = undefined
+formaNormalConjuntiva f = interiorizaDisyuncion (interiorizaNegacion
 -- ---------------------------------------------------------------------
@@ Línea 222: / Línea 231: @@
 -- ---------------------------------------------------------------------
 validaPorFNC:: Prop -> Bool
-validaPorFNC = undefined
+validaPorFNC f = valida (formaNormalConjuntiva f) f
 -- ---------------------------------------------------------------------
@@ Línea 254: / Línea 284: @@
 --    ==> (no p \/ (q /\ no r))
 -- ---------------------------------------------------------------------
 formaNormalDisyuntiva :: Prop -> Prop
-formaNormalDisyuntiva f = undefined
+formaNormalDisyuntiva f = interiorizaConjuncion (formaNormalNegativa f)
 -- ---------------------------------------------------------------------

@@ Línea 27: / Línea 27: @@
 --    esEquivalente (p \/ q)   (no ((no p) /\ (no q)))   ==>  True
 -- ---------------------------------------------------------------------
 esEquivalente :: Prop -> Prop -> Bool
-esEquivalente f g = undefined
+esEquivalente f g = modelosFormula f == modelosFormula g
 -- ---------------------------------------------------------------------
@@ Línea 45: / Línea 47: @@
 --    ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
 -- ---------------------------------------------------------------------
 eliminaEquivalencias :: Prop -> Prop
-eliminaEquivalencias = undefined
+eliminaEquivalencias (Equi h g) = Conj (Impl h g) (Impl g h)
 -- ---------------------------------------------------------------------
@@ Línea 60: / Línea 73: @@
 -- Nota: Se supone que f no tiene signos de equivalencia.
 -- ---------------------------------------------------------------------
 eliminaImplicaciones :: Prop -> Prop
-eliminaImplicaciones  = undefined
+eliminaImplicaciones (Impl h g) = Disj (Neg h) g
 -- ---------------------------------------------------------------------
@@ Línea 109: / Línea 130: @@
 --    literal (no (p --> q))  ==>  False
 -- ---------------------------------------------------------------------
 literal :: Prop -> Bool
-literal = undefined
+literal (Atom f) = True
 -- ---------------------------------------------------------------------
@@ Línea 127: / Línea 152: @@
 --    complementario (no p)  ==>  p
 -- ---------------------------------------------------------------------
 complementario :: Literal -> Literal
-complementario = undefined
+complementario (Atom f ) = Neg (Atom f)
 -- ---------------------------------------------------------------------
@@ Línea 140: / Línea 168: @@
 --    literalesFórmulaFNN (no p)                ==>  [no p]
 -- ---------------------------------------------------------------------
 literalesFórmulaFNN :: Prop -> [Literal]
-literalesFórmulaFNN = undefined
+literalesFormulaFNN (Disj f g) =
 -- ---------------------------------------------------------------------