Relación 7 - Historial de revisiones

Albromgon en 11:03 17 jun 2016

2016-06-17T11:03:47Z

Albromgon: Otra opción para la función tieneContradiccion

2016-06-17T10:57:34Z

Otra opción para la función tieneContradiccion

Angruigon2: entera

2016-04-26T11:59:14Z

entera

Mjoseh: Página creada con ' -- TablerosSemánticos.hs -- Tableros semánticos proposicionales. -- José A. Alonso Jiménez -- ------------------------------------...'

2016-04-21T11:50:43Z

Página creada con '<source lang = "haskell"> -- TablerosSemánticos.hs -- Tableros semánticos proposicionales. -- José A. Alonso Jiménez <jalonso@us.es> -- ------------------------------------...'

Página nueva

<source lang = "haskell">

-- TablerosSemánticos.hs
-- Tableros semánticos proposicionales.
-- José A. Alonso Jiménez <jalonso@us.es>
-- ---------------------------------------------------------------------

module TablerosSemanticos where

-- ---------------------------------------------------------------------
-- Librerías auxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import Data.List

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

-- ---------------------------------------------------------------------
-- Notación uniforme --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- dobleNegacion :: Prop -> Bool
-- tal que (dobleNegacion f) se verifica si f es una doble negación. Por
-- ejemplo,
-- dobleNegacion (no (no p)) ==> True
-- dobleNegacion (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

dobleNegacion :: Prop -> Bool
dobleNegacion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------

alfa :: Prop -> Bool
alfa = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------

beta :: Prop -> Bool
beta = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- componentes :: Prop -> [Prop]
-- tal que (componentes ) es la lista de las componentes de la fórmula
-- f. Por ejemplo,
-- componentes (p /\ q --> r) ==> [no (p /\ q),r]
-- componentes (no (p /\ q --> r)) ==> [(p /\ q),no r]
-- ---------------------------------------------------------------------

componentes :: Prop -> [Prop]
componentes = undefined

-- ---------------------------------------------------------------------
-- Modelos mediante tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- conjuntoDeLiterales :: [Prop] -> Bool
-- tal que (conjuntoDeLiterales fs) se verifica si fs es un conjunto de
-- literales. Por ejemplo,
-- conjuntoDeLiterales [p --> q, no r, r /\ s, p] ==> False
-- conjuntoDeLiterales [p, no q, r] ==> True
-- ---------------------------------------------------------------------

conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales fs = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- tieneContradiccion :: [Prop] -> Bool
-- tal que (tieneContradiccion fs) se verifica si fs contiene una
-- fórmula y su negación. Por ejemplo,
-- tieneContradiccion [r, p /\ q, s, no(p /\ q)] ==> True
-- ---------------------------------------------------------------------

tieneContradiccion :: [Prop] -> Bool
tieneContradiccion fs = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- expansionDN :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansionDN fs f) es la expansión de fs mediante la doble
-- negación f. Por ejemplo,
-- expansionDN [p, no(no q), r] (no(no q)) ==> [[q,p,r]]
-- ---------------------------------------------------------------------

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- expansionAlfa :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansionAlfa fs f) es la expansión de fs mediante la
-- fórmula alfa f. Por ejemplo,
-- expansionAlfa [q, (p1 /\ p2) , r] (p1 /\ p2) ==> [[p1,p2,q,r]]
-- ---------------------------------------------------------------------

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- expansionBeta :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansionBeta fs f) es la expansión de fs mediante la
-- fórmula beta f. Por ejemplo,
-- expansionBeta [q, (p1 \/ p2) , r] (p1 \/ p2) ==> [[p1,q,r],[p2,q,r]]
-- ---------------------------------------------------------------------

expansionBeta :: [Prop] -> Prop -> [[Prop]]
expansionBeta fs f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- sucesores :: [Prop] -> [[Prop]]
-- tal que (sucesores fs) es la lista de sucesores de fs. Por ejemplo,
-- sucesores [q \/ s, no(no r), p1 /\ p2] => [[r,(q \/ s),(p1 /\ p2)]]
-- sucesores [r,(q \/ s),(p1 /\ p2)] => [[p1,p2,r,(q \/ s)]]
-- sucesores [p1,p2,r,(q \/ s)] => [[q,p1,p2,r],[s,p1,p2,r]]
-- ---------------------------------------------------------------------

sucesores :: [Prop] -> [[Prop]]
sucesores = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- modelosTab :: [Prop] -> [[Prop]]
-- tal que (modelosTab fs) es el conjunto de los modelos de fs
-- calculados mediante el método de tableros semánticos. Por ejemplo,
-- modelosTab [p --> q, no(q --> p)]
-- ==> [[no p,q],[q,no p]]
-- modelosTab [p --> q, no q --> no p]
-- ==> [[q,no p],[no p],[q],[no p,q]]
-- ---------------------------------------------------------------------

modelosTab :: [Prop] -> [[Prop]]
modelosTab = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- subconjunto :: Eq a => [a] -> [a] -> Bool
-- tal que (subconjunto x y) se verifica si x es subconjunto de y. Por
-- ejemplo,
-- subconjunto [1,3] [3,2,1] ==> True
-- subconjunto [1,3,5] [3,2,1] ==> False
-- ---------------------------------------------------------------------

subconjunto :: Eq a => [a] -> [a] -> Bool
subconjunto xs ys = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- modelosGenerales :: [Prop] -> [[Prop]]
-- tal que (modelosGenerales fs) es el conjunto de los modelos generales
-- de fs calculados mediante el método de tableros semánticos. Por
-- ejemplo,
-- modelosGenerales [p --> q, no q --> no p] ==> [[no p],[q]]
-- ---------------------------------------------------------------------

modelosGenerales :: [Prop] -> [[Prop]]
modelosGenerales fs = undefined

-- ---------------------------------------------------------------------
-- Teoremas por tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- esTeoremaPorTableros :: Prop -> Bool
-- tal que (esTeoremaPorTableros f) se verifica si la fórmula f es
-- teorema (mediante tableros semánticos). Por ejemplo,
-- esTeoremaPorTableros (p --> p) ==> True
-- esTeoremaPorTableros (p --> q) ==> False
-- ---------------------------------------------------------------------

esTeoremaPorTableros :: Prop -> Bool
esTeoremaPorTableros f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia por tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esDeduciblePorTableros :: [Prop] -> Prop -> Bool
-- tal que (esDeduciblePorTableros fs f) se verifica si la fórmula f es
-- consecuencia (mediante tableros) del conjunto de fórmulas fs. Por
-- ejemplo,
-- esDeduciblePorTableros [p --> q, q --> r] (p --> r) ==> True
-- esDeduciblePorTableros [p --> q, q --> r] (p <--> r) ==> False
-- ---------------------------------------------------------------------

esDeduciblePorTableros :: [Prop] -> Prop -> Bool
esDeduciblePorTableros fs f = undefined

</source>

@@ Línea 125: / Línea 125: @@
 -- Otra forma usando pliegues
-tieneContradiccion :: [Prop] -> Bool
+tieneContradiccion2 :: [Prop] -> Bool
-tieneContradiccion fs = foldl (\acc x -> if (elem (Neg x) fs) then True else acc) False fs
+tieneContradiccion2 fs = foldl (\acc x -> if (elem (Neg x) fs) then True else acc) False fs
 -- ---------------------------------------------------------------------
 -- Ejercicio 7: Definir la función

@@ Línea 123: / Línea 123: @@
 tieneContradiccion fs = [f | f <- fs, elem (Neg f) fs] /= []
 -- ---------------------------------------------------------------------
 -- Ejercicio 7: Definir la función

@@ Línea 30: / Línea 30: @@
 literal :: Prop -> Bool
-literal = undefined
+literal  (Atom f)      = True
 -- ---------------------------------------------------------------------
@@ Línea 46: / Línea 48: @@
 dobleNegacion :: Prop -> Bool
-dobleNegacion = undefined
+dobleNegacion (Neg (Neg _)) = True
 -- ---------------------------------------------------------------------
@@ Línea 55: / Línea 58: @@
 alfa :: Prop -> Bool
-alfa = undefined
+alfa (Conj _ _)       = True
 -- ---------------------------------------------------------------------
@@ Línea 64: / Línea 70: @@
 beta :: Prop -> Bool
-beta = undefined
+beta (Disj _ _)       = True
 -- ---------------------------------------------------------------------
@@ Línea 76: / Línea 87: @@
 componentes :: Prop -> [Prop]
-componentes = undefined
+componentes (Neg (Neg f))    = [f]
+componentes (Conj f g)       = [f, g]
 -- ---------------------------------------------------------------------
 -- Modelos mediante tableros                                          --
@@ Línea 92: / Línea 110: @@
 conjuntoDeLiterales :: [Prop] -> Bool
-conjuntoDeLiterales fs = undefined
+conjuntoDeLiterales fs = and [literal f | f <- fs]
 -- ---------------------------------------------------------------------
@@ Línea 103: / Línea 121: @@
 tieneContradiccion :: [Prop] -> Bool
-tieneContradiccion fs = undefined
+tieneContradiccion fs = [f | f <- fs, elem (Neg f) fs] /= []
 -- ---------------------------------------------------------------------
@@ Línea 114: / Línea 132: @@
 expansionDN :: [Prop] -> Prop -> [[Prop]]
-expansionDN fs f = undefined
+expansionDN fs f = [(componentes f) `union` (delete f fs)]
 -- ---------------------------------------------------------------------
@@ Línea 125: / Línea 143: @@
 expansionAlfa :: [Prop] -> Prop -> [[Prop]]
-expansionAlfa fs f = undefined
+expansionAlfa fs f = [(componentes f) `union` (delete f fs)]
 -- ---------------------------------------------------------------------
@@ Línea 136: / Línea 154: @@
 expansionBeta :: [Prop] -> Prop -> [[Prop]]
-expansionBeta fs f = undefined
+expansionBeta fs f = [[g] `union` (delete f fs) | g <- componentes f]
 -- ---------------------------------------------------------------------
@@ Línea 148: / Línea 167: @@
 sucesores :: [Prop] -> [[Prop]]
-sucesores = undefined
+sucesores  fs
+    | doblesNegación /= []  = expansiónDN   fs (head doblesNegación)
 -- ---------------------------------------------------------------------
 -- Ejercicio 11: Definir la función
@@ Línea 162: / Línea 186: @@
 modelosTab :: [Prop] -> [[Prop]]
-modelosTab = undefined
+modelosTab  fs
 -- ---------------------------------------------------------------------
@@ Línea 174: / Línea 202: @@
 subconjunto :: Eq a => [a] -> [a] -> Bool
-subconjunto xs ys = undefined
+subconjunto xs ys = and [elem x ys | x <- xs]
 -- ---------------------------------------------------------------------
@@ Línea 186: / Línea 214: @@
 modelosGenerales :: [Prop] -> [[Prop]]
-modelosGenerales fs = undefined
+modelosGenerales fs = [gs | gs <- modelos, [hs | hs <- delete gs modelos, subconjunto hs gs] == []]
 -- ---------------------------------------------------------------------
@@ Línea 202: / Línea 231: @@
 esTeoremaPorTableros :: Prop -> Bool
-esTeoremaPorTableros f = undefined
+esTeoremaPorTableros f = modelosTab [Neg f] == []
 -- ---------------------------------------------------------------------
 -- Consecuencia por tableros                                          --
@@ Línea 219: / Línea 247: @@
 esDeduciblePorTableros :: [Prop] -> Prop -> Bool
-esDeduciblePorTableros fs f = undefined
+esDeduciblePorTableros fs f = modelosTab ((Neg f):fs) == []
 </source>