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

Relación 11

2013-05-14T15:53:27Z

Josconbel:

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

--Jose M Contreras

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 x = union (delete x c1) (delete (complementario x) c2)
--La función complementario se define en el fichero importado FormasNormales

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

--Jose M Contreras

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 = [resolvente c1 c2 x| x<-c1, elem (complementario x) 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]]
-- ---------------------------------------------------------------------

--Jose M Contreras

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s = unionGeneral [resolventes c x|x<-s]

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

--Jose M Contreras

esTautologia :: Clausula -> Bool
esTautologia c = or[elem (complementario x) (delete 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]]
-- ---------------------------------------------------------------------

--Jose M Contreras

eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias 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
-- ---------------------------------------------------------------------

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>

Relación 11

2013-05-14T14:55:32Z

Josconbel:

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

--Jose M Contreras

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 x = union (delete x c1) (delete (complementario x) c2)
--La función complementario se define en el fichero importado FormasNormales

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

--Jose M Contreras

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 = [resolvente c1 c2 x| x<-c1, elem (complementario x) 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]]
-- ---------------------------------------------------------------------

--Jose M Contreras

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s = unionGeneral [resolventes c x|x<-s]

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

Relación 10

2013-05-10T09:43:30Z

Josconbel:

<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]
-- ---------------------------------------------------------------------
--José M Contreras

clausula :: Prop -> Clausula
clausula f | literal f = [f]
clausula (Disj f g)=sort((clausula f)`union`(clausula g))

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

--José M Contreras

clausulasFNC :: Prop -> [Clausula]
clausulasFNC (Conj f g)= union (clausulasFNC f) (clausulasFNC 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]]
-- ---------------------------------------------------------------------

--José M Contreras

clausulas :: Prop -> [Clausula]
clausulas = clausulasFNC . formaNormalConjuntiva

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

cláusulasConjunto :: [Prop] -> [Cláusula]
cláusulasConjunto s = undefined

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

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

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

símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
símbolosProposicionalesConjuntoCláusula s = undefined

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

interpretacionesCláusula :: Cláusula -> [Interpretación]
interpretacionesCláusula c = undefined

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

interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
interpretacionesConjuntoCláusula c = undefined

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

esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral = undefined

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

esModeloCláusula :: Interpretación -> Cláusula -> Bool
esModeloCláusula i c = undefined

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

modelosCláusula :: Cláusula -> [Interpretación]
modelosCláusula c = undefined

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

esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
esModeloConjuntoCláusulas i s = undefined

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

modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
modelosConjuntoCláusulas s = undefined

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

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

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

esCláusulaInsatisfacible :: Cláusula -> Bool
esCláusulaInsatisfacible c = undefined

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

esCláusulaSatisfacible :: Cláusula -> Bool
esCláusulaSatisfacible c = undefined

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

esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
esConjuntoVálidoDeCláusulas s = undefined

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

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

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

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

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

esVálidaPorCláusulas :: Prop -> Bool
esVálidaPorCláusulas f = undefined

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

esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
esConsecuenciaEntreCláusulas s1 s2 = undefined

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

esConsecuenciaPorCláusulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorCláusulas s f = undefined

</source>

Relación 8

2013-04-24T13:20:39Z

Josconbel:

<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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = 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
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
else False

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
tieneContradiccion :: [Prop] -> Bool
tieneContradiccion [f] = False
tieneContradiccion ((Neg f):fs) = if elem f fs then True else
tieneContradiccion fs
tieneContradiccion (f:fs)= if elem (no f) fs then True else
tieneContradiccion fs

-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]

-- ---------------------------------------------------------------------
-- 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]]
-- ---------------------------------------------------------------------
--José María Contreras
elim (Neg(Neg f)) = f

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = [(elim 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]]
-- ---------------------------------------------------------------------
--José María Contreras

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = [(componentes f)`union`(delete 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]]
-- ---------------------------------------------------------------------
--José María Contreras

expansionBeta :: [Prop] -> Prop -> [[Prop]]
expansionBeta fs f = [x:(delete f fs)| x<-(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 = undefined

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

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

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

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

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

</source>

Relación 8

2013-04-24T13:13:44Z

Josconbel:

<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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = 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
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
else False

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
tieneContradiccion :: [Prop] -> Bool
tieneContradiccion [f] = False
tieneContradiccion ((Neg f):fs) = if elem f fs then True else
tieneContradiccion fs
tieneContradiccion (f:fs)= if elem (no f) fs then True else
tieneContradiccion fs

-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]

-- ---------------------------------------------------------------------
-- 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]]
-- ---------------------------------------------------------------------
--José María Contreras
elim (Neg(Neg f)) = f

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = [(elim 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]]
-- ---------------------------------------------------------------------
--José María Contreras

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = [(componentes f)`union`(delete 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 = undefined

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

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

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

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

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

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

</source>

Relación 8

2013-04-24T11:31:38Z

Josconbel:

<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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = 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
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
else False

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
tieneContradiccion :: [Prop] -> Bool
tieneContradiccion [f] = False
tieneContradiccion ((Neg f):fs) = if elem f fs then True else
tieneContradiccion fs
tieneContradiccion (f:fs)= if elem (no f) fs then True else
tieneContradiccion fs

-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]

-- ---------------------------------------------------------------------
-- 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]]
-- ---------------------------------------------------------------------
--José María Contreras
elim (Neg(Neg f)) = f

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = [(elim 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 = undefined

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

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

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

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

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

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

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

</source>

Ejercicio 2

2013-04-12T12:46:19Z

Josconbel: /* Selección del ejercicio */

== Enunciado ==
El segundo ejercicio evaluable consiste en la realización de una demostración por deducción natural en la Lógica de primer orden, con Isabelle/HOL.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[T2|T2]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* El ejercicio resuelto se enviará a mjoseh@us.es en un fichero usuario_2.thy antes del viernes 26 de abril de 2013.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1: Francisco Vilches Chacón
* Ejercicio 2:
* Ejercicio 3:
* Ejercicio 4:
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8:
* Ejercicio 9:
* Ejercicio 10:
* Ejercicio 11:
* Ejercicio 12:
* Ejercicio 13:
* Ejercicio 14:
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17:
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20:
* Ejercicio 21:
* Ejercicio 22:
* Ejercicio 23: Irene Araujo Guijo
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José Mª Contreras Beltrán
* Ejercicio 27: FºJavier Sanz Gil
* Ejercicio 28: Isabel Duarte Tosso
* Ejercicio 29:
* Ejercicio 30:
* Ejercicio 31:
* Ejercicio 32:
* Ejercicio 33:

Relación 3

2013-03-05T14:41:44Z

Josconbel:

<source lang="isar">
header {* R3: Deducción natural proposicional *}

theory R3
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación. *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

section {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

-- "Pedro G. Ros"
lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show 3: "q" using 1 2 by (rule mp)
qed

-- "Isabel Duarte"
lemma ejercicio_1b:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms(1,2) by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

-- "Pedro G. Ros"
lemma ejercicio_2a:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show 5: "r" using 2 4 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

-- "Pedro G. Ros"
lemma ejercicio_3a:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"
proof -
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show 6: "r" using 4 5 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

-- "Pedro G. Ros"
lemma ejercicio_4a:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{assume 3:"p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
thus "p⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
--"Isabel Duarte"

lemma ejercicio_5a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{assume 3: "q"
{assume 4: "p"
have "q ⟶ r" using 1 4 ..
hence 5: "r" using 3 ..}
hence 6: "p ⟶ r" by (rule impI)}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "José Mª Contreras"

lemma ejercicio_6a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2: "p ⟶ q"
{assume 3: "p"
have 4: "q ⟶ r" using 1 3 ..
have 5: "q" using 2 3 ..
have "r" using 4 5 ..}
hence "p ⟶ r" by (rule impI)}
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

-- "Pedro G. Ros Reina"

lemma ejercicio_13:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_17:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end
</source>