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

Relación 7

2015-04-12T18:20:38Z

Mansortri:

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

module TablerosSemanticos where

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

import SintaxisSemantica
import Data.List

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

-- ---------------------------------------------------------------------
-- Ejercicio 0: 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

-- Jaime Alberto

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

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

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

dobleNegación :: Prop -> Bool
dobleNegación (Neg (Neg f)) = 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 f g) = True
alfa (Neg (Disj f g))=True
alfa (Neg(Impl f g))=True
alfa (Equi f g) = 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 f g) = True
beta (Neg (Conj f g))=True
beta (Impl f g)=True
beta (Neg (Equi f g)) = 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 (Conj f g) = [f,g]
componentes (Neg (Impl f g)) = [f, no g]
componentes (Neg (Disj f g)) = [no f, no g]
componentes (Equi f g) = [no (f-->g), no (g-->f)]

componentes g = [quitanegacion (no x)|x<-componentes (quitanegacion (no g))]
where quitanegacion (Neg (Neg f)) =f
quitanegacion f = f

-- Francisco Javier Carmona

componentes1 :: Prop -> [Prop]
componentes1 (Neg (Neg f)) = [f]
componentes1 (Conj f g) = [f,g]
componentes1 (Neg (Impl f g)) = [f, Neg g]
componentes1 (Neg (Disj f g)) = [Neg f, Neg g]
componentes1 (Equi f g) = [Impl f g, Impl g f]
componentes1 (Disj f g) = [f,g]
componentes1 (Impl f g) = [Neg f, g]
componentes1 (Neg (Conj f g)) = [Neg f, Neg g]
componentes1 (Neg (Equi f g)) = [Neg (Impl f g), Neg (Impl g f)]

-- ---------------------------------------------------------------------
-- 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 = all (literal)

-- Francisco Javier Carmona

conjuntoDeLiterales1 :: [Prop] -> Bool
conjuntoDeLiterales1 fs = aux fs
where aux [] = True
aux (x:xs) = literal x && aux xs

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

tieneContradicción :: [Prop] -> Bool
tieneContradicción fs = or [elem (no p) fs| p<-fs]
tieneContradicción' fs = or (map (\x-> elem (no x) fs) fs)

tieneContradiccion1 :: [Prop]->Bool
tieneContradiccion1 [] = False
tieneContradiccion1 ((Neg x):xs) = elem x xs || elem (Neg (Neg x)) xs || tieneContradiccion xs
tieneContradiccion1 (x:xs) = elem (Neg x) xs || tieneContradiccion xs

-- Aunque en general tieneContradiccion1 no es más eficiente, sí lo puede ser para
-- casos puntuales, p.e. ys = [Neg (Atom "q")] ++ [Atom "s" | x <- [1..100000]]++[Atom "q"]

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

expansiónDN :: [Prop] -> Prop -> [[Prop]]
expansiónDN fs (Neg (Neg f)) = [f:(filter (/=Neg(Neg f)) fs)]

-- Francisco Javier Carmona

expansionDN1 :: [Prop] -> Prop -> [[Prop]]
expansionDN1 fs f = [(componentes f) ++ [ x | x <- fs, x /= f]]

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

expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
expansiónAlfa fs f = [componentes f++(filter (/=f) fs)]

-- Francisco Javier Carmona

expansionAlfa1 :: [Prop] -> Prop -> [[Prop]]
expansionAlfa1 fs f = [(componentes f) ++ [x | x <- fs, x /= f]]

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

expansiónBeta :: [Prop] -> Prop -> [[Prop]]
expansiónBeta fs f = [x:(filter(/=f) fs), y:(filter (/=f) fs)]
where x = head (componentes f)
y = last (componentes f)

-- Francisco Javier Carmona

expansionBeta1 :: [Prop] -> Prop -> [[Prop]]
expansionBeta1 fs f = [[head(componentes f)] ++ [x | x <- fs, x /= f],
[head( reverse(componentes f))] ++ [x | x <- fs, x /= 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 xs |existeDN xs = expansiónDN xs x
|existeAlfa xs = expansiónAlfa xs y
| otherwise = expansiónBeta xs z
where existeDN xs = or (map
(dobleNegación) xs)
existeAlfa xs= or (map (alfa) xs)
x= head (filter (dobleNegación) xs)
y= head (filter (alfa) xs)
z= head (filter (beta) xs)

-- Francisco Javier Carmona

sucesores1 :: [Prop] -> [[Prop]]
sucesores1 fs | [] /= haydoble fs = expansionDN fs (head (haydoble fs))
| [] /= hayalfa fs = expansionAlfa fs (head (hayalfa fs))
| [] /= haybeta fs = expansionBeta fs (head (haybeta fs))
| otherwise = [[]]

haydoble xs = [ x | x <- xs, dobleNegacion x]

hayalfa ys = [y | y <- ys, alfa y]

haybeta zs = [z | z <- zs, beta z]

-- ---------------------------------------------------------------------
-- 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 = [x |x<-aux xs, (not.tieneContradicción) x]

where aux xs |conjuntoDeLiterales xs = [xs]
| otherwise =map (nub) (concat[(modelosTab x)|x<-sucesores xs])

-- ---------------------------------------------------------------------
-- 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 [] _ = True
subconjunto [x] [y] =False
subconjunto (x:xs) ys |elem x ys = subconjunto xs ys
| otherwise=False

-- Francisco Javier Carmona

subconjunto1 :: Eq a => [a] -> [a] -> Bool
subconjunto1 xs ys = length xs == length [x | x <- xs, elem x ys]

-- ---------------------------------------------------------------------
-- 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 = aux ps (modelosTab fs)
where aux [] ys = ys
aux (x:xs) ys = aux xs (delete x ys)
ps = [x |x<-modelosTab fs, f x (modelosTab fs)]
f x xs = or [ subconjunto y x|y<-xs,x/=y]

modelosGenerales1 :: [Prop] -> [[Prop]]
modelosGenerales1 xs = limpieza (modelosTab xs)
limpieza [] = []
limpieza (x:xs) | or [subconjunto x y | y <- xs] = limpieza xs
| otherwise = x:limpieza [y | y <- xs, not(subconjunto y
x)]

-- ---------------------------------------------------------------------
-- 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 = null (modelosTab [no f])

-- Francisco Javier Carmona

esTeoremaPorTableros1 :: Prop -> Bool
esTeoremaPorTableros1 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 = null (modelosGenerales (no f:fs))

-- Francisco Javier Carmona

esDeduciblePorTableros1 :: [Prop] -> Prop -> Bool
esDeduciblePorTableros1 fs f = modelosTab ((Neg f):fs) == []

</source>

Relación 7

2015-04-11T11:09:06Z

Mansortri:

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

module TablerosSemanticos where

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

import SintaxisSemantica
import Data.List

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

-- ---------------------------------------------------------------------
-- Ejercicio 0: 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
-- dobleNegación :: Prop -> Bool
-- tal que (dobleNegación f) se verifica si f es una doble negación. Por
-- ejemplo,
-- dobleNegación (no (no p)) ==> True
-- dobleNegación (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

dobleNegación :: Prop -> Bool
dobleNegación (Neg (Neg f)) = 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 f g) = True
alfa (Neg (Disj f g))=True
alfa (Neg(Impl f g))=True
alfa (Equi f g) = 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 f g) = True
beta (Neg (Conj f g))=True
beta (Impl f g)=True
beta (Neg (Equi f g)) = 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 (Conj f g) = [f,g]
componentes (Neg (Impl f g)) = [f, no g]
componentes (Neg (Disj f g)) = [no f, no g]
componentes (Equi f g) = [no (f-->g), no (g-->f)]

componentes g = [quitanegacion (no x)|x<-componentes (quitanegacion (no g))]
where quitanegacion (Neg (Neg f)) =f
quitanegacion f = f
-- ---------------------------------------------------------------------
-- 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 = all (literal)

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

tieneContradicción :: [Prop] -> Bool
tieneContradicción fs = or [elem (no p) fs| p<-fs]
tieneContradicción' fs = or (map (\x-> elem (no x) fs) fs)

tieneContradiccion1 :: [Prop]->Bool
tieneContradiccion1 [] = False
tieneContradiccion1 ((Neg x):xs) = elem x xs || elem (Neg (Neg x)) xs || tieneContradiccion xs
tieneContradiccion1 (x:xs) = elem (Neg x) xs || tieneContradiccion xs

-- Aunque en general tieneContradiccion1 no es más eficiente, sí lo puede ser para
-- casos puntuales, p.e. ys = [Neg (Atom "q")] ++ [Atom "s" | x <- [1..100000]]++[Atom "q"]

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

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

expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
expansiónAlfa fs f = [componentes f++(filter (/=f) fs)]

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

expansiónBeta :: [Prop] -> Prop -> [[Prop]]
expansiónBeta fs f = [x:(filter(/=f) fs), y:(filter (/=f) fs)]
where x = head (componentes f)
y = last (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 xs |existeDN xs = expansiónDN xs x
|existeAlfa xs = expansiónAlfa xs y
| otherwise = expansiónBeta xs z
where existeDN xs = or (map
(dobleNegación) xs)
existeAlfa xs= or (map (alfa) xs)
x= head (filter (dobleNegación) xs)
y= head (filter (alfa) xs)
z= head (filter (beta) xs)

-- ---------------------------------------------------------------------
-- 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 = [x |x<-aux xs, (not.tieneContradicción) x]

where aux xs |conjuntoDeLiterales xs = [xs]
| otherwise =map (nub) (concat[(modelosTab x)|x<-sucesores xs])

-- ---------------------------------------------------------------------
-- 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 [] _ = True
subconjunto [x] [y] =False
subconjunto (x:xs) ys |elem x ys = subconjunto xs ys
| otherwise=False
-- ---------------------------------------------------------------------
-- 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 = aux ps (modelosTab fs)
where aux [] ys = ys
aux (x:xs) ys = aux xs (delete x ys)
ps = [x |x<-modelosTab fs, f x (modelosTab fs)]
f x xs = or [ subconjunto y x|y<-xs,x/=y]

-- ---------------------------------------------------------------------
-- 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 = null (modelosTab [no 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 = null (modelosGenerales (no f:fs))

</source>

Relación 2

2015-02-13T18:56:45Z

Mansortri:

=== Relación 2: Representación del conocimiento proposicional ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento
<blockquote>
''Siempre que un número x es divisible por 10, acaba en 0. El número x no acaba en 0. Por lo tanto, x no es divisible por 10.''
</blockquote>
Usando los símbolos D: el número es divisible por 10 y C: el número acaba en cero.
----

'''Solución:'''

(D -> C)

-C

||- -D

''' Pablo José Gerlach Mena'''

''' He utilizado los símbolos -> (condicional), - (negación) y ||- (por tanto). '''

(Observación: Sería mas conveniente en mi opinión usar el símbolo '¬' para la negación,
aunque simplemente es una cuestión de notación) Emilio Martínez Rivero

(Yo opino igual, más que nada para seguir manteniendo la notación vista en clase, al igual que opino que sería conveniente usar '|=' para Por tanto, notación también vista en clase, más que nada para que no haya mucha diferencia entre la clase y los ejercicios que resolvemos por aquí) José Martín Delgado

----
'''Ejercicio 2.''' Formalizar el siguiente argumento
<blockquote>
''Si la válvula está abierta o la monitorización está preparada, entonces se envía una señal de reconocimiento y un mensaje de funcionamiento al controlador del ordenador. Si se envía un mensaje de funcionamiento al controlador del ordenador o el sistema está en estado normal, entonces se aceptan las órdenes del operador. Por lo tanto, si la válvula está abierta, entonces se aceptan las órdenes del operador.''
</blockquote>
Usando los símbolos V: La válvula está abierta, P: La monitorización está preparada, R: Envía una señal de reconocimiento, F: Envía un mensaje de funcionamiento, A: Se aceptan órdenes del operador y N: El sistema está en estado normal.
----

'''Solución:'''

((V v P) -> (R & F))

((F v N) -> A)

||- (V -> A)

'''Pablo José Gerlach Mena'''

''' He utilizado los símbolos -> (condicional), - (negación), v (disyunción), & (conjunción) y ||- (por tanto). '''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento
<blockquote>
''Cuando tanto la temperatura como la presión atmosférica permanecen contantes, no llueve. La temperatura permanece constante. Por lo tanto, en caso de que llueva, la presión atmosférica no permanece constante.''
</blockquote>
Usando los símbolos T: La temperatura permanece constante, P: La presión atmosférica permanece constante y L: Llueve
----

'''Solución:'''

((T & P) -> -L)

T

||- (L -> -P)

'''Pablo José Gerlach Mena'''

''' He utilizado los símbolos -> (condicional), - (negación), v (disyunción), & (conjunción) y ||- (por tanto). '''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento
<blockquote>
''En cierto experimento, cuando hemos empleado un fármaco A, el paciente ha mejorado considerablemente en el caso, y sólo en el caso, en que no se haya empleado también un fármaco B. Además, o se ha empleado el fármaco A o se ha empleado el fármaco B. En consecuencia, podemos afirmar que si no hemos empleado el fármaco B, el paciente ha mejorado considerablemente.''
</blockquote>
Usando los símbolos A: Hemos empleado el fármaco A, B: Hemos empleado el fármaco B y M: El paciente ha mejorado notablemente.
----

'''Solución:'''

((A & -B) -> M)

(A v B)

||- (-B -> M)

'''Pablo José Gerlach Mena'''

''' He utilizado los símbolos -> (condicional), - (negación), v (disyunción), & (conjunción) y ||- (por tanto). '''
----
'''Ejercicio 5.''' Definir por recursión sobre fórmulas las siguientes funciones

* nv(F) que calcula el número variables proposicionales que ocurren en la fórmula F. Por ejemplo,
: nv(p → p ∨ q) = 3.
* prof(F) que calcula la profundidad del árbol de análisis de la fórmula F. Por ejemplo,
: prof(p → p ∨ q) = 2.

Demostrar por inducción, que para toda fórmula F,
: nv(F) ≤ 2^prof(F)
----

'''Solución:'''

'''1) Vamos a definir la función nv(F) como:'''

nv(F) = 1 ...................... si F es atómica

nv(F) = nv(G) ................ si F es -G

nv(F) = nv(G) + nv(H) ..... si F es (G * H)

'''Pablo José Gerlach Mena'''

'''He utilizado los símbolos - (negación) y * (operación binaria).'''

'''2) Vamos a definir la función prof(F) como:'''

prof(F) = 0 ...................................... si F es atómica

prof(F) = 1 + prof(G) ........................ si F es -G

prof(F) = 1 + max{prof(G),prof(H)} ..... si F es (G * H)

'''Pablo José Gerlach Mena'''

'''He utilizado los símbolos - (negación) y * (operación binaria).'''

Demostración: (nv(F)≤2^prof(F))

Caso base: (F atómico)

nv(F) = 1 y 2^prof(F)= 2^0 = 1 ==> nv(F)≤ 2^prof(F) [De hecho es igual]

Hipótesis de inducción: Supongamos que nv(F)≤ 2^prof(F) y nv(G)≤ 2^prof(G).

Entonces 1) nv(¬F)= nv(F) y 2^(prof(¬F)) = 2^(1+prof(F))=2*2^(prof(F))

nv(F) ≤ 2^(prof(F) por H.I. ===> nv(¬F)=nv(F) ≤2*2^(prof(F)) = 2^(prof(¬F)

2) nv(F*G) = nv(F)+nv(G) y 2^prof(F*G)= 2^(1+max{prof(F),prof(G)})

Tenemos ahora dos posibles casos:

Caso1: prof(F)≤prof(G):: H1

Entonces tenemos que nv(F)≤2^prof(F) por H.I ==> nv(F)≤2^prof(G) (por H1)
nv(G)≤2^prof(G) por H.I

Luego nv(F*G) = nv(G)+nv(F)≤2*2^(prof(G))=2^(1+max{prof(G),prof(F)}) = 2^prof(G*F)
Por tanto nv(F*G)≤2^prof(F*G)

Caso2: Es análogo al Caso1.

QED.

Emilio Martínez Rivero

----
'''Ejercicio 6.''' ¿Existe un conjunto S de tres fórmulas tal que de todos los subconjuntos de S sólo uno es consistente?
----

'''Solución:'''

Creo que sí. Bastaría tomar un conjunto S = {F_1, F_2, F_3} de modo que dos de ellas fueran insatisfacibles y la restante fuera una tautología. Obtendríamos entonces los siguientes subconjuntos:

{F_1, F_2, F_3} (no consistente por ser F_1 y F_2 insatisfacibles)

{F_1, F_2} (no consistente por ser F_1 y F_2 insatisfacibles)

{F_1, F_3} (no consistente por ser F_1 insatisfacible)

{F_2, F_3} (no consistente por ser F_2 insatisfacible)

{F_1} (no consistente por ser F_1 insatisfacible)

{F_2} (no consistente por ser F_2 insatisfacible)

{F_3} (consistente por ser F_3 una tautología)

'''Pablo José Gerlach Mena'''

----
'''Ejercicio 7.''' ¿Es cierto que si F → G y F son satisfacibles, entonces G es satisfacible? Si es cierto, dar una explicación. Si no es cierto, dar un contraejemplo.
----

'''Solución:'''

Construyamos el siguiente esquema de tabla de verdad donde el 0 representa que la fórmula no es satisfacible, y el 1 que sí es satisfacible:

F G | F -> G

0 0 | 0 1* 0 (I1)

0 1 | 0 1* 1 (I2)

1 0 | 1 0* 0 (I3)

1 1 | 1 1* 1 (I4)

Mediante * hemos denotado al resultado de la fórmula (F -> G). Como partimos de que (F -> G) es satisfacible, nos fijamos únicamente en los modelos I1, I2 e I4. Sin embargo, al decirnos que F es satisfacible, debemos eliminar los modelos I1 e I2, ya que en ellos F no es satisfacible. Por lo tanto, obtenemos que el modelo restante para (F -> G) y F satisfacibles es el modelo I4 en el cual G también es satisfacible. Por lo tanto, la respuesta a la pregunta es afirmativa.

'''Pablo José Gerlach Mena'''

'''Solución2:'''

Contraejemplo:

F=p

Q=q&-q

F->Q = p->(q&-q)

F es satsfacible si p=1, F->Q es satisfacible si p=0 pero Q es insatisfacible.

'''Manuel Soriano Trigueros'''

----
'''Ejercicio 8.''' Demostrar o refutar las siguientes proposiciones:

# Si F es una fórmula satisfacible, entonces todas las subfórmulas de F son satisfacibles.
# Existen fórmulas válidas tales que todas sus subfórmulas son válidas.
----

'''Solución:'''

'''1) Si F es una fórmula satisfacible, entonces todas las subfórmulas de F son satisfacibles.'''

La respuesta es falsa. Consideremos la fórmula F dada mediante:

(p v (q & -q)) la cual es satisfacible (tomar por ejemplo el modelo (p,q)=(1,1))

Tenemos que el conjunto de subfórmulas de F viene dado a través de:

Subf(F) = { (p v (q & -q)), p, (q & -q), q, -q}

Observemos que la subfórmula (q & -q) no es satisfacible, con lo cual ya hemos encontrado un contraejemplo válido.

'''Pablo José Gerlach Mena'''

''' He utilizado los símbolos - (negación), v (disyunción) y & (conjunción)'''

'''2) Existen fórmulas válidas tales que todas sus subfórmulas son válidas.'''

Creo que la respuesta es falsa, ya que para todo fórmula F, el conjunto de subfórmulas de F contendrá a las fórmulas atómicas, las cuales nunca son válidas.

'''Pablo José Gerlach Mena'''