Relación 7 - Historial de revisiones

Mansortri en 18:20 12 abr 2015

2015-04-12T18:20:38Z

Jaialbjai en 15:06 12 abr 2015

2015-04-12T15:06:48Z

Fracarmol1 en 12:18 12 abr 2015

2015-04-12T12:18:15Z

Mansortri en 11:09 11 abr 2015

2015-04-11T11:09:06Z

Emimarriv en 14:32 10 abr 2015

2015-04-10T14:32:30Z

Emimarriv en 13:49 10 abr 2015

2015-04-10T13:49:49Z

Emimarriv en 20:27 9 abr 2015

2015-04-09T20:27:15Z

Emimarriv en 17:18 9 abr 2015

2015-04-09T17:18:23Z

Emimarriv en 15:24 9 abr 2015

2015-04-09T15:24:32Z

Emimarriv en 11:31 9 abr 2015

2015-04-09T11:31:57Z

@@ Línea 298: / Línea 298: @@
            ps  = [x |x<-modelosTab fs, f x (modelosTab fs)]
            f x xs = or [ subconjunto y x|y<-xs,x/=y]
 -- ---------------------------------------------------------------------

@@ Línea 32: / Línea 32: @@
 literal (Neg (Atom f)) = True
 literal _ = False
 -- ---------------------------------------------------------------------

@@ Línea 94: / Línea 94: @@
      where quitanegacion (Neg (Neg f)) =f
            quitanegacion f       = f
 -- ---------------------------------------------------------------------
 -- Modelos mediante tableros                                          --
@@ Línea 109: / Línea 124: @@
 conjuntoDeLiterales :: [Prop] -> Bool
 conjuntoDeLiterales = all (literal)
 -- ---------------------------------------------------------------------
@@ Línea 129: / Línea 151: @@
 -- Aunque en general tieneContradiccion1 no es más eficiente, sí lo puede ser para
 -- casos puntuales, p.e. ys = [Neg (Atom "q")] ++ [Atom "s" | x <- [1..100000]]++[Atom "q"]
 -- ---------------------------------------------------------------------
@@ Línea 140: / Línea 163: @@
 expansiónDN :: [Prop] -> Prop -> [[Prop]]
 expansiónDN fs (Neg (Neg f)) = [f:(filter (/=Neg(Neg f)) fs)]
 -- ---------------------------------------------------------------------
 -- Ejercicio 8: Definir la función
@@ Línea 150: / Línea 180: @@
 expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
 expansiónAlfa fs f = [componentes f++(filter (/=f) fs)]
 -- ---------------------------------------------------------------------
@@ Línea 163: / Línea 198: @@
                       where x = head (componentes f)
                             y = last (componentes f)
 -- ---------------------------------------------------------------------
@@ Línea 183: / Línea 224: @@
                                      y= head (filter (alfa) xs)
                                      z= head (filter (beta) xs)
 -- ---------------------------------------------------------------------
@@ Línea 215: / Línea 270: @@
 subconjunto (x:xs) ys |elem x ys = subconjunto xs ys
                        | otherwise=False
 -- ---------------------------------------------------------------------
 -- Ejercicio 13: Definir la función
@@ Línea 246: / Línea 307: @@
 esTeoremaPorTableros :: Prop -> Bool
 esTeoremaPorTableros f = null (modelosTab [no f])
 -- ---------------------------------------------------------------------
 -- Consecuencia por tableros                                          --
@@ Línea 262: / Línea 330: @@
 esDeduciblePorTableros :: [Prop] -> Prop -> Bool
 esDeduciblePorTableros fs f = null (modelosGenerales (no f:fs))
 </source>

@@ Línea 121: / Línea 121: @@
 tieneContradicción fs = or [elem (no p) fs| p<-fs]
 tieneContradicción' fs = or (map (\x-> elem (no x) fs) fs)
 -- ---------------------------------------------------------------------

@@ Línea 253: / Línea 253: @@
 esDeduciblePorTableros :: [Prop] -> Prop -> Bool
-esDeduciblePorTableros fs f = undefined
+esDeduciblePorTableros fs f = null (modelosGenerales (no f:fs))
 </source>

@@ Línea 188: / Línea 188: @@
 modelosTab :: [Prop] -> [[Prop]]
-modelosTab fs = undefined
+modelosTab fs = [x |x<-aux xs, (not.tieneContradicción) x]
 -- ---------------------------------------------------------------------
@@ Línea 200: / Línea 203: @@
 subconjunto :: Eq a => [a] -> [a] -> Bool
-subconjunto xs ys =  [x |x<-aux xs, (not.tieneContradicción) x]
+subconjunto [] _ = True
+subconjunto [x] [y] =False
-    where aux xs |conjuntoDeLiterales xs = [xs]
+subconjunto (x:xs) ys |elem x ys = subconjunto xs ys
-                 | otherwise =map (nub) (concat[(modelosTab x)|x<-sucesores xs])
+                      | otherwise=False
 -- ---------------------------------------------------------------------
 -- Ejercicio 13: Definir la función
@@ Línea 215: / Línea 217: @@
 modelosGenerales :: [Prop] -> [[Prop]]
-modelosGenerales fs = undefined
+modelosGenerales fs =  aux ps (modelosTab fs)
 -- ---------------------------------------------------------------------
@@ Línea 231: / Línea 237: @@
 esTeoremaPorTableros :: Prop -> Bool
-esTeoremaPorTableros f = undefined
+esTeoremaPorTableros f = null (modelosTab [no f])
 -- ---------------------------------------------------------------------
 -- Consecuencia por tableros                                          --

@@ Línea 108: / Línea 108: @@
 conjuntoDeLiterales :: [Prop] -> Bool
-conjuntoDeLiterales fs = undefined
+conjuntoDeLiterales = all (literal)
 -- ---------------------------------------------------------------------
@@ Línea 119: / Línea 119: @@
 tieneContradicción :: [Prop] -> Bool
-tieneContradicción fs = undefined
+tieneContradicción fs = or [elem (no p) fs| p<-fs]
 -- ---------------------------------------------------------------------
@@ Línea 130: / Línea 131: @@
 expansiónDN :: [Prop] -> Prop -> [[Prop]]
-expansiónDN fs f = undefined
+expansiónDN fs (Neg (Neg f)) = [f:(filter (/=Neg(Neg f)) fs)]
 -- ---------------------------------------------------------------------
 -- Ejercicio 8: Definir la función
@@ Línea 141: / Línea 141: @@
 expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
-expansiónAlfa fs f = undefined
+expansiónAlfa fs f = [componentes f++(filter (/=f) fs)]
 -- ---------------------------------------------------------------------
@@ Línea 152: / Línea 152: @@
 expansiónBeta :: [Prop] -> Prop -> [[Prop]]
-expansiónBeta fs f = undefined
+expansiónBeta fs f = [x:(filter(/=f) fs), y:(filter (/=f) fs)]
 -- ---------------------------------------------------------------------
@@ Línea 164: / Línea 166: @@
 sucesores :: [Prop] -> [[Prop]]
-sucesores fs = undefined
+sucesores xs |existeDN xs = expansiónDN xs x
 -- ---------------------------------------------------------------------

@@ Línea 91: / Línea 91: @@
-componentes g = [(no x)|x<-componentes (quitanegacion (no g))]
+componentes g = [quitanegacion (no x)|x<-componentes (quitanegacion (no g))]
      where quitanegacion (Neg (Neg f)) =f
            quitanegacion f       = f

@@ Línea 29: / Línea 29: @@
 literal :: Prop -> Bool
-literal = undefined
+literal (Atom f) = True
 -- ---------------------------------------------------------------------
@@ Línea 45: / Línea 47: @@
 dobleNegación :: Prop -> Bool
-dobleNegación = undefined
+dobleNegación (Neg (Neg f)) = True
 -- ---------------------------------------------------------------------
@@ Línea 54: / Línea 57: @@
 alfa :: Prop -> Bool
-alfa = undefined
+alfa (Conj f g) = True
+alfa (Neg (Disj f g))=True
 -- ---------------------------------------------------------------------
 -- Ejercicio 3: Definir la función
@@ Línea 63: / Línea 69: @@
 beta :: Prop -> Bool
-beta = undefined
+beta (Disj f g) = True
 -- ---------------------------------------------------------------------
@@ Línea 75: / Línea 85: @@
 componentes :: Prop -> [Prop]
-componentes = undefined
+componentes (Conj f g)       = [f,g]
 -- ---------------------------------------------------------------------
 -- Modelos mediante tableros                                          --