Problema 1 - Historial de revisiones

Marsilden: /* Soluciones colaborativas */

2013-02-23T12:05:03Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T12:02:05Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T12:00:27Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T11:50:52Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T11:50:15Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T11:48:55Z

‎Soluciones colaborativas

Marsilden: /* Soluciones colaborativas */

2013-02-23T11:47:02Z

‎Soluciones colaborativas

Pedrosrei: /* Soluciones colaborativas */

2013-02-20T17:42:18Z

‎Soluciones colaborativas

Pedrosrei: /* Soluciones colaborativas */

2013-02-20T17:36:33Z

‎Soluciones colaborativas

Pedrosrei: /* Soluciones colaborativas */

2013-02-20T17:35:53Z

‎Soluciones colaborativas

← Revisión anterior		Revisión del 12:05 23 feb 2013
Línea 65:		Línea 65:

	-}		-}
		+
		+
		+

	-- Reme Sillero		-- Reme Sillero

@@ Línea 67: / Línea 67: @@
 -- Reme Sillero
 -- Mis definiciones de número de variables y de profundidad son prácticamente iguales a las definidas por mi compañero pero he añadido
 -- constructores que pienso que hacen falta.
@@ Línea 73: / Línea 75: @@
 module SintaxisSemantica where
 import Data.List
 type SimboloProposicional = String
 data Prop = Atom SimboloProposicional
            | Neg Prop
@@ Línea 86: / Línea 91: @@
            deriving (Eq,Ord)
 instance Show Prop where
      show (Atom p)   = p
@@ Línea 93: / Línea 99: @@
      show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
      show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"
 p, p1, p2, q, r, s, t, u :: Prop
@@ Línea 103: / Línea 110: @@
 t  = Atom "t"
 u  = Atom "u"
 no :: Prop -> Prop
 no = Neg
 infixr 5 \/
@@ Línea 116: / Línea 125: @@
 (-->)  = Impl
 (<-->) = Equi
 -- Pasamos a definir las funciones:
 --1.
 n_variables :: Prop -> Integer
 n_variables (Atom p)   = 1
@@ Línea 130: / Línea 142: @@
 --*SintaxisSemantica> n_variables (p <--> (p \/ q ))
 --3
 --2.
 profundidad :: Prop -> Integer
 profundidad (Atom p)   = 0

← Revisión anterior		Revisión del 12:00 23 feb 2013
Línea 65:		Línea 65:

	-}		-}
		+
		+	-- Reme Sillero
		+	-- Mis definiciones de número de variables y de profundidad son prácticamente iguales a las definidas por mi compañero pero he añadido
		+	-- constructores que pienso que hacen falta.
		+
		+	-- Primero definimos todo lo relativo a tipo y a representación:
		+
		+	module SintaxisSemantica where
		+
		+	import Data.List
		+
		+	type SimboloProposicional = String
		+
		+	data Prop = Atom SimboloProposicional
		+	\| 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 ++ ")"
		+
		+	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"
		+
		+	no :: Prop -> Prop
		+	no = Neg
		+
		+	infixr 5 \/
		+	infixr 4 /\
		+	infixr 3 -->
		+	infixr 2 <-->
		+	(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
		+	(/\) = Conj
		+	(\/) = Disj
		+	(-->) = Impl
		+	(<-->) = Equi
		+
		+	-- Pasamos a definir las funciones:
		+
		+	--1.
		+	n_variables :: Prop -> Integer
		+	n_variables (Atom p) = 1
		+	n_variables (Neg p) = n_variables p
		+	n_variables (Conj p q) = n_variables p + n_variables q
		+	n_variables (Disj p q) = n_variables p + n_variables q
		+	n_variables (Impl p q) = n_variables p + n_variables q
		+	n_variables (Equi p q) = n_variables p + n_variables q
		+
		+	--*SintaxisSemantica> n_variables (p <--> (p \/ q ))
		+	--3
		+
		+	--2.
		+	profundidad :: Prop -> Integer
		+	profundidad (Atom p) = 0
		+	profundidad (Neg p) = 1 + profundidad p
		+	profundidad (Conj p q) = 1 + profundidad p + profundidad q
		+	profundidad (Disj p q) = 1 + profundidad p + profundidad q
		+	profundidad (Impl p q) = 1 + profundidad p + profundidad q
		+	profundidad (Equi p q) = 1 + profundidad p + profundidad q
		+
		+	--*SintaxisSemantica> profundidad (p --> (p /\ q ))
		+	--2
		+
		+
	</source>		</source>

← Revisión anterior		Revisión del 11:50 23 feb 2013
Línea 66:		Línea 66:
	-}		-}
	</source>		</source>
−
−
−
−
−
−	~~-- Reme Sillero~~
−
−	~~-- Mi definición de número de variables y de profundidad es prácticamente igual a la definida por mi compañero, pero he añadido más~~
−	~~-- constructores que pienso que hacen falta.~~
−
−	~~-- Primero definimos todo lo necesario en cuanto a tipo y representación:~~
−
−	~~--import Data.List~~
−
−	~~--type SimboloProposicional = String~~
−
−	~~--data Prop = Atom SimboloProposicional~~
−	~~-- \| Neg Prop~~
−	~~-- \| Conj Prop Prop~~
−	~~-- \| Disj Prop Prop~~
−	~~-- \| Impl Prop Prop~~
−	~~-- \| Equi Prop Prop~~
−	~~-- deriving (Eq,Ord)~~
−
−
−
−
−	~~-- Pasamos a definir las dos funciones pedidas:~~
−
−	~~--1.~~
−
−	~~--n_variables :: Prop -> Integer~~
−	~~--n_variables (Atom p) = 1~~
−	~~--n_variables (Neg p) = n_variables p~~
−	~~--n_variables (Conj p q) = n_variables p + n_variables q~~
−	~~--n_variables (Disj p q) = n_variables p + n_variables q~~
−	~~--n_variables (Impl p q) = n_variables p + n_variables q~~
−	~~--n_variables (Equi p q) = n_variables p + n_variables q~~
−
−
−	~~-- *SintaxisSemantica> n_variables (p <--> (p \/ q ))~~
−	~~-- 3~~
−
−
−	~~--2.~~
−
−	~~--profundidad :: Prop -> Integer~~
−	~~--profundidad (Atom p) = 0~~
−	~~--profundidad (Neg p) = 1 + profundidad p~~
−	~~--profundidad (Conj p q) = 1 + profundidad p + profundidad q~~
−	~~--profundidad (Disj p q) = 1 + profundidad p + profundidad q~~
−	~~--profundidad (Impl p q) = 1 + profundidad p + profundidad q~~
−	~~--profundidad (Equi p q) = 1 + profundidad p + profundidad q~~
−
−	~~-- *SintaxisSemantica> profundidad (p --> (p \/ q ))~~
−	~~-- 2~~

@@ Línea 78: / Línea 78: @@
 -- Primero definimos todo lo necesario en cuanto a tipo y representación:
-import Data.List
+--import Data.List
-type SimboloProposicional = String
+--type SimboloProposicional = String
-data Prop = Atom SimboloProposicional
+--data Prop = Atom SimboloProposicional
-          | Neg Prop
+--          | Neg Prop
-          | Conj Prop Prop
+--          | Conj Prop Prop
-          | Disj Prop Prop
+--          | Disj Prop Prop
-          | Impl Prop Prop
+--          | Impl Prop Prop
-          | Equi Prop Prop
+--          | Equi Prop Prop
-          deriving (Eq,Ord)
+--          deriving (Eq,Ord)
@@ Línea 97: / Línea 97: @@
 --1.
-n_variables :: Prop -> Integer
+--n_variables :: Prop -> Integer
-n_variables (Atom p)   = 1
+--n_variables (Atom p)   = 1
-n_variables (Neg p)    = n_variables p
+--n_variables (Neg p)    = n_variables p
-n_variables (Conj p q) = n_variables p + n_variables q
+--n_variables (Conj p q) = n_variables p + n_variables q
-n_variables (Disj p q) = n_variables p + n_variables q
+--n_variables (Disj p q) = n_variables p + n_variables q
-n_variables (Impl p q) = n_variables p + n_variables q
+--n_variables (Impl p q) = n_variables p + n_variables q
-n_variables (Equi p q) = n_variables p + n_variables q
+--n_variables (Equi p q) = n_variables p + n_variables q
@@ Línea 112: / Línea 112: @@
 --2.
-profundidad :: Prop -> Integer
+--profundidad :: Prop -> Integer
-profundidad (Atom p)   = 0
+--profundidad (Atom p)   = 0
-profundidad (Neg p)    = 1 + profundidad p
+--profundidad (Neg p)    = 1 + profundidad p
-profundidad (Conj p q) = 1 + profundidad p + profundidad q
+--profundidad (Conj p q) = 1 + profundidad p + profundidad q
-profundidad (Disj p q) = 1 + profundidad p + profundidad q
+--profundidad (Disj p q) = 1 + profundidad p + profundidad q
-profundidad (Impl p q) = 1 + profundidad p + profundidad q
+--profundidad (Impl p q) = 1 + profundidad p + profundidad q
-profundidad (Equi p q) = 1 + profundidad p + profundidad q
+--profundidad (Equi p q) = 1 + profundidad p + profundidad q
 -- *SintaxisSemantica> profundidad (p --> (p \/ q ))
 -- 2

← Revisión anterior		Revisión del 11:48 23 feb 2013
Línea 90:		Línea 90:
	deriving (Eq,Ord)		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 ++ ")"~~

−	~~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"~~
−
−	~~no :: Prop -> Prop~~
−	~~no = Neg~~
−
−	~~infixr 5 \/~~
−	~~infixr 4 /\~~
−	~~infixr 3 -->~~
−	~~infixr 2 <-->~~
−	~~(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop~~
−	~~(/\) = Conj~~
−	~~(\/) = Disj~~
−	~~(-->) = Impl~~
−	~~(<-->) = Equi~~

← Revisión anterior		Revisión del 11:47 23 feb 2013
Línea 66:		Línea 66:
	-}		-}
	</source>		</source>
		+
		+
		+
		+
		+
		+	-- Reme Sillero
		+
		+	-- Mi definición de número de variables y de profundidad es prácticamente igual a la definida por mi compañero, pero he añadido más
		+	-- constructores que pienso que hacen falta.
		+
		+	-- Primero definimos todo lo necesario en cuanto a tipo y representación:
		+
		+	import Data.List
		+
		+	type SimboloProposicional = String
		+
		+	data Prop = Atom SimboloProposicional
		+	\| 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 ++ ")"
		+
		+	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"
		+
		+	no :: Prop -> Prop
		+	no = Neg
		+
		+	infixr 5 \/
		+	infixr 4 /\
		+	infixr 3 -->
		+	infixr 2 <-->
		+	(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
		+	(/\) = Conj
		+	(\/) = Disj
		+	(-->) = Impl
		+	(<-->) = Equi
		+
		+
		+	-- Pasamos a definir las dos funciones pedidas:
		+
		+	--1.
		+
		+	n_variables :: Prop -> Integer
		+	n_variables (Atom p) = 1
		+	n_variables (Neg p) = n_variables p
		+	n_variables (Conj p q) = n_variables p + n_variables q
		+	n_variables (Disj p q) = n_variables p + n_variables q
		+	n_variables (Impl p q) = n_variables p + n_variables q
		+	n_variables (Equi p q) = n_variables p + n_variables q
		+
		+
		+	-- *SintaxisSemantica> n_variables (p <--> (p \/ q ))
		+	-- 3
		+
		+
		+	--2.
		+
		+	profundidad :: Prop -> Integer
		+	profundidad (Atom p) = 0
		+	profundidad (Neg p) = 1 + profundidad p
		+	profundidad (Conj p q) = 1 + profundidad p + profundidad q
		+	profundidad (Disj p q) = 1 + profundidad p + profundidad q
		+	profundidad (Impl p q) = 1 + profundidad p + profundidad q
		+	profundidad (Equi p q) = 1 + profundidad p + profundidad q
		+
		+	-- *SintaxisSemantica> profundidad (p --> (p \/ q ))
		+	-- 2

@@ Línea 35: / Línea 35: @@
 prof (Vari a) = 0
 prof (Impl a b) = 1 + (prof a) + (prof b)
-prof (Nega b) = (prof b)
+prof (Nega b) = 1+ (prof b)
 prof (Conj a b) = 1+ (prof a) + (prof b)

@@ Línea 26: / Línea 26: @@
 nv (Vari a) = 1
 nv (Impl a b) = (nv a) + (nv b)
-nv (Nega p) = 1 + (nv p)
+nv (Nega p) = (nv p)
 nv (Conj c d)= (nv c) + (nv d)
@@ Línea 48: / Línea 48: @@
 Supongamos cierta la hipótesis para m y n dos proposiciones, y pongamos los casos:
-nv (Nega m) = 1 + (nv m) <= 1+ 2^(prof m)
+nv (Nega m) = (nv m) <= 1+ 2^(prof m)
-y obviamente: prof (Nega m) = 1+ (prof m)<= 1+ 2^(prof m)
+y obviamente: prof (Nega m) = (prof m)<=  2^(prof m)
 Ya que estamos practicando la inducción haré que