Mjoseh en 11:48 21 abr 2016

2016-04-21T11:48:21Z

Mjoseh en 10:41 8 mar 2016

2016-03-08T10:41:18Z

Mjoseh: Página creada con ' -- SintaxisSemanticaProp.hs -- Lógica proposicional: Sintaxis y semántica -- --------------------------------------------------------------------- mod...'

2016-03-08T10:40:51Z

Página creada con '<sourca lang="haskell"> -- SintaxisSemanticaProp.hs -- Lógica proposicional: Sintaxis y semántica -- --------------------------------------------------------------------- mod...'

Página nueva

<sourca lang="haskell">
-- SintaxisSemanticaProp.hs
-- Lógica proposicional: Sintaxis y semántica
-- ---------------------------------------------------------------------

module SintaxisSemantica where

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

import Data.List

-- ---------------------------------------------------------------------
-- Gramática de fórmulas prosicionales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir los siguientes tipos de datos:
-- * SímboloProposicional para representar los símbolos de proposiciones
-- * Prop para representar las fórmulas proposicionales usando los
-- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas
-- atómicas, negaciones, conjunciones, implicaciones y equivalencias,
-- respectivamente.
-- ---------------------------------------------------------------------

type SímboloProposicional = String

data Prop = Atom SímboloProposicional
| Neg Prop
| Conj Prop Prop
| Disj Prop Prop
| Impl Prop Prop
| Equi Prop Prop
deriving (Eq,Ord)

instance Show Prop where
show (Atom p) = p
show (Neg p) = "no " ++ show p
show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir las siguientes fórmulas proposicionales
-- atómicas: p, p1, p2, q, r, s, t y u.
-- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop
p = Atom "p"
p1 = Atom "p1"
p2 = Atom "p2"
q = Atom "q"
r = Atom "r"
s = Atom "s"
t = Atom "t"
u = Atom "u"

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- no :: Prop -> Prop
-- tal que (no f) es la negación de f.
-- ---------------------------------------------------------------------

no :: Prop -> Prop
no = Neg

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir los siguientes operadores
-- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
-- tales que
-- f /\ g es la conjunción de f y g
-- f \/ g es la disyunción de f y g
-- f --> g es la implicación de f a g
-- f <--> g es la equivalencia entre f y g
-- ---------------------------------------------------------------------

infixr 5 \/
infixr 4 /\
infixr 3 -->
infixr 2 <-->
(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
(/\) = Conj
(\/) = Disj
(-->) = Impl
(<-->) = Equi

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una fórmula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- símbolosPropFórm :: Prop -> [Prop]
-- tal que (símbolosPropFórm f) es el conjunto formado por todos los
-- símbolos proposicionales que aparecen en f. Por ejemplo,
-- símbolosPropFórm (p /\ q --> p) ==> [p,q]
-- ---------------------------------------------------------------------

símbolosPropFórm :: Prop -> [Prop]
símbolosPropFórm (Atom f) = [(Atom f)]
símbolosPropFórm (Neg f) = símbolosPropFórm f
símbolosPropFórm (Conj f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Disj f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Impl f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Equi f g) = símbolosPropFórm f `union` símbolosPropFórm g

-- ---------------------------------------------------------------------
-- Interpretaciones --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir el tipo de datos Interpretación para
-- representar las interpretaciones como listas de fórmulas atómicas.
-- ---------------------------------------------------------------------

type Interpretación = [Prop]

-- ---------------------------------------------------------------------
-- Significado de una fórmula en una interpretación --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- significado :: Prop -> Interpretación -> Bool
-- tal que (significado f i) es el significado de f en i. Por ejemplo,
-- significado ((p \/ q) /\ ((no q) \/ r)) [r] ==> False
-- significado ((p \/ q) /\ ((no q) \/ r)) [p,r] ==> True
-- ---------------------------------------------------------------------

significado :: Prop -> Interpretación -> Bool
significado (Atom f) i = (Atom f) `elem` i
significado (Neg f) i = not (significado f i)
significado (Conj f g) i = (significado f i) && (significado g i)
significado (Disj f g) i = (significado f i) || (significado g i)
significado (Impl f g) i = significado (Disj (Neg f) g) i
significado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i

-- ---------------------------------------------------------------------
-- Interpretaciones de una fórmula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- subconjuntos :: [a] -> [[a]]
-- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por
-- ejmplo,
-- subconjuntos "abc" ==> ["abc","ab","ac","a","bc","b","c",""]
-- ---------------------------------------------------------------------

subconjuntos :: [a] -> [[a]]
subconjuntos [] = [[]]
subconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss
where xss = subconjuntos xs

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesFórm :: Prop -> [Interpretación]
-- tal que (interpretacionesFórm f) es la lista de todas las
-- interpretaciones de f. Por ejemplo,
-- interpretacionesFórm (p /\ q --> p) ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

interpretacionesFórm :: Prop -> [Interpretación]
interpretacionesFórm f = subconjuntos (símbolosPropFórm f)

-- ---------------------------------------------------------------------
-- Modelos de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloFórmula :: Interpretación -> Prop -> Bool
-- tal que (esModeloFórmula i f) se verifica si i es un modelo de f. Por
-- ejemplo,
-- esModeloFórmula [r] ((p \/ q) /\ ((no q) \/ r)) ==> False
-- esModeloFórmula [p,r] ((p \/ q) /\ ((no q) \/ r)) ==> True
-- ---------------------------------------------------------------------

esModeloFórmula :: Interpretación -> Prop -> Bool
esModeloFórmula i f = significado f i

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- modelosFórmula :: Prop -> [Interpretación]
-- tal que (modelosFórmula f) es la lista de todas las interpretaciones
-- de f que son modelo de F. Por ejemplo,
-- modelosFórmula ((p \/ q) /\ ((no q) \/ r))
-- ==> [[p,q,r],[p,r],[p],[q,r]]
-- ---------------------------------------------------------------------

modelosFórmula :: Prop -> [Interpretación]
modelosFórmula f =
[i | i <- interpretacionesFórm f,
esModeloFórmula i f]

-- ---------------------------------------------------------------------
-- Fórmulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

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

esVálida :: Prop -> Bool
esVálida f =
modelosFórmula f == interpretacionesFórm f

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esInsatisfacible :: Prop -> Bool
-- tal que (esInsatisfacible f) se verifica si f es insatisfacible. Por
-- ejemplo,
-- esInsatisfacible (p /\ (no p)) ==> True
-- esInsatisfacible ((p --> q) /\ (q --> r)) ==> False
-- ---------------------------------------------------------------------

esInsatisfacible :: Prop -> Bool
esInsatisfacible f =
modelosFórmula f == []

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

esSatisfacible :: Prop -> Bool
esSatisfacible f =
modelosFórmula f /= []

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- uniónGeneral :: Eq a => [[a]] -> [a]
-- tal que (uniónGeneral x) es la unión de los conjuntos de la lista de
-- conjuntos x. Por ejemplo,
-- uniónGeneral [] ==> []
-- uniónGeneral [[1]] ==> [1]
-- uniónGeneral [[1],[1,2],[2,3]] ==> [1,2,3]
-- ---------------------------------------------------------------------

uniónGeneral :: Eq a => [[a]] -> [a]
uniónGeneral [] = []
uniónGeneral (xs:xss) = xs `union` uniónGeneral xss

uniónG :: Eq a => [[a]] -> [a]
uniónG = foldl union []

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- símbolosPropConj :: [Prop] -> [Prop]
-- tal que (símbolosPropConj s) es el conjunto de los símbolos
-- proposiciones de s. Por ejemplo,
-- símbolosPropConj [p /\ q --> r, p --> s] ==> [p,q,r,s]
-- ---------------------------------------------------------------------

símbolosPropConj :: [Prop] -> [Prop]
símbolosPropConj s
= uniónGeneral [símbolosPropFórm f | f <- s]

símbolosPropConj2 :: [Prop] -> [Prop]
símbolosPropConj2 = uniónG . map símbolosPropFórm

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- interpretacionesConjunto :: [Prop] -> [Interpretación]
-- tal que (interpretacionesConjunto s) es la lista de las
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjunto [p --> q, q --> r]
-- ==> [[p,q,r],[p,q],[p,r],[p],[q,r],[q],[r],[]]
-- ---------------------------------------------------------------------

interpretacionesConjunto :: [Prop] -> [Interpretación]
interpretacionesConjunto s =
subconjuntos (símbolosPropConj s)

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esModeloConjunto :: Interpretación -> [Prop] -> Bool
-- tal que (esModeloConjunto i s) se verifica si i es modelo de s. Por
-- ejemplo,
-- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), q --> r]
-- ==> True
-- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), r --> q]
-- ==> False
-- ---------------------------------------------------------------------

esModeloConjunto :: Interpretación -> [Prop] -> Bool
esModeloConjunto i s =
and [esModeloFórmula i f | f <- s]

esModeloConjunto2 :: Interpretación -> [Prop] -> Bool
esModeloConjunto2 i s = all (esModeloFórmula i) s

-- --------------------g-------------------------------------------------
-- Ejercicio 19: Definir la función
-- modelosConjunto :: [Prop] -> [Interpretación]
-- tal que (modelosConjunto s) es la lista de modelos del conjunto
-- s. Por ejemplo,
-- modelosConjunto [(p \/ q) /\ ((no q) \/ r), q --> r]
-- ==> [[p,q,r],[p,r],[p],[q,r]]
-- modelosConjunto [(p \/ q) /\ ((no q) \/ r), r --> q]
-- ==> [[p,q,r],[p],[q,r]]
-- ---------------------------------------------------------------------

modelosConjunto :: [Prop] -> [Interpretación]
modelosConjunto s =
[i | i <- interpretacionesConjunto s,
esModeloConjunto i s]

-- ---------------------------------------------------------------------
-- Conjuntos consistentes e inconsistentes de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConsistente :: [Prop] -> Bool
-- tal que (esConsistente s) se verifica si s es consistente. Por
-- ejemplo,
-- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r]
-- ==> True
-- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r]
-- ==> False
-- ---------------------------------------------------------------------

esConsistente :: [Prop] -> Bool
esConsistente s =
modelosConjunto s /= []

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esInconsistente :: [Prop] -> Bool
-- tal que (esInconsistente s) se verifica si s es inconsistente. Por
-- ejemplo,
-- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r]
-- ==> False
-- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r]
-- ==> True
-- ---------------------------------------------------------------------

esInconsistente :: [Prop] -> Bool
esInconsistente s =
modelosConjunto s == []

-- ---------------------------------------------------------------------
-- Consecuencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuencia :: [Prop] -> Prop -> Bool
-- tal que (esConsecuencia s f) se verifica si f es consecuencia de
-- s. Por ejemplo,
-- esConsecuencia [p --> q, q --> r] (p --> r) ==> True
-- esConsecuencia [p] (p /\ q) ==> False
-- ---------------------------------------------------------------------

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f =
null [i | i <- interpretacionesConjunto (f:s),
esModeloConjunto i s,
not (esModeloFórmula i f)]

esConsecuencia2 :: [Prop] -> Prop -> Bool
esConsecuencia2 s f =
and [esModeloFórmula i f | i <- interpretacionesConjunto (f:s),
esModeloConjunto i s]

</source>

@@ Línea 1: / Línea 1: @@
-<sourca lang="haskell">
+<source lang="haskell">
 -- SintaxisSemanticaProp.hs
 -- Lógica proposicional: Sintaxis y semántica

R2a sol - Historial de revisiones

Mjoseh en 11:48 21 abr 2016

Mjoseh en 10:41 8 mar 2016

Mjoseh: Página creada con ' -- SintaxisSemanticaProp.hs -- Lógica proposicional: Sintaxis y semántica -- --------------------------------------------------------------------- mod...'