Relación 12 - Historial de revisiones

Luipalbla en 14:49 11 may 2015

2015-05-11T14:49:07Z

Luipalbla en 14:48 11 may 2015

2015-05-11T14:48:29Z

Luipalbla en 15:46 9 may 2015

2015-05-09T15:46:14Z

Fracarmol1 en 17:49 30 abr 2015

2015-04-30T17:49:03Z

Mjoseh: Página creada con ' -- ResolucionProposicional.hs -- Resolución proposicional. -- --------------------------------------------------------------------- module Resolucion...'

2015-04-29T10:24:49Z

Página creada con '<source lang = "haskell"> -- ResolucionProposicional.hs -- Resolución proposicional. -- --------------------------------------------------------------------- module Resolucion...'

Página nueva

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

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = undefined

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

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = undefined

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

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = undefined

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

esTautología :: Cláusula -> Bool
esTautología c = undefined

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

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = undefined

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

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

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

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = undefined

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

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = undefined

</source>

@@ Línea 119: / Línea 119: @@
 esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s
--- La solución anterior no es correcta ya que esta resuelta por clausula
+-- La solución anterior no es correcta ya que esta resuelta por clausula,
 -- no por resolución, la propuesta en clase es:

@@ Línea 118: / Línea 118: @@
 esInconsistentePorResolución :: [Cláusula] -> Bool
 esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s
 -- ---------------------------------------------------------------------

@@ Línea 113: / Línea 113: @@
 --    ==> True
 -- ---------------------------------------------------------------------
 esInconsistentePorResolución :: [Cláusula] -> Bool
-esInconsistentePorResolución s = undefined
+esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s
 -- ---------------------------------------------------------------------
@@ Línea 130: / Línea 132: @@
 --    esVálidaPorResolución (p --> q)                 ==>  False
 -- ---------------------------------------------------------------------
 esVálidaPorResolución :: Prop -> Bool
-esVálidaPorResolución f = undefined
+esVálidaPorResolución f = esConjuntoValidoDeClausulas (clausulas f)
 -- ---------------------------------------------------------------------
@@ Línea 148: / Línea 152: @@
 --    ==> False
 -- ---------------------------------------------------------------------
 esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-esConsecuenciaPorResolución s f = undefined
+esConsecuenciaPorResolución s f =  esInconsistentePorResolucion (clausulasConjunto ((Neg f):s))
 </source>

@@ Línea 24: / Línea 24: @@
 --    resolvente [no p,q] [no p,no q] q  ==>  [no p]
 -- ---------------------------------------------------------------------
 resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-resolvente c1 c2 l = undefined
+resolvente c1 c2 l = nub (filter (/= l )(filter
 -- ---------------------------------------------------------------------
@@ Línea 36: / Línea 39: @@
 --    resolventes [no p,q] [p,q]     ==>  [[q]]
 -- ---------------------------------------------------------------------
 resolventes :: Cláusula -> Cláusula -> [Cláusula]
-resolventes c1 c2 = undefined
+resolventes c1 c2 = [resolvente c1 c2 l | l <- c1,
 -- ---------------------------------------------------------------------
@@ Línea 48: / Línea 54: @@
 --    ==> [[q],[q,r],[no p,s]]
 -- ---------------------------------------------------------------------
 resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-resolventesCláusulaConjunto c s = undefined
+resolventesCláusulaConjunto c s = aux c s
 -- ---------------------------------------------------------------------
@@ Línea 65: / Línea 76: @@
 --    esTautología []            ==>  False
 -- ---------------------------------------------------------------------
 esTautología :: Cláusula -> Bool
-esTautología c = undefined
+esTautología c = or [elem (complementario x) c | x <- c]
 -- ---------------------------------------------------------------------
@@ Línea 76: / Línea 89: @@
 --    eliminaTautologías [[p, q], [p, q, no p]]  ==>  [[p,q]]
 -- ---------------------------------------------------------------------
 eliminaTautologías :: [Cláusula] -> [Cláusula]
-eliminaTautologías s = undefined
+eliminaTautologías s = [ x | x <- s, not( esTautologia x)]
 -- ---------------------------------------------------------------------