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

Relación 10

2013-05-15T17:15:34Z

Mirnunolm:

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

--Isabel Duarte
clausulasConjunto :: [Prop] -> [Cláusula]
clausulasConjunto s = unionGeneral [clausulas f | f <- s]

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

--Isabel Duarte
simbolosProposicionalesClausula :: Clausula -> [Prop]
simbolosProposicionalesClausula = simbolosPropConj

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

--Isabel Duarte
simbolosProposicionalesConjuntoClausula :: [Cláusula] -> [Prop]
simbolosProposicionalesConjuntoClausula s =
unionGeneral [simbolosProposicionalesClausula c | c <- s]

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

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

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

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

--Isabel Duarte
interpretacionesConjuntoClausula :: [Cláusula] -> [Interpretación]
interpretacionesConjuntoClausula c =
subconjuntos (simbolosProposicionalesConjuntoClausula c)

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

--Isabel Duarte
esModeloLiteral :: Interpretacion -> Literal -> Bool
esModeloLiteral i (Atom s) = elem (Atom s) i
esModeloLiteral i (Neg (Atom s)) = notElem (Atom s) i

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

--Isabel Duarte
esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i c = or [esModeloLiteral i p | p <- c]

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

--Isabel Duarte
modelosClausula :: Clausula -> [Interpretacion]
modelosClausula c = [ x | x <- (interpretacionesClausula c), esModeloClausula x c]

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

--Miriam Núñez-Romero

esModeloConjuntoClausulas :: Interpretacion -> [Clausula] -> Bool
esModeloConjuntoClausulas i s = and [esModeloClausula i c|c<-s]

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

--Miriam Núñez-Romero

modelosConjuntoClausulas :: [Clausula] -> [Interpretacion]
modelosConjuntoClausulas s = [i|i<-interpretacionesConjuntoClausula s,
esModeloConjuntoClausulas i s]

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

--Miriam Núñez-Romero

esClausulaValida :: Clausula -> Bool
esClausulaValida c = [l|l<-c,elem (complementario l) c]/=[]

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

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 11

2013-05-14T16:41:22Z

Mirnunolm:

<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

--Miriam Núñez-Romero

resolvente2 :: Clausula -> Clausula -> Literal -> Clausula
resolvente2 c1 c2 l = delete l (delete (complementario l) (c1`union`c2))
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

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

--Miriam Núñez-Romero
esTautologia2 :: Clausula -> Bool
esTautologia2 c = or [elem (complementario x) c |x<-c]

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

--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-14T16:15:09Z

Mirnunolm:

<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

--Miriam Núñez-Romero

resolvente2 :: Clausula -> Clausula -> Literal -> Clausula
resolvente2 c1 c2 l = delete l (delete (complementario l) (c1`union`c2))
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

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

Ejercicio 3

2013-05-06T16:17:55Z

Mirnunolm: /* Selección del ejercicio */

== Enunciado ==
El tercer ejercicio evaluable consiste en la realización de un ejercicio de argumentación en lógica de primer orden, haciendo la demostración por deducción natural con Isabelle/HOL y por tableros semánticos.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[E3|E3]].
* 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.
* Se enviará a mjoseh@us.es antes del viernes 10 de mayo de 2013, dos ficheros: uno usuario_3a.thy con la prueba por deducción natural y otro con la prueba por tableros.
* Los lemas que se usen en una demostración tendrán que ser probados de forma no automática.
* 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:
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3: Salvador Joaquín Franco Peña
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8:
* Ejercicio 9:
* Ejercicio 10: Gonzalo José Muñoz González-Meneses
* Ejercicio 11: José Antonio Jaime Sabín
* Ejercicio 12: Erlinda Menéndez Pérez
* Ejercicio 13: Concepción García Vidal
* Ejercicio 14: Carmen Martínez Navarro
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17: Jesús Horno Cobo
* Ejercicio 18: Lourdes Díaz Mena
* Ejercicio 19: Mª de los Remedios Sillero Denamiel
* Ejercicio 20: Antonio Jesús Molero del Río
* Ejercicio 21: Irene Araujo Guijo
* Ejercicio 22: FºJavier Sanz Gil
* Ejercicio 23:
* Ejercicio 24:
* Ejercicio 25: Pedro José Perea Rojo
* Ejercicio 26: José María Contreras Beltrán
* Ejercicio 27: Isabel Duarte Tosso
* Ejercicio 28: Miriam Núñez-Romero Olmo

Ejercicio 2

2013-04-15T15:42:06Z

Mirnunolm:

== 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: Ana Rocío del Valle Benavides
* Ejercicio 3:
* Ejercicio 4:
* Ejercicio 5: Concepción García Vidal
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8: Inmaculada Arjona Arjona
* Ejercicio 9:
* Ejercicio 10: Carmen Martínez Navarro
* Ejercicio 11: Pedro José Perea Rojo
* Ejercicio 12:
* Ejercicio 13:
* Ejercicio 14:
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17: Miriam Núñez-Romero Olmo
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20:
* Ejercicio 21:
* Ejercicio 22: Erlinda Menéndez Pérez
* 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: Antonio Jesús Molero del Río
* Ejercicio 32: Mª de los Remedios Sillero Denamiel
* Ejercicio 33: Pedro Ros Reina

Relación 3

2013-03-20T18:10:37Z

Mirnunolm:

<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

-- "Pedro G. Ros"
lemma ejercicio_1c:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
using assms ..

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

-- "Isabel Duarte"
lemma ejercicio_2b:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
with `q ⟶ r` show "r" ..
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

-- "Isabel Duarte"
lemma ejercicio_3b:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using assms(1,3) ..
have "q" using assms(2,3) ..
with `q ⟶ r` show "r" ..
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

lemma ejercicio_4d:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
using assms by auto

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

-- "Pedro G. Ros Reina"
lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof -
{assume 1: "q"}
show "q⟶ p" using assms(1) by (rule impI)
qed

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

-- "Pedro G. Ros"
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof -
{assume 1: "p"
hence 2: "q ⟶ p" by (rule impI)}
thus "p ⟶q⟶p" by (rule impI)
qed

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

-- "Carmen Martinez Navarro, Erlinda Menendez Perez"

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

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q⟶ (p⟶ s)"
proof
assume "q"
show "p⟶ s"
proof
assume "p"
with assms have "q⟶ r⟶ s" ..
hence "r⟶ s" using `q` ..
thus "s" using `r`..
qed
qed
qed

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

lemma ejercicio_11a:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ (q ⟶ r)"
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume 3: "p⟶ q"
show 4: "p⟶ r"
proof
assume 5: "p"
have 6: "q" using 3 5 by (rule mp)
have 7:"q⟶ r" using 1 5 by (rule mp)
show 8: "r" using 7 6 ..
qed
qed
qed

-- "Reme Sillero"

lemma ejercicio_11b:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p⟶ (q ⟶ r)` `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12a:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
have 1: "(p⟶ q)⟶ r" using assms by this
{assume 2: "p"
{assume 3: "q"
{assume 4: "p"
have 5: "q" using 3 by this}
hence 6: "p⟶ q" ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶ r" ..}
thus 9: "p⟶ (q⟶ r)" ..
qed

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

-- "Pedro G. Ros"
lemma ejercicio_13b:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_14b:
assumes "p ∧ q"
shows "p"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_15b:
assumes "p ∧ q"
shows "q"
using assms ..

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

-- "Reme Sillero"
lemma ejercicio_18a:
assumes "p ∧ q"
shows "p ⟶ q"
proof
assume "p"
show "q" using assms ..
qed

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

-- "Carmen Martinez Navarro , Erlinda Menendez Perez"

lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ (q ∧ r)"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using assms by (rule conjunct1)
have 4: "q" using 3 2 by (rule mp)
have 5: "p ⟶ r" using assms by (rule conjunct2)
have 6: "r" using 5 2 by (rule mp)
show "q ∧ r" using 4 6 by (rule conjI)
qed

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

-- "Jesús Horno Cobo"

lemma ejercicio_20:
assumes 1:"p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof -
{ assume 3: "p"
have 4: "q ∧ r" using 1 3 by (rule mp)
have 5: "q" using 4 by (rule conjunct1) }
hence 6: "p ⟶ q" by (rule impI)
{ assume 7: "p"
have 8: "q ∧ r" using 1 7 by (rule mp)
have 9: "r" using 8 by (rule conjunct2) }
hence 10: "p ⟶ r" by (rule impI)
show "(p ⟶ q) ∧ (p ⟶ r)" using 6 10 by (rule conjI)
qed

-- "Antonio Jesús Molero"
lemma ejercicio_20a:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "q" ..
qed
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "r" ..
qed
qed

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

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

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

-- "Pedro G. Ros"
lemma ejercicio_22a:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q⟶ r"
proof
assume "q"
have "p∧q" using `p` `q` ..
show "r" using assms `p∧q`..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_23a:
assumes 1:"(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume 2:"p∧q"
hence 3:"p" ..
have 4:"q" using 2 ..
hence 5: "p⟶ q" ..
show"r" using 1 5 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24a:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume 0:"p⟶ q"
show "r"
proof -
have 1: "p" using assms ..
have 2: "q" using 0 1 ..
have 3: "q⟶ r" using assms ..
show 3: "r" using 3 2 ..
qed
qed

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

-- "Pedro G. Ros Reina"
lemma ejercicio_25b:
assumes "p"
shows "p ∨ q"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_26b:
assumes "q"
shows "p ∨ q"
using assms ..

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
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_28a:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume 1: "p∨q"
moreover
{assume "p"
hence "p∨r" by (rule disjI1)}
moreover
{assume "q"
have "r" using assms `q`..
hence "p∨r" ..}
ultimately
show "p∨r" ..
qed

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

-- "Pedro Ros"
lemma ejercicio_29a:
assumes "p ∨ p"
shows "p"
proof-
have "p∨p" using assms by this
moreover
{assume "p"
hence "p" by this}
moreover
{assume "p"
hence "p" by this}
ultimately
show "p" ..
qed

-- "Pedro Ros"
lemma ejercicio_29b:
assumes "p ∨ p"
shows "p"
using assms ..

-- "Antonio Jesús Molero"
lemma ejercicio_29c:
assumes "p ∨ p"
shows "p"
using assms
proof (rule disjE)
assume "p"
thus "p" by this
next
assume "p"
thus "p" by this
qed

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
proof -
show "p∨p" using assms ..
qed

-- "Pedro Ros"
lemma ejercicio_30b:
assumes "p"
shows "p ∨ p"
using assms ..

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

-- "Pedro G. Ros"
lemma ejercicio_31a:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have 1: "p ∨ (q ∨ r)" using assms by this
moreover
{assume "p"
hence "(p∨q)" ..
hence "(p∨q)∨r" ..}
moreover
{assume "(q∨r)"
moreover
{assume "q"
hence "(p∨q)"..
hence "(p∨q)∨r" ..}
moreover
{assume "r"
hence "(p∨q)∨r" ..}
ultimately
have "(p∨q)∨r"..}
ultimately
show "(p∨q)∨r" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms(1)
proof
assume "p∨q"
thus "p∨q∨r"
proof
assume "p"
thus "p∨q∨r" ..
next
assume "q"
hence "q∨r" ..
thus "p∨q∨r" ..
qed
next
assume "r"
hence "q∨r" ..
thus "p∨q∨r" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_33a:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms ..
have 2: "q∨r" using assms ..
moreover
{assume 3: "q"
have "(p∧q)" using 1 3 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
moreover
{assume 4: "r"
have "p∧r" using 1 4 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
ultimately
show "(p ∧ q) ∨ (p ∧ r)" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_34a:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this
moreover
{assume "(p ∧ q)"
hence "p" ..
have "q" using `p ∧ q` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
moreover
{assume "(p∧r)"
hence "p" ..
have "r" using `p ∧ r` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
ultimately
show "p ∧ (q ∨ r)" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_35a:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have 1: "p ∨ (q ∧ r)" using assms by this
moreover
{assume "p"
hence 2: "(p∨q)" ..
have 3: "(p∨r)" using `p` ..
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}
moreover
{assume 5:"(q∧r)"
hence 6: "q" ..
have 7: "r" using 5 ..
have 8: "p∨q" using 6 ..
have 9: "p∨r" using 7 ..
have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}
ultimately
show "(p ∨ q) ∧ (p ∨ r)" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p∨q" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "q"
have "p∨r" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "r"
with `q` have "q∧r"..
hence "p∨(q∧r)"..}
ultimately have "p∨(q∧r)"..}
ultimately show "p∨(q∧r)"..
qed

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

-- "Erlinda Menendez Perez , Carmen Martinez Navarro"

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume 1: "p ∨ q"
thus "r"
proof (rule disjE)
assume 2:"p"
have 3: "p ⟶ r" using assms by (rule conjunct1)
show "r" using 3 2 by (rule mp)
next
assume 5:"q"
have 6: "q ⟶ r" using assms by (rule conjunct2)
show "r" using 6 5 by (rule mp)
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof -
{assume 1: "p"
have 2:"p ∨ q" using 1 ..
have 3: "r" using assms 2 ..}
hence 4: "p⟶r" ..
{assume 5: "q"
have 6: "p ∨ q" using 5 ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶r" ..
show "(p⟶r)∧(q⟶r)" using 4 8 ..
qed

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

-- "Pedro G. Ros Reina"
lemma ejercicio_39b:
assumes "p"
shows "¬¬p"
using assms by (rule notnotI)

-- "Raúl Montes Pajuelo"

lemma ejercicio_39c:
assumes "p"
shows "¬¬p"
proof (rule notI)
assume "¬p"
show False using `¬p` assms..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
{assume 1: "p"
show "q" using assms 1 by (rule notE)}
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
{assume "¬q"
with assms show "¬p" by (rule mt) }
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
proof -
note `p∨q`
moreover
{assume "p"
hence "p" by this}
moreover
{assume "q"
with assms (2) have "p" ..}
ultimately show "p" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
note `p∨q`
moreover
{assume "p"
with assms (2) have False..
hence "q"..}
moreover
{assume "q"
hence "q" .}
ultimately show "q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof -
{assume "¬p∧¬q"
note `p∨q`
moreover
{have "¬p" using `¬p∧¬q`by (rule conjunct1)
assume "p"
with `¬p`have False by (rule notE)}
moreover
{have "¬q" using `¬p∧¬q`by (rule conjunct2)
assume "q"
with `¬q`have False by (rule notE)}
ultimately have False by (rule disjE)}
thus "¬(¬p∧¬q)" by (rule notI)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume "¬p∨¬q"
show False
proof (rule disjE)
{show "¬p∨¬q" using `¬p∨¬q`.
next
show "¬p⟹False"
proof -
{assume "¬p"
have "p" using assms..
with `¬p`show False..}
qed
next
show "¬q⟹False"
proof -
{assume "¬q"
have "q" using assms..
with `¬q`show False..}
qed}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
{assume "p"
hence "p∨q"..
with assms show False..}
qed
next
show "¬q"
proof (rule notI)
{assume "q"
hence "p∨q"..
with assms show False..}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
assume "p∨q"
show False
proof (rule disjE)
{show "p∨q" using `p∨q` .
next
show "p⟹False"
proof -
{have "¬p" using assms..
assume "p"
with `¬p`show False..}
qed
next
show "q⟹False"
proof -
{have "¬q" using assms..
assume "q"
with `¬q`show False..}
qed}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p∨¬q" using assms .
next
show "¬p⟹¬(p∧q)"
proof -
{assume "¬p"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "p"..
with `¬p`show False..}
qed}
qed
next
show "¬q⟹¬(p∧q)"
proof -
{assume "¬q"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "q"..
with `¬q`show False..}
qed}
qed
qed

-- "Pedro Ros"
lemma ejercicio_48b:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p ∨ ¬q" using assms .
next
assume 1: "¬p"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "p" ..
show "False" using 1 2 ..
qed
next
assume 1: "¬q"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "q" ..
show "False" using 1 2 ..
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof (rule notI)
assume "p∧¬p"
hence "¬p"..
have "p" using `p∧¬p`..
with `¬p`show False..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
proof (rule notE)
show "p" using assms ..
show "¬p" using assms ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
proof (rule ccontr)
assume "¬p"
with `¬¬p` show False..
qed

-- "Pedro Ros"
lemma ejercicio_51b:
assumes "¬¬p"
shows "p"
using assms by (rule notnotD)

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
{assume "¬(p∨¬p)"
have "p"
proof (rule ccontr)
{assume "¬p"
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p⟶q)⟶p"
show "p"
proof (rule ccontr)
note `(p⟶q)⟶p`
assume "¬p"
with `(p⟶q)⟶p` have "¬(p⟶q)" by (rule mt)
{assume "p"
with `¬p` have "q" by (rule notE)}
hence "p⟶q" by (rule impI)
with `¬(p⟶q)` show False by (rule notE)
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume "p"
hence "¬¬p" by (rule notnotI)
with `¬q⟶¬p` have "¬¬q" by (rule mt)
show "q"
proof (rule ccontr)
{assume "¬q"
with `¬¬q` show False..}
qed}
qed

-- "Pedro Ros"
lemma ejercicio_54b:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus q by (rule notnotD)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
show "¬p∨p"..
show "¬p⟹p∨q"
proof -
{assume "¬p"
have "q"
proof (rule ccontr)
{assume "¬q"
with `¬p` have "¬p∧¬q"..
with assms show False..}
qed
then show "p∨q"..}
qed
show "p⟹p∨q"
proof -
{assume "p"
then show "p∨q"..}
qed
qed

-- "Pedro Ros"
lemma ejercicio_55b:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence " ¬p ∧ ¬q" by (rule ejercicio_46)
with assms show "False" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof(rule conjI)
show "p"
proof(rule ccontr)
{assume "¬p"
hence "¬p∨¬q"..
with assms show False..}
qed
show "q"
proof(rule ccontr)
{assume "¬q"
hence "¬p∨¬q"..
with assms show False..}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p∨p"..
moreover
{assume "¬p"
hence "¬p∨¬q"..}
moreover
{assume "p"
have "¬q∨q"..
moreover
{assume "¬q"
hence "¬p∨¬q"..}
moreover
{assume "q"
with `p`have "p∧q"..
with `¬(p∧q)` have "¬p∨¬q"..}
ultimately have "¬p∨¬q"..}
ultimately show "¬p∨¬q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" ..
moreover
{assume "¬p"
{assume "p"
with `¬p` have "q" ..}
hence "p⟶q" ..
hence "(p⟶q)∨(q⟶p)" ..}
moreover
{assume "p"
{assume "q"
note `p`}
hence "q⟶p"..
hence "(p⟶q)∨(q⟶p)"..}
ultimately show "(p⟶q)∨(q⟶p)" ..
qed

-- "Raúl Montes Pajuelo: Voy a añadir algunos ejercicios de examen más. Creo que es interesante tenerlos aquí resueltos"

text {* ---------------------------------------------------------------
Ejercicio 59: Examen de Septiembre del 2006. Demostrar
(p ⟶ r) ∨ (q ⟶ s) ⊢ (p ∧ q) ⟶ (r ∨ s)
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_59:
assumes "(p ⟶ r) ∨ (q ⟶ s)"
shows "(p ∧ q) ⟶ (r ∨ s)"
proof
assume "p ∧ q"
show "r ∨ s"
proof (rule disjE)
show "(p ⟶ r) ∨ (q ⟶ s)" using assms.
next
show "p ⟶ r ⟹ r ∨ s"
proof -
assume "p ⟶ r"
have "p" using `p ∧ q`..
with `p ⟶ r`have "r"..
thus "r ∨ s"..
qed
next
show "q ⟶ s ⟹ (r ∨ s)"
proof -
assume "q ⟶ s"
have "q" using `p ∧ q`..
with `q ⟶ s`have "s"..
thus "r ∨ s"..
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 60: Examen de Junio del 2005. Demostrar
p ∧ ¬(q ⟶ r) ⊢ (p ∧ q) ∧ ¬r
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_60:
assumes "p ∧ ¬(q ⟶ r)"
shows "(p ∧ q) ∧ ¬r"
proof (rule conjI)
have "p" using assms..
have "¬(q ⟶ r)" using assms..
have "q"
proof (rule ccontr)
assume "¬q"
have "q ⟶ r"
proof
assume "q"
with `¬q` have False..
thus "r"..
qed
with `¬(q ⟶ r)` show False..
qed
with `p` show "p ∧ q"..
show "¬r"
proof (rule notI)
assume "r"
have "q ⟶ r"
proof
assume "q"
show "r" using `r`.
qed
with `¬(q ⟶ r)`show False..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 61: Examen de Diciembre del 2005. Demostrar
⊢(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_61:
"(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "(p ⟶ ¬q) ∧ (p ⟶ ¬r)"
show "(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "p"
show "¬(q ∨ r)"
proof (rule notI)
assume "q ∨ r"
thus False
proof
assume "q"
hence "¬¬q" by (rule notnotI)
have "p ⟶ ¬q" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬q` `¬¬q` by (rule mt)
show False using `¬p` `p`..
next
assume "r"
hence "¬¬r" by (rule notnotI)
have "p ⟶ ¬r" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬r` `¬¬r` by (rule mt)
show False using `¬p` `p`..
qed
qed
qed
qed

end
</source>

Relación 3

2013-03-20T18:09:41Z

Mirnunolm:

<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

-- "Pedro G. Ros"
lemma ejercicio_1c:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
using assms ..

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

-- "Isabel Duarte"
lemma ejercicio_2b:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
with `q ⟶ r` show "r" ..
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

-- "Isabel Duarte"
lemma ejercicio_3b:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using assms(1,3) ..
have "q" using assms(2,3) ..
with `q ⟶ r` show "r" ..
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

lemma ejercicio_4d:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
using assms by auto

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

-- "Pedro G. Ros Reina"
lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof -
{assume 1: "q"}
show "q⟶ p" using assms(1) by (rule impI)
qed

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

-- "Pedro G. Ros"
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof -
{assume 1: "p"
hence 2: "q ⟶ p" by (rule impI)}
thus "p ⟶q⟶p" by (rule impI)
qed

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

-- "Carmen Martinez Navarro, Erlinda Menendez Perez"

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

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q⟶ (p⟶ s)"
proof
assume "q"
show "p⟶ s"
proof
assume "p"
with assms have "q⟶ r⟶ s" ..
hence "r⟶ s" using `q` ..
thus "s" using `r`..
qed
qed
qed

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

lemma ejercicio_11a:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ (q ⟶ r)"
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume 3: "p⟶ q"
show 4: "p⟶ r"
proof
assume 5: "p"
have 6: "q" using 3 5 by (rule mp)
have 7:"q⟶ r" using 1 5 by (rule mp)
show 8: "r" using 7 6 ..
qed
qed
qed

-- "Reme Sillero"

lemma ejercicio_11b:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p⟶ (q ⟶ r)` `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12a:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
have 1: "(p⟶ q)⟶ r" using assms by this
{assume 2: "p"
{assume 3: "q"
{assume 4: "p"
have 5: "q" using 3 by this}
hence 6: "p⟶ q" ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶ r" ..}
thus 9: "p⟶ (q⟶ r)" ..
qed

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

-- "Pedro G. Ros"
lemma ejercicio_13b:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_14b:
assumes "p ∧ q"
shows "p"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_15b:
assumes "p ∧ q"
shows "q"
using assms ..

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

-- "Reme Sillero"
lemma ejercicio_18a:
assumes "p ∧ q"
shows "p ⟶ q"
proof
assume "p"
show "q" using assms ..
qed

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

-- "Carmen Martinez Navarro , Erlinda Menendez Perez"

lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ (q ∧ r)"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using assms by (rule conjunct1)
have 4: "q" using 3 2 by (rule mp)
have 5: "p ⟶ r" using assms by (rule conjunct2)
have 6: "r" using 5 2 by (rule mp)
show "q ∧ r" using 4 6 by (rule conjI)
qed

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

-- "Jesús Horno Cobo"

lemma ejercicio_20:
assumes 1:"p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof -
{ assume 3: "p"
have 4: "q ∧ r" using 1 3 by (rule mp)
have 5: "q" using 4 by (rule conjunct1) }
hence 6: "p ⟶ q" by (rule impI)
{ assume 7: "p"
have 8: "q ∧ r" using 1 7 by (rule mp)
have 9: "r" using 8 by (rule conjunct2) }
hence 10: "p ⟶ r" by (rule impI)
show "(p ⟶ q) ∧ (p ⟶ r)" using 6 10 by (rule conjI)
qed

-- "Antonio Jesús Molero"
lemma ejercicio_20a:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "q" ..
qed
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "r" ..
qed
qed

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

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

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

-- "Pedro G. Ros"
lemma ejercicio_22a:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q⟶ r"
proof
assume "q"
have "p∧q" using `p` `q` ..
show "r" using assms `p∧q`..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_23a:
assumes 1:"(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume 2:"p∧q"
hence 3:"p" ..
have 4:"q" using 2 ..
hence 5: "p⟶ q" ..
show"r" using 1 5 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24a:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume 0:"p⟶ q"
show "r"
proof -
have 1: "p" using assms ..
have 2: "q" using 0 1 ..
have 3: "q⟶ r" using assms ..
show 3: "r" using 3 2 ..
qed
qed

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

-- "Pedro G. Ros Reina"
lemma ejercicio_25b:
assumes "p"
shows "p ∨ q"
using assms ..

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

-- "Pedro G. Ros Reina"
lemma ejercicio_26b:
assumes "q"
shows "p ∨ q"
using assms ..

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
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_28a:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume 1: "p∨q"
moreover
{assume "p"
hence "p∨r" by (rule disjI1)}
moreover
{assume "q"
have "r" using assms `q`..
hence "p∨r" ..}
ultimately
show "p∨r" ..
qed

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

-- "Pedro Ros"
lemma ejercicio_29a:
assumes "p ∨ p"
shows "p"
proof-
have "p∨p" using assms by this
moreover
{assume "p"
hence "p" by this}
moreover
{assume "p"
hence "p" by this}
ultimately
show "p" ..
qed

-- "Pedro Ros"
lemma ejercicio_29b:
assumes "p ∨ p"
shows "p"
using assms ..

-- "Antonio Jesús Molero"
lemma ejercicio_29c:
assumes "p ∨ p"
shows "p"
using assms
proof (rule disjE)
assume "p"
thus "p" by this
next
assume "p"
thus "p" by this
qed

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
proof -
show "p∨p" using assms ..
qed

-- "Pedro Ros"
lemma ejercicio_30b:
assumes "p"
shows "p ∨ p"
using assms ..

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

-- "Pedro G. Ros"
lemma ejercicio_31a:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have 1: "p ∨ (q ∨ r)" using assms by this
moreover
{assume "p"
hence "(p∨q)" ..
hence "(p∨q)∨r" ..}
moreover
{assume "(q∨r)"
moreover
{assume "q"
hence "(p∨q)"..
hence "(p∨q)∨r" ..}
moreover
{assume "r"
hence "(p∨q)∨r" ..}
ultimately
have "(p∨q)∨r"..}
ultimately
show "(p∨q)∨r" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms(1)
proof
assume "p∨q"
thus "p∨q∨r"
proof
assume "p"
thus "p∨q∨r" ..
next
assume "q"
hence "q∨r" ..
thus "p∨q∨r" ..
qed
next
assume "r"
hence "q∨r" ..
thus "p∨q∨r" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_33a:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms ..
have 2: "q∨r" using assms ..
moreover
{assume 3: "q"
have "(p∧q)" using 1 3 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
moreover
{assume 4: "r"
have "p∧r" using 1 4 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
ultimately
show "(p ∧ q) ∨ (p ∧ r)" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_34a:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this
moreover
{assume "(p ∧ q)"
hence "p" ..
have "q" using `p ∧ q` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
moreover
{assume "(p∧r)"
hence "p" ..
have "r" using `p ∧ r` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
ultimately
show "p ∧ (q ∨ r)" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_35a:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have 1: "p ∨ (q ∧ r)" using assms by this
moreover
{assume "p"
hence 2: "(p∨q)" ..
have 3: "(p∨r)" using `p` ..
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}
moreover
{assume 5:"(q∧r)"
hence 6: "q" ..
have 7: "r" using 5 ..
have 8: "p∨q" using 6 ..
have 9: "p∨r" using 7 ..
have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}
ultimately
show "(p ∨ q) ∧ (p ∨ r)" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p∨q" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "q"
have "p∨r" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "r"
with `q` have "q∧r"..
hence "p∨(q∧r)"..}
ultimately have "p∨(q∧r)"..}
ultimately show "p∨(q∧r)"..
qed

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

-- "Erlinda Menendez Perez , Carmen Martinez Navarro"

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume 1: "p ∨ q"
thus "r"
proof (rule disjE)
assume 2:"p"
have 3: "p ⟶ r" using assms by (rule conjunct1)
show "r" using 3 2 by (rule mp)
next
assume 5:"q"
have 6: "q ⟶ r" using assms by (rule conjunct2)
show "r" using 6 5 by (rule mp)
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof -
{assume 1: "p"
have 2:"p ∨ q" using 1 ..
have 3: "r" using assms 2 ..}
hence 4: "p⟶r" ..
{assume 5: "q"
have 6: "p ∨ q" using 5 ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶r" ..
show "(p⟶r)∧(q⟶r)" using 4 8 ..
qed

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

-- "Pedro G. Ros Reina"
lemma ejercicio_39b:
assumes "p"
shows "¬¬p"
using assms by (rule notnotI)

-- "Raúl Montes Pajuelo"

lemma ejercicio_39c:
assumes "p"
shows "¬¬p"
proof (rule notI)
assume "¬p"
show False using `¬p` assms..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
{assume 1: "p"
show "q" using assms 1 by (rule notE)}
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
{assume "¬q"
with assms show "¬p" by (rule mt) }
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
proof -
note `p∨q`
moreover
{assume "p"
hence "p" by this}
moreover
{assume "q"
with assms (2) have "p" ..}
ultimately show "p" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
note `p∨q`
moreover
{assume "p"
with assms (2) have False..
hence "q"..}
moreover
{assume "q"
hence "q" .}
ultimately show "q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof -
{assume "¬p∧¬q"
note `p∨q`
moreover
{have "¬p" using `¬p∧¬q`by (rule conjunct1)
assume "p"
with `¬p`have False by (rule notE)}
moreover
{have "¬q" using `¬p∧¬q`by (rule conjunct2)
assume "q"
with `¬q`have False by (rule notE)}
ultimately have False by (rule disjE)}
thus "¬(¬p∧¬q)" by (rule notI)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume "¬p∨¬q"
show False
proof (rule disjE)
{show "¬p∨¬q" using `¬p∨¬q`.
next
show "¬p⟹False"
proof -
{assume "¬p"
have "p" using assms..
with `¬p`show False..}
qed
next
show "¬q⟹False"
proof -
{assume "¬q"
have "q" using assms..
with `¬q`show False..}
qed}
qed
qed

--Miriam Núñez
lemma ejercicio_45b:
assumes 1:"p \<and> q"
shows "\<not>(\<not>p \<or> \<not>q)"
proof-
{assume 2:"\<not>p\<or>\<not>q"
moreover
{assume 3:" \<not>p"
have 4: "p" using 1 by (rule conjunct1)
have False using 3 4 by (rule notE)}
moreover
{assume 5: "\<not>q"
have 6: "q" using 1 by (rule conjunct2)
have False using 5 6 by (rule notE)}
ultimately have False by (rule disjE)}
thus "\<not>(\<not>p\<or>\<not>q)" by (rule notI)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
{assume "p"
hence "p∨q"..
with assms show False..}
qed
next
show "¬q"
proof (rule notI)
{assume "q"
hence "p∨q"..
with assms show False..}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
assume "p∨q"
show False
proof (rule disjE)
{show "p∨q" using `p∨q` .
next
show "p⟹False"
proof -
{have "¬p" using assms..
assume "p"
with `¬p`show False..}
qed
next
show "q⟹False"
proof -
{have "¬q" using assms..
assume "q"
with `¬q`show False..}
qed}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p∨¬q" using assms .
next
show "¬p⟹¬(p∧q)"
proof -
{assume "¬p"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "p"..
with `¬p`show False..}
qed}
qed
next
show "¬q⟹¬(p∧q)"
proof -
{assume "¬q"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "q"..
with `¬q`show False..}
qed}
qed
qed

-- "Pedro Ros"
lemma ejercicio_48b:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p ∨ ¬q" using assms .
next
assume 1: "¬p"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "p" ..
show "False" using 1 2 ..
qed
next
assume 1: "¬q"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "q" ..
show "False" using 1 2 ..
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof (rule notI)
assume "p∧¬p"
hence "¬p"..
have "p" using `p∧¬p`..
with `¬p`show False..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
proof (rule notE)
show "p" using assms ..
show "¬p" using assms ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
proof (rule ccontr)
assume "¬p"
with `¬¬p` show False..
qed

-- "Pedro Ros"
lemma ejercicio_51b:
assumes "¬¬p"
shows "p"
using assms by (rule notnotD)

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
{assume "¬(p∨¬p)"
have "p"
proof (rule ccontr)
{assume "¬p"
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p⟶q)⟶p"
show "p"
proof (rule ccontr)
note `(p⟶q)⟶p`
assume "¬p"
with `(p⟶q)⟶p` have "¬(p⟶q)" by (rule mt)
{assume "p"
with `¬p` have "q" by (rule notE)}
hence "p⟶q" by (rule impI)
with `¬(p⟶q)` show False by (rule notE)
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume "p"
hence "¬¬p" by (rule notnotI)
with `¬q⟶¬p` have "¬¬q" by (rule mt)
show "q"
proof (rule ccontr)
{assume "¬q"
with `¬¬q` show False..}
qed}
qed

-- "Pedro Ros"
lemma ejercicio_54b:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus q by (rule notnotD)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
show "¬p∨p"..
show "¬p⟹p∨q"
proof -
{assume "¬p"
have "q"
proof (rule ccontr)
{assume "¬q"
with `¬p` have "¬p∧¬q"..
with assms show False..}
qed
then show "p∨q"..}
qed
show "p⟹p∨q"
proof -
{assume "p"
then show "p∨q"..}
qed
qed

-- "Pedro Ros"
lemma ejercicio_55b:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence " ¬p ∧ ¬q" by (rule ejercicio_46)
with assms show "False" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof(rule conjI)
show "p"
proof(rule ccontr)
{assume "¬p"
hence "¬p∨¬q"..
with assms show False..}
qed
show "q"
proof(rule ccontr)
{assume "¬q"
hence "¬p∨¬q"..
with assms show False..}
qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p∨p"..
moreover
{assume "¬p"
hence "¬p∨¬q"..}
moreover
{assume "p"
have "¬q∨q"..
moreover
{assume "¬q"
hence "¬p∨¬q"..}
moreover
{assume "q"
with `p`have "p∧q"..
with `¬(p∧q)` have "¬p∨¬q"..}
ultimately have "¬p∨¬q"..}
ultimately show "¬p∨¬q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" ..
moreover
{assume "¬p"
{assume "p"
with `¬p` have "q" ..}
hence "p⟶q" ..
hence "(p⟶q)∨(q⟶p)" ..}
moreover
{assume "p"
{assume "q"
note `p`}
hence "q⟶p"..
hence "(p⟶q)∨(q⟶p)"..}
ultimately show "(p⟶q)∨(q⟶p)" ..
qed

-- "Raúl Montes Pajuelo: Voy a añadir algunos ejercicios de examen más. Creo que es interesante tenerlos aquí resueltos"

text {* ---------------------------------------------------------------
Ejercicio 59: Examen de Septiembre del 2006. Demostrar
(p ⟶ r) ∨ (q ⟶ s) ⊢ (p ∧ q) ⟶ (r ∨ s)
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_59:
assumes "(p ⟶ r) ∨ (q ⟶ s)"
shows "(p ∧ q) ⟶ (r ∨ s)"
proof
assume "p ∧ q"
show "r ∨ s"
proof (rule disjE)
show "(p ⟶ r) ∨ (q ⟶ s)" using assms.
next
show "p ⟶ r ⟹ r ∨ s"
proof -
assume "p ⟶ r"
have "p" using `p ∧ q`..
with `p ⟶ r`have "r"..
thus "r ∨ s"..
qed
next
show "q ⟶ s ⟹ (r ∨ s)"
proof -
assume "q ⟶ s"
have "q" using `p ∧ q`..
with `q ⟶ s`have "s"..
thus "r ∨ s"..
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 60: Examen de Junio del 2005. Demostrar
p ∧ ¬(q ⟶ r) ⊢ (p ∧ q) ∧ ¬r
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_60:
assumes "p ∧ ¬(q ⟶ r)"
shows "(p ∧ q) ∧ ¬r"
proof (rule conjI)
have "p" using assms..
have "¬(q ⟶ r)" using assms..
have "q"
proof (rule ccontr)
assume "¬q"
have "q ⟶ r"
proof
assume "q"
with `¬q` have False..
thus "r"..
qed
with `¬(q ⟶ r)` show False..
qed
with `p` show "p ∧ q"..
show "¬r"
proof (rule notI)
assume "r"
have "q ⟶ r"
proof
assume "q"
show "r" using `r`.
qed
with `¬(q ⟶ r)`show False..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 61: Examen de Diciembre del 2005. Demostrar
⊢(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))
------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_61:
"(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "(p ⟶ ¬q) ∧ (p ⟶ ¬r)"
show "(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "p"
show "¬(q ∨ r)"
proof (rule notI)
assume "q ∨ r"
thus False
proof
assume "q"
hence "¬¬q" by (rule notnotI)
have "p ⟶ ¬q" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬q` `¬¬q` by (rule mt)
show False using `¬p` `p`..
next
assume "r"
hence "¬¬r" by (rule notnotI)
have "p ⟶ ¬r" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬r` `¬¬r` by (rule mt)
show False using `¬p` `p`..
qed
qed
qed
qed

end
</source>

Relación 2

2013-02-23T17:44:12Z

Mirnunolm:

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

module SintaxisSemantica where

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

import Data.List

-- ---------------------------------------------------------------------
-- Gramática de fórmulas prosicionales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir los siguientes tipos de datos:
-- * SímboloProposicional para representar los símbolos de proposiciones
-- * Prop para representar las fórmulas proposicionales usando los
-- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas
-- atómicas, negaciones, conjunciones, implicaciones y equivalencias,
-- respectivamente.
-- ---------------------------------------------------------------------

type SímboloProposicional = String

data Prop = Atom SímboloProposicional
| Neg Prop
| Conj Prop Prop
| Disj Prop Prop
| Impl Prop Prop
| Equi Prop Prop
deriving (Eq,Ord)

instance Show Prop where
show (Atom p) = p
show (Neg p) = "no " ++ show p
show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir las siguientes fórmulas proposicionales
-- atómicas: p, p1, p2, q, r, s, t y u.
-- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop
p = Atom "p"
p1 = Atom "p1"
p2 = Atom "p2"
q = Atom "q"
r = Atom "r"
s = Atom "s"
t = Atom "t"
u = Atom "u"

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- no :: Prop -> Prop
-- tal que (no f) es la negación de f.
-- ---------------------------------------------------------------------

no :: Prop -> Prop
no = Neg

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir los siguientes operadores
-- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
-- tales que
-- f /\ g es la conjunción de f y g
-- f \/ g es la disyunción de f y g
-- f --> g es la implicación de f a g
-- f <--> g es la equivalencia entre f y g
-- ---------------------------------------------------------------------

infixr 5 \/
infixr 4 /\
infixr 3 -->
infixr 2 <-->
(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
(/\) = Conj
(\/) = Disj
(-->) = Impl
(<-->) = Equi

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una fórmula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- símbolosPropFórm :: Prop -> [Prop]
-- tal que (símbolosPropFórm f) es el conjunto formado por todos los
-- símbolos proposicionales que aparecen en f. Por ejemplo,
-- símbolosPropFórm (p /\ q --> p) ==> [p,q]
-- ---------------------------------------------------------------------

-- Antonio Molero

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

-- ---------------------------------------------------------------------
-- Interpretaciones --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir el tipo de datos Interpretación para
-- representar las interpretaciones como listas de fórmulas atómicas.
-- ---------------------------------------------------------------------

type Interpretación = [Prop]

-- ---------------------------------------------------------------------
-- Significado de una fórmula en una interpretación --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- significado :: Prop -> Interpretación -> Bool
-- tal que (significado f i) es el significado de f en i. Por ejemplo,
-- significado ((p \/ q) /\ ((no q) \/ r)) [r] ==> False
-- significado ((p \/ q) /\ ((no q) \/ r)) [p,r] ==> True
-- ---------------------------------------------------------------------
-- Pedro G. Ros
significado :: Prop -> Interpretacion -> Bool
significado (Neg(Atom p)) a = elem (no (Atom p)) a
significado (Atom p) a = elem (Atom p) a
significado (Neg p) a = not (significado p a)
significado (Conj p q) a= (significado p a)&& (significado q a)
significado (Disj p q) a =(significado p a)|| (significado q a)
significado (Impl p q) a = if (significado p a) then (significado q a)==
True else True
significado (Equi p q) a = (significado (Impl p q) a )&&(significado (Impl q p)) a

-- ---------------------------------------------------------------------
-- Interpretaciones de una fórmula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- subconjuntos :: [a] -> [[a]]
-- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por
-- ejmplo,
-- subconjuntos "abc" ==> ["abc","ab","ac","a","bc","b","c",""]
-- ---------------------------------------------------------------------

-- Reme Sillero

subconjuntos :: [a] -> [[a]]
subconjuntos [] = [[]]
subconjuntos (x:xs) = [x:ys | ys <- subconjuntos xs] ++ subconjuntos xs

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesFórm :: Prop -> [Interpretación]
-- tal que (interpretacionesFórm f) es la lista de todas las
-- interpretaciones de f. Por ejemplo,
-- interpretacionesFórm (p /\ q --> p) ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

-- Reme Sillero

interpretacionesForm :: Prop -> [Interpretación]
interpretacionesForm p = subconjuntos (simbolosPropForm p)

-- ---------------------------------------------------------------------
-- Modelos de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloFórmula :: Interpretación -> Prop -> Bool
-- tal que (esModeloFórmula i f) se verifica si i es un modelo de f. Por
-- ejemplo,
-- esModeloFórmula [r] ((p \/ q) /\ ((no q) \/ r)) ==> False
-- esModeloFórmula [p,r] ((p \/ q) /\ ((no q) \/ r)) ==> True
-- ---------------------------------------------------------------------
--Pedro G. Ros
esModeloFórmula :: Interpretación -> Prop -> Bool
esModeloFórmula i (Conj a b)= significado (Conj a b) i
esModeloFórmula i (Disj a b) = esModeloFórmula i (Conj a b)
esModeloFórmula i (Impl a b)=if a/= b then esModeloFórmula i (Conj a b) else True
esModeloFórmula i (Equi a b)=(esModeloFórmula i (Impl a b))&&(esModeloFórmula i (Impl b a))
esModeloFórmula i (Neg b)=not(esModeloFórmula i b)
esModeloFórmula i p = significado p i

-- Miriam Núñez-Romero.
esModeloFormula2 :: InterpretaciÃ³n -> Prop -> Bool
esModeloFormula2 i f | (significado f i) ==True =True
|otherwise=False
-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- modelosFórmula :: Prop -> [Interpretación]
-- tal que (modelosFórmula f) es la lista de todas las interpretaciones
-- de f que son modelo de F. Por ejemplo,
-- modelosFórmula ((p \/ q) /\ ((no q) \/ r))
-- ==> [[p,q,r],[p,r],[p],[q,r]]
-- ---------------------------------------------------------------------
--Pedro G. Ros
modelosFórmula :: Prop -> [Interpretación]
modelosFórmula f = [x|x<-(interpretacionesForm f),esModeloFórmula x f]

-- ---------------------------------------------------------------------
-- Fórmulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

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

-- Reme Sillero

esVálida :: Prop -> Bool
esVálida f = modelosFormula f == interpretacionesForm f

--Pedro G. Ros
--Ser válida es ser tautología, luego la definición anterior no es correcta, sería:
esVálida f = elem [] (modelosFormula f)
-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esInsatisfacible :: Prop -> Bool
-- tal que (esInsatisfacible f) se verifica si f es insatisfacible. Por
-- ejemplo,
-- esInsatisfacible (p /\ (no p)) ==> True
-- esInsatisfacible ((p --> q) /\ (q --> r)) ==> False
-- ---------------------------------------------------------------------

-- Reme Sillero

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

--Pedro G. Ros
esInsatisfacible2 :: Prop-> Bool
esInsatisfacible2 f = esVálida (no f)
-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- esSatisfacible :: Prop -> Bool
-- tal que (esSatisfacible f) se verifica si f es satisfacible. Por
-- ejemplo,
-- esSatisfacible (p /\ (no p)) ==> False
-- esSatisfacible ((p --> q) /\ (q --> r)) ==> True
-- ---------------------------------------------------------------------
-- Reme Sillero

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

-- Isabel Duarte
esSatisfacible2 :: Prop -> Bool
esSatisfacible2 f = not (esInsatisfacible f)

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- uniónGeneral :: Eq a => [[a]] -> [a]
-- tal que (uniónGeneral x) es la unión de los conjuntos de la lista de
-- conjuntos x. Por ejemplo,
-- uniónGeneral [] ==> []
-- uniónGeneral [[1]] ==> [1]
-- uniónGeneral [[1],[1,2],[2,3]] ==> [1,2,3]
-- ---------------------------------------------------------------------

-- Antonio Molero

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

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- símbolosPropConj :: [Prop] -> [Prop]
-- tal que (símbolosPropConj s) es el conjunto de los símbolos
-- proposiciones de s. Por ejemplo,
-- símbolosPropConj [p /\ q --> r, p --> s] ==> [p,q,r,s]
-- ---------------------------------------------------------------------

-- Antonio Molero

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = unionGeneral [simbolosPropForm x|x<-s]

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- interpretacionesConjunto :: [Prop] -> [Interpretación]
-- tal que (interpretacionesConjunto s) es la lista de las
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjunto [p --> q, q --> r]
-- ==> [[p,q,r],[p,q],[p,r],[p],[q,r],[q],[r],[]]
-- ---------------------------------------------------------------------

-- Reme Sillero

interpretacionesConjunto :: [Prop] -> [Interpretación]
interpretacionesConjunto s = subconjuntos (simbolosPropConj s)

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esModeloConjunto :: Interpretación -> [Prop] -> Bool
-- tal que (esModeloConjunto i s) se verifica si i es modelo de s. Por
-- ejemplo,
-- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), q --> r]
-- ==> True
-- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), r --> q]
-- ==> False
-- ---------------------------------------------------------------------

--Isabel Duarte
esModeloConjunto :: Interpretación -> [Prop] -> Bool
esModeloConjunto i s = and [ esModeloFórmula i x | x <- s]

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- modelosConjunto :: [Prop] -> [Interpretación]
-- tal que (modelosConjunto s) es la lista de modelos del conjunto
-- s. Por ejemplo,
-- modelosConjunto [(p \/ q) /\ ((no q) \/ r), q --> r]
-- ==> [[p,q,r],[p,r],[p],[q,r]]
-- modelosConjunto [(p \/ q) /\ ((no q) \/ r), r --> q]
-- ==> [[p,q,r],[p],[q,r]]
-- ---------------------------------------------------------------------

--Isabel Duarte
modelosConjunto :: [Prop] -> [Interpretación]
modelosConjunto s = [ x | x <- (interpretacionesConjunto s), esModeloConjunto x s]

-- ---------------------------------------------------------------------
-- Conjuntos consistentes e inconsistentes de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConsistente :: [Prop] -> Bool
-- tal que (esConsistente s) se verifica si s es consistente. Por
-- ejemplo,
-- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r]
-- ==> True
-- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r]
-- ==> False
-- ---------------------------------------------------------------------

--Jesús Horno Cobo
esConsistente :: [Prop] -> Bool
esConsistente s = modelosConjunto s /= []

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esInconsistente :: [Prop] -> Bool
-- tal que (esInconsistente s) se verifica si s es inconsistente. Por
-- ejemplo,
-- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r]
-- ==> False
-- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r]
-- ==> True
-- ---------------------------------------------------------------------

--Jesús Horno Cobo
esInconsistente :: [Prop] -> Bool
esInconsistente s = modelosConjunto s == []

-- ---------------------------------------------------------------------
-- Consecuencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuencia :: [Prop] -> Prop -> Bool
-- tal que (esConsecuencia s f) se verifica si f es consecuencia de
-- s. Por ejemplo,
-- esConsecuencia [p --> q, q --> r] (p --> r) ==> True
-- esConsecuencia [p] (p /\ q) ==> False
-- ---------------------------------------------------------------------

--Jesús Horno Cobo
esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = esInconsistente ((no f):s)
</source>