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

Ejercicio 3

2013-04-29T14:15:05Z

Jeshorcob:

== 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:
* 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:
* 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:
* Ejercicio 26: José María Contreras Beltrán
* Ejercicio 27: Isabel Duarte Tosso
* Ejercicio 28:

Relación 2

2013-04-24T11:06:52Z

Jeshorcob:

<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 Interpretacion = [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 -> [Interpretacion]
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
esModeloFormula :: Interpretacion ->Prop -> Bool
esModeloFormula = \f-> \i -> (significado i f)

-- Miriam Núñez-Romero.
esModeloFormula2 :: Interpretacion -> 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
modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = [x|x<-(interpretacionesForm f),esModeloFormula2 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

esValida :: Prop -> Bool
esValida 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:
esValida2 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 = esValida (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] -> [Interpretacion]
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 :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = and [ esModeloFormula i x | x <- s]

--Pedro G. Ros
esModeloConjunto2 :: Interpretacion-> [Prop] -> Bool
esModeloConjunto2 i [] = True
esModeloConjunto2 i (x:xs) = (esModeloFormula2 i x)&&(esModeloConjunto2 i xs)

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

Ejercicio 2

2013-04-16T10:43:09Z

Jeshorcob:

== 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: Salvador Joaquín Franco Peña
* Ejercicio 4:
* Ejercicio 5: Concepción García Vidal
* Ejercicio 6:
* Ejercicio 7: Jesús Horno Cobo
* 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-13T11:54:41Z

Jeshorcob:

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

theory R3
imports Main
begin

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

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

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

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

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

section {* Implicaciones *}

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

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

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

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

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

-- "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))"
lemma ejercicio_11:
shows "(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

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

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

section {* Conjunciones *}

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

-- "Pedro G. Ros Reina"

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

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

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

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

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

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

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

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

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

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

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
-- "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

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

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
proof -
show "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)
------------------------------------------------------------------ *}

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

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

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

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

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

section {* Negaciones *}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma ejercicio_52:
"p ∨ ¬p"
oops

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

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

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

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

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

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

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

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

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

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

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

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

end
</source>

Relación 3

2013-03-08T14:56:02Z

Jeshorcob:

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

theory R3
imports Main
begin

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

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

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

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

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

section {* Implicaciones *}

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

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

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

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

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

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

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

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

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

section {* Conjunciones *}

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

-- "Pedro G. Ros Reina"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

section {* Disyunciones *}

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

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

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

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

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

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

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

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

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

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

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

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "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)
------------------------------------------------------------------ *}

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

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

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

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

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

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

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

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

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

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

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

section {* Negaciones *}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma ejercicio_52:
"p ∨ ¬p"
oops

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

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

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

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

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

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

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

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

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

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

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

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

end
</source>

Relación 3

2013-03-08T14:54:02Z

Jeshorcob:

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

theory R3
imports Main
begin

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

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

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

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

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

section {* Implicaciones *}

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

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

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

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

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

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

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

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

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

section {* Conjunciones *}

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

-- "Pedro G. Ros Reina"

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

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

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

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

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

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

--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 "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof -
{ assume 3: "p"
have 4: "q \<and> r" using 1 3 by (rule mp)
have 5: "q" using 4 by (rule conjunct1) }
hence 6: "p \<longrightarrow> q" by (rule impI)
{ assume 7: "p"
have 8: "q \<and> r" using 1 7 by (rule mp)
have 9: "r" using 8 by (rule conjunct2) }
hence 10: "p \<longrightarrow> r" by (rule impI)
show "(p \<longrightarrow> q) \<and> (p \<longrightarrow> r)" using 6 10 by (rule conjI)
qed

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

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

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

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

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

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

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

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

section {* Disyunciones *}

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

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

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

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

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

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

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

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

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

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

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

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "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)
------------------------------------------------------------------ *}

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

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

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

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

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

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

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

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

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

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

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

section {* Negaciones *}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma ejercicio_52:
"p ∨ ¬p"
oops

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

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

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

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

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

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

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

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

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

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

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

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

end
</source>

Relación 2

2013-02-22T17:25:39Z

Jeshorcob:

<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 (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 (Atom p) = significado (Atom p) i
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)=esModeloFórmula i (Conj a b)
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)

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

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

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

Relación 2

2013-02-22T17:02:43Z

Jeshorcob:

<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 (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 (Atom p) = significado (Atom p) i
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)=esModeloFórmula i (Conj a b)
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)

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

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

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

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = undefined
</source>