Lógica matemática y fundamentos (2014-15) - Contribuciones del usuario [es]

Relación 12

2015-05-11T14:49:07Z

Luipalbla:

<source lang = "haskell">
-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-- 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]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = nub (filter (/= l )(filter
(/= (complementario l)) (c1 ++ c2)))

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- 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]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = [resolvente c1 c2 l | l <- c1,
elem (complementario l) c2 ]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = aux c s
where aux x [] = []
aux x (y:ys) = resolventes x y ++
aux x ys

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautología [p, q, no p] ==> True
-- esTautología [p, q, no r] ==> False
-- esTautología [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esTautología :: Cláusula -> Bool
esTautología c = or [elem (complementario x) c | x <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologías [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = [ x | x <- s, not( esTautologia x)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolución [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolución [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

-- Luis Palma, no hay acentos

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s

-- La solución anterior no es correcta ya que esta resuelta por clausula,
-- no por resolución, la propuesta en clase es:

esInconsistentePorResolucion1 :: [Clausula] -> Bool
esInconsistentePorResolucion1 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
-- esVálidaPorResolución :: Prop -> Bool
-- tal que (esVálidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo,
-- esVálidaPorResolución (p --> p) ==> True
-- esVálidaPorResolución ((p --> q) \/ (q --> p)) ==> True
-- esVálidaPorResolución (p --> q) ==> False
-- ---------------------------------------------------------------------

--Luis Palma

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = esInconsistentePorResolucion (clausulasConjunto ((Neg f):s))

</source>

Relación 12

2015-05-11T14:48:29Z

Luipalbla:

<source lang = "haskell">
-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-- 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]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = nub (filter (/= l )(filter
(/= (complementario l)) (c1 ++ c2)))

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- 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]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = [resolvente c1 c2 l | l <- c1,
elem (complementario l) c2 ]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = aux c s
where aux x [] = []
aux x (y:ys) = resolventes x y ++
aux x ys

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautología [p, q, no p] ==> True
-- esTautología [p, q, no r] ==> False
-- esTautología [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esTautología :: Cláusula -> Bool
esTautología c = or [elem (complementario x) c | x <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologías [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = [ x | x <- s, not( esTautologia x)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolución [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolución [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

-- Luis Palma, no hay acentos

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s

-- La solución anterior no es correcta ya que esta resuelta por clausula
-- no por resolución, la propuesta en clase es:

esInconsistentePorResolucion1 :: [Clausula] -> Bool
esInconsistentePorResolucion1 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
-- esVálidaPorResolución :: Prop -> Bool
-- tal que (esVálidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo,
-- esVálidaPorResolución (p --> p) ==> True
-- esVálidaPorResolución ((p --> q) \/ (q --> p)) ==> True
-- esVálidaPorResolución (p --> q) ==> False
-- ---------------------------------------------------------------------

--Luis Palma

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = esInconsistentePorResolucion (clausulasConjunto ((Neg f):s))

</source>

Relación 12

2015-05-09T15:46:14Z

Luipalbla:

<source lang = "haskell">
-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-- 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]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = nub (filter (/= l )(filter
(/= (complementario l)) (c1 ++ c2)))

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- 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]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = [resolvente c1 c2 l | l <- c1,
elem (complementario l) c2 ]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = aux c s
where aux x [] = []
aux x (y:ys) = resolventes x y ++
aux x ys

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautología [p, q, no p] ==> True
-- esTautología [p, q, no r] ==> False
-- esTautología [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esTautología :: Cláusula -> Bool
esTautología c = or [elem (complementario x) c | x <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologías [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = [ x | x <- s, not( esTautologia x)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolución [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolución [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

-- Luis Palma, no hay acentos

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s

-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------

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

--Luis Palma

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = esInconsistentePorResolucion (clausulasConjunto ((Neg f):s))

</source>

Relación 11

2015-05-09T15:39:11Z

Luipalbla:

<source lang = "haskell">
-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------

module Clausulas where

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

import SintaxisSemantica
import FormasNormales
import Data.List

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Cláusula como una lista de
-- literales.
-- ---------------------------------------------------------------------

type Cláusula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- cláusula :: Prop -> Cláusula
-- tal que (cláusula f) es la cláusula de la fórmula-clausal f. Por
-- ejemplo,
-- cláusula p ==> [p]
-- cláusula (no p) ==> [no p]
-- cláusula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusula :: Prop -> Cláusula
cláusula f = literalesFormulaFNN f

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- cláusulasFNC :: Prop -> [Cláusula]
-- tal que (cláusulasFNC f) es el conjunto de cláusulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- cláusulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- cláusulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------

-- Luis Palma

cláusulasFNC :: Prop -> [Cláusula]
clausulasFNC (Conj f g) = (clausulasFNC f) ++ (clausulasFNC g)
clausulasFNC (Disj f g) = map sort [clausula f ++ clausula g]
clausulasFNC f = [clausula f]

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- cláusulas :: Prop -> [Cláusula]
-- tal que (cláusulas f) es un conjunto de cláusulas equivalente a
-- f. Por ejemplo,
-- cláusulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- cláusulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- cláusulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusulas :: Prop -> [Cláusula]
cláusulas f = clausulasFNC (formaNormalConjuntiva f)

-- ---------------------------------------------------------------------
-- Cláusulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- cláusulasConjunto :: [Prop] -> [Cláusula]
-- tal que (cláusulasConjunto s) es un conjunto de cláusulas equivalente
-- a s. Por ejemplo,
-- cláusulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- cláusulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusulasConjunto :: [Prop] -> [Cláusula]
cláusulasConjunto s = nub (aux s)
where aux [] = []
aux (x:xs) = clausulas x ++ aux xs

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- símbolosProposicionalesCláusula :: Cláusula -> [Prop]
-- tal que (símbolosProposicionalesCláusula c) es el conjunto de los
-- símbolos proposicionales de c. Por ejemplo,
-- símbolosProposicionalesCláusula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

símbolosProposicionalesCláusula :: Cláusula -> [Prop]
símbolosProposicionalesCláusula f = simbolosPropConj f

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
-- tal que (símbolosProposicionalesConjuntoCláusula s) es el conjunto de los
-- símbolos proposicionales de s. Por ejemplo,
-- símbolosProposicionalesConjuntoCláusula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
símbolosProposicionalesConjuntoCláusula s = nub (aux s)
where aux [] = []
aux (x:xs) = simbolosPropConj x ++ aux x

-- ---------------------------------------------------------------------
-- Interpretaciones de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesCláusula :: Cláusula -> [Interpretación]
-- tal que (interpretacionesCláusula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesCláusula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesCláusula [] ==> [[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

interpretacionesCláusula :: Cláusula -> [Interpretación]
interpretacionesCláusula c = subconjuntos
(simbolosProposicionalesClausula c)

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
-- tal que (interpretacionesConjuntoCláusula s) es el conjunto de
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjuntoCláusula [[p, no q],[no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- interpretacionesConjuntoCláusula []
-- ==> [[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
interpretacionesConjuntoCláusula c = nub (aux c)
where aux [] = [[]]
aux (x:xs) =
interpretacionesClausula x ++ aux xs

-- ---------------------------------------------------------------------
-- Modelos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretación -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------

-- Luis Palma

esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral xs (Atom x) = or [y == (Atom x) | y <- xs]
esModeloLiteral xs x = and [not(y == (interiorizaNegacion (Neg x))) | y <- xs]

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloCláusula :: Interpretación -> Cláusula -> Bool
-- tal que (esModeloCláusula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloCláusula [p,r] [p, q] ==> True
-- esModeloCláusula [r] [p, no q] ==> True
-- esModeloCláusula [q,r] [p, no q] ==> False
-- esModeloCláusula [q,r] [] ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esModeloCláusula :: Interpretación -> Cláusula -> Bool
esModeloCláusula i c = or [esModeloLiteral i t | t <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- modelosCláusula :: Cláusula -> [Interpretación]
-- tal que (modelosCláusula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosCláusula [no p, q] ==> [[p,q],[q],[]]
-- modelosCláusula [no p, p] ==> [[p],[]]
-- modelosCláusula [] ==> []
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

modelosCláusula :: Cláusula -> [Interpretación]
modelosCláusula c = aux (interpretacionesClausula c)
where aux [] = []
aux (x:xs) | esModeloClausula x c = x : aux xs
| otherwise = aux xs

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
-- tal que (esModeloConjuntoCláusulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoCláusulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoCláusulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoCláusulas [p] [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
esModeloConjuntoCláusulas i s = aux i s
where aux i [] = True
aux i (x:xs) = esModeloClausula i x && aux i xs

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
-- tal que (modelosConjuntoCláusulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoCláusulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoCláusulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoCláusulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
modelosConjuntoCláusulas s = aux1 (aux2 s)
where aux1 [] = []
aux1 (x:xs) | not (elem (reverse x) xs) = x : aux1 xs
| otherwise = aux1 xs

aux2 s = aux2 (interpretacionesConjuntoClausula s)
where aux2 [] = []
aux2 (x:xs) | esModeloConjuntoClausulas x s = x : aux2 xs
| otherwise = aux2 xs

-- ---------------------------------------------------------------------
-- Cláusulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esCláusulaVálida :: Cláusula -> Bool
-- tal que (esCláusulaVálida c) se verifica si la cláusula c es
-- válida. Por ejemplo,
-- esCláusulaVálida [p, q, no p] ==> True
-- esCláusulaVálida [p, q, no r] ==> False
-- esCláusulaVálida [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaVálida :: Cláusula -> Bool
esCláusulaVálida c = modelosClausula c == interpretacionesClausula c

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- esCláusulaInsatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaInsatisfacible c) se verifica si la cláusula c es
-- insatisfacible. Por ejemplo,
-- esCláusulaInsatisfacible [p, q, no p] ==> False
-- esCláusulaInsatisfacible [p, q, no r] ==> False
-- esCláusulaInsatisfacible [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaInsatisfacible :: Cláusula -> Bool
esCláusulaInsatisfacible c = modelosClausula c == []

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esCláusulaSatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaSatisfacible c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo,
-- esCláusulaSatisfacible [p, q, no p] ==> True
-- esCláusulaSatisfacible [p, q, no r] ==> True
-- esCláusulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaSatisfacible :: Cláusula -> Bool
esCláusulaSatisfacible c = modelosClausula c /= []

-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoVálidoDeCláusulas s) se verifica si el conjunto de
-- cláusulas s es válido. Por ejemplo,
-- esConjuntoVálidoDeCláusulas [[no p, q], [no q, p]] ==> False
-- esConjuntoVálidoDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoVálidoDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
esConjuntoVálidoDeCláusulas s = aux s
where aux [] = True
aux (x:xs) = esClausulaValida x &&
aux xs

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoConsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeCláusulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoConsistenteDeCláusulas s = modelosConjuntoClausulas s /= []

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoInconsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeCláusulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeCláusulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoInconsistenteDeCláusulas s = modelosConjuntoClausulas s == []

-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esVálidaPorCláusulas :: Prop -> Bool
-- tal que (esVálidaPorCláusulas f) se verifica si el conjunto de
-- cláusulas de f es válido. Por ejemplo,
-- esVálidaPorCláusulas (p --> q) ==> False
-- esVálidaPorCláusulas (p --> p) ==> True
-- esVálidaPorCláusulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esVálidaPorCláusulas :: Prop -> Bool
esVálidaPorCláusulas f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
-- tal que (esConsecuenciaEntreCláusulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreCláusulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreCláusulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
esConsecuenciaEntreCláusulas s1 s2 = and [esModeloConjuntoCláusulas x s2 | x <- (modelosConjuntoCláusulas s1)]

-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorCláusulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorCláusulas s f) se verifica si las cláusulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorCláusulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorCláusulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorCláusulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorCláusulas s f = and [elem x (concat (cláusulasConjunto s)) | x <- (concat (cláusulas f))]

</source>

Relación 11

2015-05-07T17:59:48Z

Luipalbla:

<source lang = "haskell">
-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------

module Clausulas where

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

import SintaxisSemantica
import FormasNormales
import Data.List

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Cláusula como una lista de
-- literales.
-- ---------------------------------------------------------------------

type Cláusula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- cláusula :: Prop -> Cláusula
-- tal que (cláusula f) es la cláusula de la fórmula-clausal f. Por
-- ejemplo,
-- cláusula p ==> [p]
-- cláusula (no p) ==> [no p]
-- cláusula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusula :: Prop -> Cláusula
cláusula f = literalesFormulaFNN f

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- cláusulasFNC :: Prop -> [Cláusula]
-- tal que (cláusulasFNC f) es el conjunto de cláusulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- cláusulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- cláusulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------

-- Luis Palma

cláusulasFNC :: Prop -> [Cláusula]
clausulasFNC (Conj f g) = (clausulasFNC f) ++ (clausulasFNC g)
clausulasFNC (Disj f g) = map sort [clausula f ++ clausula g]
clausulasFNC f = [clausula f]

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- cláusulas :: Prop -> [Cláusula]
-- tal que (cláusulas f) es un conjunto de cláusulas equivalente a
-- f. Por ejemplo,
-- cláusulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- cláusulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- cláusulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusulas :: Prop -> [Cláusula]
cláusulas f = clausulasFNC (formaNormalConjuntiva f)

-- ---------------------------------------------------------------------
-- Cláusulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- cláusulasConjunto :: [Prop] -> [Cláusula]
-- tal que (cláusulasConjunto s) es un conjunto de cláusulas equivalente
-- a s. Por ejemplo,
-- cláusulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- cláusulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

cláusulasConjunto :: [Prop] -> [Cláusula]
cláusulasConjunto s = nub (aux s)
where aux [] = []
aux (x:xs) = clausulas x ++ aux xs

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- símbolosProposicionalesCláusula :: Cláusula -> [Prop]
-- tal que (símbolosProposicionalesCláusula c) es el conjunto de los
-- símbolos proposicionales de c. Por ejemplo,
-- símbolosProposicionalesCláusula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

símbolosProposicionalesCláusula :: Cláusula -> [Prop]
símbolosProposicionalesCláusula f = simbolosPropConj f

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
-- tal que (símbolosProposicionalesConjuntoCláusula s) es el conjunto de los
-- símbolos proposicionales de s. Por ejemplo,
-- símbolosProposicionalesConjuntoCláusula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
símbolosProposicionalesConjuntoCláusula s = nub (aux s)
where aux [] = []
aux (x:xs) = simbolosPropConj x ++ aux x

-- ---------------------------------------------------------------------
-- Interpretaciones de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesCláusula :: Cláusula -> [Interpretación]
-- tal que (interpretacionesCláusula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesCláusula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesCláusula [] ==> [[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

interpretacionesCláusula :: Cláusula -> [Interpretación]
interpretacionesCláusula c = subconjuntos
(simbolosProposicionalesClausula c)

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
-- tal que (interpretacionesConjuntoCláusula s) es el conjunto de
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjuntoCláusula [[p, no q],[no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- interpretacionesConjuntoCláusula []
-- ==> [[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
interpretacionesConjuntoCláusula c = nub (aux c)
where aux [] = [[]]
aux (x:xs) =
interpretacionesClausula x ++ aux xs

-- ---------------------------------------------------------------------
-- Modelos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretación -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------

-- Luis Palma

esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral xs (Atom x) = or [y == (Atom x) | y <- xs]
esModeloLiteral xs x = and [not(y == (interiorizaNegacion (Neg x))) | y <- xs]

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloCláusula :: Interpretación -> Cláusula -> Bool
-- tal que (esModeloCláusula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloCláusula [p,r] [p, q] ==> True
-- esModeloCláusula [r] [p, no q] ==> True
-- esModeloCláusula [q,r] [p, no q] ==> False
-- esModeloCláusula [q,r] [] ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esModeloCláusula :: Interpretación -> Cláusula -> Bool
esModeloClausula i c = or [esModeloLiteral i t | t <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- modelosCláusula :: Cláusula -> [Interpretación]
-- tal que (modelosCláusula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosCláusula [no p, q] ==> [[p,q],[q],[]]
-- modelosCláusula [no p, p] ==> [[p],[]]
-- modelosCláusula [] ==> []
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

modelosCláusula :: Cláusula -> [Interpretación]
modelosCláusula c = aux (interpretacionesClausula c)
where aux [] = []
aux (x:xs) | esModeloClausula x c = x : aux xs
| otherwise = aux xs

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
-- tal que (esModeloConjuntoCláusulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoCláusulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoCláusulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoCláusulas [p] [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
esModeloConjuntoCláusulas i s = aux i s
where aux i [] = True
aux i (x:xs) = esModeloClausula i x && aux i xs

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
-- tal que (modelosConjuntoCláusulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoCláusulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoCláusulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoCláusulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
modelosConjuntoCláusulas s = aux1 (aux2 s)
where aux1 [] = []
aux1 (x:xs) | not (elem (reverse x) xs) = x : aux1 xs
| otherwise = aux1 xs

aux2 s = aux2 (interpretacionesConjuntoClausula s)
where aux2 [] = []
aux2 (x:xs) | esModeloConjuntoClausulas x s = x : aux2 xs
| otherwise = aux2 xs

-- ---------------------------------------------------------------------
-- Cláusulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esCláusulaVálida :: Cláusula -> Bool
-- tal que (esCláusulaVálida c) se verifica si la cláusula c es
-- válida. Por ejemplo,
-- esCláusulaVálida [p, q, no p] ==> True
-- esCláusulaVálida [p, q, no r] ==> False
-- esCláusulaVálida [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaVálida :: Cláusula -> Bool
esCláusulaVálida c = modelosClausula c == interpretacionesClausula c

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- esCláusulaInsatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaInsatisfacible c) se verifica si la cláusula c es
-- insatisfacible. Por ejemplo,
-- esCláusulaInsatisfacible [p, q, no p] ==> False
-- esCláusulaInsatisfacible [p, q, no r] ==> False
-- esCláusulaInsatisfacible [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaInsatisfacible :: Cláusula -> Bool
esCláusulaInsatisfacible c = modelosClausula c == []

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esCláusulaSatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaSatisfacible c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo,
-- esCláusulaSatisfacible [p, q, no p] ==> True
-- esCláusulaSatisfacible [p, q, no r] ==> True
-- esCláusulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esCláusulaSatisfacible :: Cláusula -> Bool
esCláusulaSatisfacible c = modelosClausula c /= []

-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoVálidoDeCláusulas s) se verifica si el conjunto de
-- cláusulas s es válido. Por ejemplo,
-- esConjuntoVálidoDeCláusulas [[no p, q], [no q, p]] ==> False
-- esConjuntoVálidoDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoVálidoDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
esConjuntoVálidoDeCláusulas s = aux s
where aux [] = True
aux (x:xs) = esClausulaValida x &&
aux xs

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoConsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeCláusulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoConsistenteDeCláusulas s = modelosConjuntoClausulas s /= []

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoInconsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeCláusulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeCláusulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoInconsistenteDeCláusulas s = modelosConjuntoClausulas s == []

-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esVálidaPorCláusulas :: Prop -> Bool
-- tal que (esVálidaPorCláusulas f) se verifica si el conjunto de
-- cláusulas de f es válido. Por ejemplo,
-- esVálidaPorCláusulas (p --> q) ==> False
-- esVálidaPorCláusulas (p --> p) ==> True
-- esVálidaPorCláusulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esVálidaPorCláusulas :: Prop -> Bool
esVálidaPorCláusulas f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
-- tal que (esConsecuenciaEntreCláusulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreCláusulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreCláusulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
esConsecuenciaEntreClausulas s1 s2 = and [esModeloConjuntoClausulas x s2 | x <- (modelosConjuntoClausulas s1)]

-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorCláusulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorCláusulas s f) se verifica si las cláusulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorCláusulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorCláusulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorCláusulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas s f = and [elem x (concat (clausulasConjunto s)) | x <- (concat (clausulas f))]

</source>

Relación 2a

2015-03-08T19:15:26Z

Luipalbla:

<source lang = "haskell">
-- SintaxisSemanticaProp.hs
-- Lógica proposicional: Sintaxis y semántica
-- José A. Alonso Jiménez <jalonso@us.es>
-- ---------------------------------------------------------------------

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

simbolosPropForm :: Prop -> [Prop]
simbolosPropForm (Atom p) = [Atom p]
simbolosPropForm (Neg p) = simbolosPropForm p
simbolosPropForm (Conj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Disj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Impl p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Equi p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))

-- Luis Curquejo

-- Comentario: La definición se puede mejorar usando la función union.

-- ---------------------------------------------------------------------
-- 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 -> Interpretacion -> Bool
significado (Atom f) xs | elem (Atom f) xs = True
| otherwise = False
significado (Neg f) xs = not (significado f xs)
significado (Conj f q) xs = (significado f xs) && (significado q xs)
significado (Disj f q) xs = (significado f xs) || (significado q xs)
significado (Impl f q) xs | (significado f xs) == True = significado q xs
| otherwise = True
significado (Equi f q) xs = (significado f xs) == (significado q xs)

--Luis Curquejo

-- Comentario: la definición se puede simplificar.

significado :: Prop -> Interpretacion -> Bool
significado (Atom p) i = elem (Atom p) i
significado (Neg p) i = not (significado p i)
significado (Conj p q) i = (significado p i)&&(significado q i)
significado (Disj p q) i = (significado p i)||(significado q i)
significado (Impl p q) i | significado p i = significado q i
| otherwise = True
significado (Equi p q) i = (significado p i)==(significado q i)

--María Dolores Mateo Ceballos

-- ---------------------------------------------------------------------
-- 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 [a] = [[],[a]]
subconjuntos (x:xs) = [x:ys | ys <- sub] ++ sub
where sub = subconjuntos xs
-- Me acordaba de primero (seguro) Javier Rodríguez Vivas
-- Jaime Alberto

subconjuntos :: [a] -> [[a]]
subconjuntos [] = [[]]
subconjuntos (x:xs) = [x:ys | ys<-subconjuntos xs] ++ 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],[]]
-- ---------------------------------------------------------------------

interpretacionesForm :: Prop -> [Interpretacion]
interpretacionesForm f = subconjuntos (simbolosPropForm f)

--Luis Curquejo

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

esModeloFormula :: Interpretacion -> Prop -> Bool
esModeloFormula i f = significado f i

-- Luis Curquejo
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 <- subconjuntos (símbolosPropFórm f), esModeloFórmula i f]

-- Elisa Mazuelos Jiménez

-- Comentario: la definición se puede simplificar usando interpretacionesForm.

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = [xs|xs<-(interpretacionesForm f), esModeloFormula xs f]

--María Dolores Mateo Ceballos

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = aux (interpretacionesForm f)
where aux [] = []
aux (x:xs) | esModeloFormula x f = x : aux xs
| otherwise = aux xs

-- Francisco Javier Carmona

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

esValida :: Prop -> Bool
esValida f = subconjuntos (simPro f) == modelosFormula f

-- Javier Rodríguez Vivas

-- Comentario: la definición se puede simplificar usando interpretacionesForm.

esValida :: Prop -> Bool
esValida f = modelosFormula f == interpretacionesForm f

-- María Dolores Mateo Ceballos
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = null (modelosFórmula f)
--Emilio Martinez Rivero

esInsatisfacible :: Prop -> Bool
esInsatisfacible f = modelosFormula f == []

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . EsInsatisfacible
--Emilio Martinez Rivero

esSatisfacible :: Prop -> Bool
esSatisfacible f = modelosFormula f /= []

-- Francisco Javier Carmona

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

unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (x:xs) = nub(x++ unionGeneral xs)

--Javier Rodríguez Vivas
-- Francisco Javier Carmona

-- Comentario: La definición se puede mejorar usando la función union.

uniónGeneral :: Eq a => [[a]] -> [a]
uniónGeneral = nub . concat

-- Elisa Mazuelos Jiménez

unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (xs:xss) = union xs (unionGeneral xss)

-- Maria del Carmen Mesa Marquez

-- ---------------------------------------------------------------------
-- 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 [simb x | x<-s]

--Emilio Martinez Rivero

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = nub (aux s)
where aux [] = []
aux (x:xs) = simbolosPropForm x ++
simbolosPropConj xs

-- Francisco Javier Carmona

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = unionGeneral (map simbolosPropForm s)

-- Luis Palma Blanco

-- ---------------------------------------------------------------------
-- 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 = subconjuntos . símbolosPropConj

-- Elisa Mazuelos Jiménez

-- ---------------------------------------------------------------------
-- 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 = elem False xs == False
where xs = [esModeloFormula i f | f<-s]

--Javier Rodriguez Vivas

-- Comentario: la definición se puede mejorar.

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = and [esModeloFormula i f| f<-s]

--María Dolores Mateo Ceballos

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = aux i s
where aux i [] = True
aux i (x:xs) = esModeloFormula i x &&
esModeloConjunto i xs

-- Francisco Javier Carmona

-- Jaime Alberto
esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i [f] = esModeloFormula i f
esModeloConjunto i (x:xs) | esModeloFormula i x = esModeloConjunto i xs
| otherwise = False

-- ---------------------------------------------------------------------
-- 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 = [x|x<-interpretacionesConjunto s, esModeloConjunto x s]
--Emilio Martinez Rivero
-- ---------------------------------------------------------------------
-- 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 = or [esModeloConjunto x s | x <- (modelosConjunto s)]

-- Elisa Mazuelos Jiménez

-- Comentario: La definición se puede mejorar.

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . esConsistente

-- Elisa Mazuelos Jiménez

esInconsistente :: [Prop] -> Bool
esInconsistente s = null (modelosConjunto s)

-- María Dolores Mateo Ceballos

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = and [esModeloFórmula x f| x<-modelosConjunto s]

--Emilio Martinez Rivero

-- Comentario: la definición no es correcta.

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = esInconsistente ((no f):s)

--María Dolores Mateo Ceballos

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = or [elem x (modelosConjunto s)| x<-(modelosFormula f)]

-- Luis Palma Blanco

</source>

Relación 2a

2015-03-08T17:37:40Z

Luipalbla:

Relación 2a

2015-03-08T17:34:19Z

Luipalbla:

<source lang = "haskell">
-- SintaxisSemanticaProp.hs
-- Lógica proposicional: Sintaxis y semántica
-- José A. Alonso Jiménez <jalonso@us.es>
-- ---------------------------------------------------------------------

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

simbolosPropForm :: Prop -> [Prop]
simbolosPropForm (Atom p) = [Atom p]
simbolosPropForm (Neg p) = simbolosPropForm p
simbolosPropForm (Conj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Disj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Impl p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Equi p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))

-- Luis Curquejo

-- Comentario: La definición se puede mejorar usando la función union.

-- ---------------------------------------------------------------------
-- 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 -> Interpretacion -> Bool
significado (Atom f) xs | elem (Atom f) xs = True
| otherwise = False
significado (Neg f) xs = not (significado f xs)
significado (Conj f q) xs = (significado f xs) && (significado q xs)
significado (Disj f q) xs = (significado f xs) || (significado q xs)
significado (Impl f q) xs | (significado f xs) == True = significado q xs
| otherwise = True
significado (Equi f q) xs = (significado f xs) == (significado q xs)

--Luis Curquejo

-- Comentario: la definición se puede simplificar.

significado :: Prop -> Interpretacion -> Bool
significado (Atom p) i = elem (Atom p) i
significado (Neg p) i = not (significado p i)
significado (Conj p q) i = (significado p i)&&(significado q i)
significado (Disj p q) i = (significado p i)||(significado q i)
significado (Impl p q) i | significado p i = significado q i
| otherwise = True
significado (Equi p q) i = (significado p i)==(significado q i)

--María Dolores Mateo Ceballos

-- ---------------------------------------------------------------------
-- 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 [a] = [[],[a]]
subconjuntos (x:xs) = [x:ys | ys <- sub] ++ sub
where sub = subconjuntos xs
-- Me acordaba de primero (seguro) Javier Rodríguez Vivas
-- Jaime Alberto

subconjuntos :: [a] -> [[a]]
subconjuntos [] = [[]]
subconjuntos (x:xs) = [x:ys | ys<-subconjuntos xs] ++ 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],[]]
-- ---------------------------------------------------------------------

interpretacionesForm :: Prop -> [Interpretacion]
interpretacionesForm f = subconjuntos (simbolosPropForm f)

--Luis Curquejo

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

esModeloFormula :: Interpretacion -> Prop -> Bool
esModeloFormula i f = significado f i

-- Luis Curquejo
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 <- subconjuntos (símbolosPropFórm f), esModeloFórmula i f]

-- Elisa Mazuelos Jiménez

-- Comentario: la definición se puede simplificar usando interpretacionesForm.

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = [xs|xs<-(interpretacionesForm f), esModeloFormula xs f]

--María Dolores Mateo Ceballos

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = aux (interpretacionesForm f)
where aux [] = []
aux (x:xs) | esModeloFormula x f = x : aux xs
| otherwise = aux xs

-- Francisco Javier Carmona

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

esValida :: Prop -> Bool
esValida f = subconjuntos (simPro f) == modelosFormula f

-- Javier Rodríguez Vivas

-- Comentario: la definición se puede simplificar usando interpretacionesForm.

esValida :: Prop -> Bool
esValida f = modelosFormula f == interpretacionesForm f

-- María Dolores Mateo Ceballos
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = null (modelosFórmula f)
--Emilio Martinez Rivero

esInsatisfacible :: Prop -> Bool
esInsatisfacible f = modelosFormula f == []

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . EsInsatisfacible
--Emilio Martinez Rivero

esSatisfacible :: Prop -> Bool
esSatisfacible f = modelosFormula f /= []

-- Francisco Javier Carmona

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

unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (x:xs) = nub(x++ unionGeneral xs)

--Javier Rodríguez Vivas
-- Francisco Javier Carmona

-- Comentario: La definición se puede mejorar usando la función union.

uniónGeneral :: Eq a => [[a]] -> [a]
uniónGeneral = nub . concat

-- Elisa Mazuelos Jiménez

unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (xs:xss) = union xs (unionGeneral xss)

-- Maria del Carmen Mesa Marquez

-- ---------------------------------------------------------------------
-- 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 [simb x | x<-s]

--Emilio Martinez Rivero

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = nub (aux s)
where aux [] = []
aux (x:xs) = simbolosPropForm x ++
simbolosPropConj xs

-- Francisco Javier Carmona

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = unionGeneral (map (simbolosPropForm) s)

-- Luis Palma Blanco

-- ---------------------------------------------------------------------
-- 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 = subconjuntos . símbolosPropConj

-- Elisa Mazuelos Jiménez

-- ---------------------------------------------------------------------
-- 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 = elem False xs == False
where xs = [esModeloFormula i f | f<-s]

--Javier Rodriguez Vivas

-- Comentario: la definición se puede mejorar.

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = and [esModeloFormula i f| f<-s]

--María Dolores Mateo Ceballos

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = aux i s
where aux i [] = True
aux i (x:xs) = esModeloFormula i x &&
esModeloConjunto i xs

-- Francisco Javier Carmona

-- Jaime Alberto
esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i [f] = esModeloFormula i f
esModeloConjunto i (x:xs) | esModeloFormula i x = esModeloConjunto i xs
| otherwise = False

-- ---------------------------------------------------------------------
-- 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 = [x|x<-interpretacionesConjunto s, esModeloConjunto x s]
--Emilio Martinez Rivero
-- ---------------------------------------------------------------------
-- 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 = or [esModeloConjunto x s | x <- (modelosConjunto s)]

-- Elisa Mazuelos Jiménez

-- Comentario: La definición se puede mejorar.

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . esConsistente

-- Elisa Mazuelos Jiménez

esInconsistente :: [Prop] -> Bool
esInconsistente s = null (modelosConjunto s)

-- María Dolores Mateo Ceballos

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = and [esModeloFórmula x f| x<-modelosConjunto s]

--Emilio Martinez Rivero

-- Comentario: la definición no es correcta.

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = esInconsistente ((no f):s)

--María Dolores Mateo Ceballos

</source>