Acciones

Diferencia entre revisiones de «Relación 7»

De Lógica Matemática y fundamentos (2015-16)

(Página creada con '<source lang = "haskell"> -- TablerosSemánticos.hs -- Tableros semánticos proposicionales. -- José A. Alonso Jiménez <jalonso@us.es> -- ------------------------------------...')
 
(entera)
Línea 30: Línea 30:
  
 
literal :: Prop -> Bool
 
literal :: Prop -> Bool
−
literal = undefined
+
literal (Atom f)      = True
 +
literal (Neg (Atom f)) = True
 +
literal _              = False
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 46: Línea 48:
  
 
dobleNegacion :: Prop -> Bool
 
dobleNegacion :: Prop -> Bool
−
dobleNegacion = undefined
+
dobleNegacion (Neg (Neg _)) = True
 +
dobleNegación _            = False
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 55: Línea 58:
  
 
alfa :: Prop -> Bool
 
alfa :: Prop -> Bool
−
alfa = undefined
+
alfa (Conj _ _)      = True
 +
alfa (Neg (Impl _ _)) = True
 +
alfa (Neg (Disj _ _)) = True
 +
alfa _                = False
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 64: Línea 70:
  
 
beta :: Prop -> Bool
 
beta :: Prop -> Bool
−
beta = undefined
+
beta (Disj _ _)      = True
 +
beta (Impl _ _)      = True
 +
beta (Neg (Conj _ _)) = True
 +
beta (Equi _ _)      = True
 +
beta (Neg (Equi _ _)) = True
 +
beta _                = False
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 76: Línea 87:
  
 
componentes :: Prop -> [Prop]
 
componentes :: Prop -> [Prop]
−
componentes = undefined
+
componentes (Neg (Neg f))    = [f]
−
 
+
componentes (Conj f g)      = [f, g]
 +
componentes (Neg (Impl f g)) = [f, Neg g]
 +
componentes (Neg (Disj f g)) = [Neg f, Neg g]
 +
componentes (Disj f g)      = [f, g]
 +
componentes (Impl f g)      = [Neg f, g]
 +
componentes (Neg (Conj f g)) = [Neg f, Neg g]
 +
componentes (Equi f g)      = [Conj f g, Conj (Neg f) (Neg g)]
 +
componentes (Neg (Equi f g)) = [Conj f (Neg g), Conj (Neg f) g]
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
 
-- Modelos mediante tableros                                          --
 
-- Modelos mediante tableros                                          --
Línea 92: Línea 110:
  
 
conjuntoDeLiterales :: [Prop] -> Bool
 
conjuntoDeLiterales :: [Prop] -> Bool
−
conjuntoDeLiterales fs = undefined
+
conjuntoDeLiterales fs = and [literal f | f <- fs]
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 103: Línea 121:
  
 
tieneContradiccion :: [Prop] -> Bool
 
tieneContradiccion :: [Prop] -> Bool
−
tieneContradiccion fs = undefined
+
tieneContradiccion fs = [f | f <- fs, elem (Neg f) fs] /= []
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 114: Línea 132:
  
 
expansionDN :: [Prop] -> Prop -> [[Prop]]
 
expansionDN :: [Prop] -> Prop -> [[Prop]]
−
expansionDN fs f = undefined
+
expansionDN fs f = [(componentes f) `union` (delete f fs)]
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 125: Línea 143:
  
 
expansionAlfa :: [Prop] -> Prop -> [[Prop]]
 
expansionAlfa :: [Prop] -> Prop -> [[Prop]]
−
expansionAlfa fs f = undefined
+
expansionAlfa fs f = [(componentes f) `union` (delete f fs)]
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 136: Línea 154:
  
 
expansionBeta :: [Prop] -> Prop -> [[Prop]]
 
expansionBeta :: [Prop] -> Prop -> [[Prop]]
−
expansionBeta fs f = undefined
+
expansionBeta fs f = [[g] `union` (delete f fs) | g <- componentes f]
 +
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 148: Línea 167:
  
 
sucesores :: [Prop] -> [[Prop]]
 
sucesores :: [Prop] -> [[Prop]]
−
sucesores = undefined
+
sucesores fs
−
 
+
    | doblesNegación /= []  = expansiónDN  fs (head doblesNegación)
 +
    | alfas /= []          = expansiónAlfa fs (head alfas)
 +
    | betas /= []          = expansiónBeta fs (head betas)
 +
    where doblesNegación = [f | f <- fs, dobleNegación f]
 +
          alfas          = [f | f <- fs, alfa f]
 +
          betas          = [f | f <- fs, beta f]
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
 
-- Ejercicio 11: Definir la función
 
-- Ejercicio 11: Definir la función
Línea 162: Línea 186:
  
 
modelosTab :: [Prop] -> [[Prop]]
 
modelosTab :: [Prop] -> [[Prop]]
−
modelosTab = undefined
+
modelosTab fs
 +
    | tieneContradicción fs  = []
 +
    | conjuntoDeLiterales fs = [fs]
 +
    | otherwise              = uniónGeneral [modelosTab gs
 +
                                            | gs <- sucesores fs]
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 174: Línea 202:
  
 
subconjunto :: Eq a => [a] -> [a] -> Bool
 
subconjunto :: Eq a => [a] -> [a] -> Bool
−
subconjunto xs ys = undefined
+
subconjunto xs ys = and [elem x ys | x <- xs]
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 186: Línea 214:
  
 
modelosGenerales :: [Prop] -> [[Prop]]
 
modelosGenerales :: [Prop] -> [[Prop]]
−
modelosGenerales fs = undefined
+
modelosGenerales fs = [gs | gs <- modelos, [hs | hs <- delete gs modelos, subconjunto hs gs] == []]
 +
    where modelos = modelosTab fs
  
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
Línea 202: Línea 231:
  
 
esTeoremaPorTableros :: Prop -> Bool
 
esTeoremaPorTableros :: Prop -> Bool
−
esTeoremaPorTableros f = undefined
+
esTeoremaPorTableros f = modelosTab [Neg f] == []
−
 
 
 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
 
-- Consecuencia por tableros                                          --
 
-- Consecuencia por tableros                                          --
Línea 219: Línea 247:
  
 
esDeduciblePorTableros :: [Prop] -> Prop -> Bool
 
esDeduciblePorTableros :: [Prop] -> Prop -> Bool
−
esDeduciblePorTableros fs f = undefined
+
esDeduciblePorTableros fs f = modelosTab ((Neg f):fs) == []
  
  
 
</source>
 
</source>

Revisión del 12:59 26 abr 2016

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

module TablerosSemanticos where

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

import SintaxisSemantica
import Data.List 

-- ---------------------------------------------------------------------
-- Literales                                                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
--    literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo, 
--    literal p               ==>  True
--    literal (no p)          ==>  True
--    literal (no (p --> q))  ==>  False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal  (Atom f)      = True
literal (Neg (Atom f)) = True
literal _              = False

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

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

dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg _)) = True
dobleNegación _             = False 

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

alfa :: Prop -> Bool
alfa (Conj _ _)       = True
alfa (Neg (Impl _ _)) = True
alfa (Neg (Disj _ _)) = True
alfa _                = False

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

beta :: Prop -> Bool
beta (Disj _ _)       = True
beta (Impl _ _)       = True
beta (Neg (Conj _ _)) = True
beta (Equi _ _)       = True
beta (Neg (Equi _ _)) = True
beta _                = False

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

componentes :: Prop -> [Prop]
componentes (Neg (Neg f))    = [f]
componentes (Conj f g)       = [f, g]
componentes (Neg (Impl f g)) = [f, Neg g]
componentes (Neg (Disj f g)) = [Neg f, Neg g]
componentes (Disj f g)       = [f, g]
componentes (Impl f g)       = [Neg f, g]
componentes (Neg (Conj f g)) = [Neg f, Neg g]
componentes (Equi f g)       = [Conj f g, Conj (Neg f) (Neg g)]
componentes (Neg (Equi f g)) = [Conj f (Neg g), Conj (Neg f) g]
-- ---------------------------------------------------------------------
-- Modelos mediante tableros                                          --
-- ---------------------------------------------------------------------

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

conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales fs = and [literal f | f <- fs]

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

tieneContradiccion :: [Prop] -> Bool
tieneContradiccion fs = [f | f <- fs, elem (Neg f) fs] /= []

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

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = [(componentes f) `union` (delete f fs)]

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

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = [(componentes f) `union` (delete f fs)]

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

expansionBeta :: [Prop] -> Prop -> [[Prop]]
expansionBeta fs f = [[g] `union` (delete f fs) | g <- componentes f]
 

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

sucesores :: [Prop] -> [[Prop]]
sucesores  fs
    | doblesNegación /= []  = expansiónDN   fs (head doblesNegación)
    | alfas /= []           = expansiónAlfa fs (head alfas)
    | betas /= []           = expansiónBeta fs (head betas)
    where doblesNegación = [f | f <- fs, dobleNegación f]
          alfas          = [f | f <- fs, alfa f]
          betas          = [f | f <- fs, beta f]
-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
--    modelosTab :: [Prop] -> [[Prop]]
-- tal que (modelosTab fs) es el conjunto de los modelos de fs
-- calculados mediante el método de tableros semánticos. Por ejemplo,
--    modelosTab [p --> q, no(q --> p)]  
--    ==> [[no p,q],[q,no p]]
--    modelosTab [p --> q, no q --> no p]  
--    ==> [[q,no p],[no p],[q],[no p,q]]
-- ---------------------------------------------------------------------

modelosTab :: [Prop] -> [[Prop]]
modelosTab  fs 
    | tieneContradicción fs  = []
    | conjuntoDeLiterales fs = [fs]
    | otherwise              = uniónGeneral [modelosTab gs 
                                             | gs <- sucesores fs]

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

subconjunto :: Eq a => [a] -> [a] -> Bool
subconjunto xs ys = and [elem x ys | x <- xs]

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

modelosGenerales :: [Prop] -> [[Prop]]
modelosGenerales fs = [gs | gs <- modelos, [hs | hs <- delete gs modelos, subconjunto hs gs] == []]
    where modelos = modelosTab fs

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

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

esTeoremaPorTableros :: Prop -> Bool
esTeoremaPorTableros f = modelosTab [Neg f] == []
-- ---------------------------------------------------------------------
-- Consecuencia por tableros                                          --
-- ---------------------------------------------------------------------

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

esDeduciblePorTableros :: [Prop] -> Prop -> Bool
esDeduciblePorTableros fs f = modelosTab ((Neg f):fs) == []
Obtenido de «https://www.glc.us.es/~jalonso/LMF2016/index.php?title=Relación_7&oldid=195»