Lógica Matemática y fundamentos (2015-16) - Contribuciones del usuario [es]

R16 sol

2016-05-11T09:57:50Z

Mjoseh: Página creada con '=== Relación 16: Resolución en Lógica de primer orden === ---- '''Ejercicio 1.''' Se consideran las siguientes fórmulas: reflexiva: ∀x R(x,x) simétrica: ∀x ∀y (...'

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)

simétrica: ∀x ∀y (R(x,y) → R(y,x))

transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))

notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un
padre rico, entonces existe una persona rica que tiene un abuelo rico.
Usar la relación R(x) para representar que x es rico, y la función p(x) para
representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero
que le impida el paso. A algunas personas motorizadas que intentan entrar en un
país le impiden el paso únicamente personas motorizadas. Ninguna persona
motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.
Las premisas pueden formalizarse por:
1. ∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
2. ∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
3. ∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula
∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))), P(a, f (a)) ∧ P( f (b), b)}

En el caso de que no lo sea, construir a partir de la resolución un
modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Relación 16

2016-05-11T09:57:31Z

Mjoseh: Protegió «Relación 16» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Relación 16

2016-05-11T09:57:19Z

Mjoseh:

Relación 16

2016-05-11T09:56:47Z

Mjoseh:

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un
padre rico, entonces existe una persona rica que tiene un abuelo rico.
Usar la relación R(x) para representar que x es rico, y la función p(x) para
representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero
que le impida el paso. A algunas personas motorizadas que intentan entrar en un
país le impiden el paso únicamente personas motorizadas. Ninguna persona
motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.
Las premisas pueden formalizarse por:
1. ∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
2. ∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
3. ∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula
∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),
P(a, f (a)) ∧ P( f (b), b)}

En el caso de que no lo sea, construir a partir de la resolución un
modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Relación 16

2016-05-11T09:55:21Z

Mjoseh: Página creada con ' === Relación 16: Resolución en Lógica de primer orden === ---- '''Ejercicio 1.''' Se consideran las siguientes fórmulas: reflexiva: ∀x R(x,x) simétrica: ∀x ∀y (...'

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un
padre rico, entonces existe una persona rica que tiene un abuelo rico.
Usar la relación R(x) para representar que x es rico, y la función p(x) para
representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes
inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes
inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para
representar que x es un estudiante inteligente y Q(x) para representar
que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando
una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos
dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos
elementos como máximo.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente
dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente
tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero
que le impida el paso. A algunas personas motorizadas que intentan entrar en un
país le impiden el paso únicamente personas motorizadas. Ninguna persona
motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.
Las premisas pueden formalizarse por:
1. ∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
2. ∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
3. ∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula
∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),
P(a, f (a)) ∧ P( f (b), b)}

En el caso de que no lo sea, construir a partir de la resolución un
modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R15 sol

2016-05-11T09:54:51Z

Mjoseh: Página creada con ' === Relación 15: Ejercicios de Lógica proposicional === ---- '''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide: * Pr...'

=== Relación 15: Ejercicios de Lógica proposicional ===

----
'''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide:
* Probar que A ⊧ B, mediante resolución proposicional.
* Describir, razonadamente, todos los modelos de A y, a continuación, probar nuevamente que A ⊧ B, utilizando la definición de consecuencia lógica.
* ¿Es ¬B → ¬A una tautología?

----

'''Solución:'''

----
'''Ejercicio 2.''' Consideremos la fórmula proposicional A : (r → p) ∧ (¬r → q ∨ s) → p ∨ q ∨ s
y el conjunto de fórmulas U = {r ⇔ p ∨ q, s → p, ¬s ∧ ¬r → s ∨ t}.
* Probar, mediante tableros semánticos, que A es una tautología.
* Probar, razonadamente, que U es consistente, mostrando para ello un modelo de U.
* Probar, mediante resolución, que U ⊧ ¬p → (q ∨ t).
* Sea B la fórmula anterior (¬p → (q ∨ t)). ¿Podemos eliminar alguna fórmula de U de manera que la fórmula B sea consecuencia lógica del conjunto de fórmulas restante?

----

'''Solución:'''

Relación 15

2016-05-11T09:54:28Z

Mjoseh: Protegió «Relación 15» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Relación 15

2016-05-11T09:54:16Z

Mjoseh:

Relación 15

2016-05-11T09:53:53Z

=== Relación 15: Ejercicios de Lógica proposicional ===

----
'''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide:
* Probar que A ⊧ B, mediante resolución proposicional.
* Describir, razonadamente, todos los modelos de A y, a continuación, probar nuevamente
que A ⊧ B, utilizando la definición de consecuencia lógica.
* ¿Es ¬B → ¬A una tautología?

----

'''Solución:'''

----
'''Ejercicio 2.''' Consideremos la fórmula proposicional A : (r → p) ∧ (¬r → q ∨ s) → p ∨ q ∨ s
y el conjunto de fórmulas U = {r ⇔ p ∨ q, s → p, ¬s ∧ ¬r → s ∨ t}.
* Probar, mediante tableros semánticos, que A es una tautología.
* Probar, razonadamente, que U es consistente, mostrando para ello un modelo de U.
* Probar, mediante resolución, que U ⊧ ¬p → (q ∨ t).
* Sea B la fórmula anterior (¬p → (q ∨ t)). ¿Podemos eliminar alguna fórmula de U de
manera que la fórmula B sea consecuencia lógica del conjunto de fórmulas restante?

----

'''Solución:'''

Lógica matemática y fundamentos (2015-16)

2016-05-11T09:53:20Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 11 |Solución colaborativa]] y [[R11 sol | Una solución ]]).
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 12 |Solución colaborativa]] y [[R12 sol | Una solución ]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 14 |Solución colaborativa]] y [[R14 sol | Una solución ]]).
* '''Relación 15''': Ejercicios de Lógica proposicional. ([[Relación 15 |Solución colaborativa]] y [[R15 sol | Una solución ]]).
* '''Relación 16''': Resolución en Lógica de primer orden. ([[Relación 16 |Solución colaborativa]] y [[R16 sol | Una solución ]]).

R14 sol

2016-05-10T12:34:46Z

Mjoseh: Página creada con '<source lang ="haskell"> -- ResolucionProposicional.hs -- Resolución proposicional. -- --------------------------------------------------------------------- module ResolucionP...'

<source lang ="haskell">
-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Clausula -> Clausula -> Literal -> Clausula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
-- resolvente [no p,q] [no q,r] q ==> [no p,r]
-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]
-- resolvente [no p,q] [no p,no q] q ==> [no p]
-- ---------------------------------------------------------------------

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 l =
union (delete l c1) (delete (complementario l) c2)

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Clausula -> Clausula -> [Clausula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 =
[resolvente c1 c2 l | l <- c1, (complementario l) `elem` c2]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautologia :: Clausula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautologia [p, q, no p] ==> True
-- esTautologia [p, q, no r] ==> False
-- esTautologia [] ==> False
-- ---------------------------------------------------------------------

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

esTautologia2 :: Clausula -> Bool
esTautologia2 c =
or [elem (complementario f) c | f <- c]

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

eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias s =
[c | c <- s, not (esTautologia c)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolucion :: [Clausula] -> Bool
-- tal que (esInconsistentePorResolucion s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolucion [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolucion [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

esInconsistentePorResolucion :: [Clausula] -> Bool
esInconsistentePorResolucion s =
esInconsistentePorResolucion' s []

esInconsistentePorResolucion' :: [Clausula] -> [Clausula] -> Bool
esInconsistentePorResolucion' soporte usables
| null soporte = False
| elem [] soporte = True
| otherwise =
esInconsistentePorResolucion' soporte' usables'
where actual = head soporte
usables' = union [actual] usables
soporte' = union (tail soporte)
[c
| c <- resolventesClausulaConjunto
actual
usables'
, not (esTautologia c)
, notElem c soporte
, notElem c usables']

-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------

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

esValidaPorResolucion :: Prop -> Bool
esValidaPorResolucion f =
esInconsistentePorResolucion
(eliminaTautologias (clausulas (Neg f)))

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolucion s f =
esInconsistentePorResolucion
(eliminaTautologias (clausulasConjunto ((Neg f):s)))

</source>

R12 sol

2016-05-10T12:34:03Z

Mjoseh: Página creada con '<source lang ="haskell"> -- Clausulas.hs -- Cláusulas. -- --------------------------------------------------------------------- module Clausulas where -- --------------------...'

<source lang ="haskell">
-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------

module Clausulas where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import FormasNormales
import Data.List

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Clausula como una lista de
-- literales.
-- ---------------------------------------------------------------------

type Clausula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- clausula :: Prop -> Clausula
-- tal que (clausula f) es la clausula de la fórmula-clausal f. Por
-- ejemplo,
-- clausula p ==> [p]
-- clausula (no p) ==> [no p]
-- clausula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- clausulasFNC :: Prop -> [Clausula]
-- tal que (clausulasFNC f) es el conjunto de clausulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- clausulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- clausulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------

clausulasFNC :: Prop -> [Clausula]
clausulasFNC (Conj f g) =
(clausulasFNC f) `union` (clausulasFNC g)
clausulasFNC f =
[clausula f]

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- clausulas :: Prop -> [Clausula]
-- tal que (clausulas f) es un conjunto de clausulas equivalente a
-- f. Por ejemplo,
-- clausulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- clausulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- clausulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------

clausulas :: Prop -> [Clausula]
clausulas f =
clausulasFNC (formaNormalConjuntiva f)

-- ---------------------------------------------------------------------
-- Clausulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- clausulasConjunto :: [Prop] -> [Clausula]
-- tal que (clausulasConjunto s) es un conjunto de clausulas equivalente
-- a s. Por ejemplo,
-- clausulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- clausulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------

clausulasConjunto :: [Prop] -> [Clausula]
clausulasConjunto s =
unionGeneral [clausulas f | f <- s]

-- ---------------------------------------------------------------------
-- Simbolos proposicionales de una clausula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- simbolosProposicionalesClausula :: Clausula -> [Prop]
-- tal que (simbolosProposicionalesClausula c) es el conjunto de los
-- simbolos proposicionales de c. Por ejemplo,
-- simbolosProposicionalesClausula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Simbolos proposicionales de un conjunto de clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
-- tal que (simbolosProposicionalesConjuntoClausula s) es el conjunto de los
-- simbolos proposicionales de s. Por ejemplo,
-- simbolosProposicionalesConjuntoClausula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------

simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
simbolosProposicionalesConjuntoClausula s =
unionGeneral [simbolosProposicionalesClausula c | c <- s]

-- ---------------------------------------------------------------------
-- Interpretaciones de una clausula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesClausula :: Clausula -> [Interpretación]
-- tal que (interpretacionesClausula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesClausula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesClausula [] ==> [[]]
-- ---------------------------------------------------------------------

interpretacionesClausula :: Clausula -> [Interpretación]
interpretacionesClausula c =
subconjuntos (simbolosProposicionalesClausula c)

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de clausulas --
-- ---------------------------------------------------------------------

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

interpretacionesConjuntoClausula :: [Clausula] -> [Interpretación]
interpretacionesConjuntoClausula c =
subconjuntos (simbolosProposicionalesConjuntoClausula c)

-- ---------------------------------------------------------------------
-- Modelos de clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretación -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------

esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral i (Atom s) = elem (Atom s) i
esModeloLiteral i (Neg (Atom s)) = notElem (Atom s) i

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloClausula :: Interpretación -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [p,r] [p, q] ==> True
-- esModeloClausula [r] [p, no q] ==> True
-- esModeloClausula [q,r] [p, no q] ==> False
-- esModeloClausula [q,r] [] ==> False
-- ---------------------------------------------------------------------

esModeloClausula :: Interpretación -> Clausula -> Bool
esModeloClausula i c =
or [esModeloLiteral i l | l <- c]

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

modelosClausula :: Clausula -> [Interpretación]
modelosClausula c =
[i | i <- interpretacionesClausula c,
esModeloClausula i c]

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoClausulas :: Interpretación -> [Clausula] -> Bool
-- tal que (esModeloConjuntoClausulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoClausulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoClausulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoClausulas [p] [] ==> True
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoClausulas :: [Clausula] -> [Interpretación]
-- tal que (modelosConjuntoClausulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoClausulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoClausulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoClausulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

modelosConjuntoClausulas :: [Clausula] -> [Interpretación]
modelosConjuntoClausulas s =
[i | i <- interpretacionesConjuntoClausula s,
esModeloConjuntoClausulas i s]

-- ---------------------------------------------------------------------
-- Clausulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esClausulaValida :: Clausula -> Bool
-- tal que (esClausulaValida c) se verifica si la clausula c es
-- válida. Por ejemplo,
-- esClausulaValida [p, q, no p] ==> True
-- esClausulaValida [p, q, no r] ==> False
-- esClausulaValida [] ==> False
-- ---------------------------------------------------------------------

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

esClausulaValida1 :: Clausula -> Bool
esClausulaValida1 c =
or [elem (complementario l) c | l <- c]

-- Definición alternativa:
esClausulaValida2 :: Clausula -> Bool
esClausulaValida2 c =
and [esModeloClausula i c | i <- interpretacionesClausula c]

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- esClausulaInsatisfacible :: Clausula -> Bool
-- tal que (esClausulaInsatisfacible c) se verifica si la clausula c es
-- insatisfacible. Por ejemplo,
-- esClausulaInsatisfacible [p, q, no p] ==> False
-- esClausulaInsatisfacible [p, q, no r] ==> False
-- esClausulaInsatisfacible [] ==> True
-- ---------------------------------------------------------------------

esClausulaInsatisfacible :: Clausula -> Bool
esClausulaInsatisfacible c =
null c

-- Definición alternativa:
esClausulaInsatisfacible1 :: Clausula -> Bool
esClausulaInsatisfacible1 c =
and [not (esModeloClausula i c) | i <- interpretacionesClausula c]

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esClausulaSatisfacible :: Clausula -> Bool
-- tal que (esClausulaSatisfacible c) se verifica si la clausula c es
-- satisfacible. Por ejemplo,
-- esClausulaSatisfacible [p, q, no p] ==> True
-- esClausulaSatisfacible [p, q, no r] ==> True
-- esClausulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------

esClausulaSatisfacible :: Clausula -> Bool
esClausulaSatisfacible c =
not (null c)

-- Definición alternativa:
esClausulaSatisfacible1 :: Clausula -> Bool
esClausulaSatisfacible1 c =
or [esModeloClausula i c | i <- interpretacionesClausula c]

-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoValidoDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoValidoDeClausulas s) se verifica si el conjunto de
-- clausulas s es válido. Por ejemplo,
-- esConjuntoValidoDeClausulas [[no p, q], [no q, p]] ==> False
-- esConjuntoValidoDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoValidoDeClausulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoValidoDeClausulas :: [Clausula] -> Bool
esConjuntoValidoDeClausulas s =
and [esClausulaValida c | c <- s]

-- Definición alternativa:
esConjuntoValidoDeClausulas1 :: [Clausula] -> Bool
esConjuntoValidoDeClausulas1 s =
modelosConjuntoClausulas s == interpretacionesConjuntoClausula s

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoConsistenteDeClausulas s) se verifica si el
-- conjunto de clausulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeClausulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeClausulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoConsistenteDeClausulas s =
not (null (modelosConjuntoClausulas s))

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoInconsistenteDeClausulas s) se verifica si el
-- conjunto de clausulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeClausulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeClausulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------

esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoInconsistenteDeClausulas s =
null (modelosConjuntoClausulas s)

-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esValidaPorClausulas :: Prop -> Bool
-- tal que (esValidaPorClausulas f) se verifica si el conjunto de
-- clausulas de f es válido. Por ejemplo,
-- esValidaPorClausulas (p --> q) ==> False
-- esValidaPorClausulas (p --> p) ==> True
-- esValidaPorClausulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------

esValidaPorClausulas :: Prop -> Bool
esValidaPorClausulas f =
esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante clausulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
-- tal que (esConsecuenciaEntreClausulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreClausulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreClausulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
esConsecuenciaEntreClausulas s1 s2 =
null [i | i <- interpretacionesConjuntoClausula (s1++s2)
, esModeloConjuntoClausulas i s1
, not ((esModeloConjuntoClausulas i s2))]

-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorClausulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorClausulas s f) se verifica si las clausulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorClausulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorClausulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorClausulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas s f =
esConsecuenciaEntreClausulas (clausulasConjunto s) (clausulas f)

-- Definición alternativa:
esConsecuenciaPorClausulas1 :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas1 s f =
esConjuntoInconsistenteDeClausulas (clausulasConjunto ((Neg f):s))

</source>

Lógica matemática y fundamentos (2015-16)

2016-05-10T12:33:20Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 11 |Solución colaborativa]] y [[R11 sol | Una solución ]]).
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 12 |Solución colaborativa]] y [[R12 sol | Una solución ]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 14 |Solución colaborativa]] y [[R14 sol | Una solución ]]).

R11 sol

2016-05-03T12:41:58Z

Mjoseh: Página creada con '<source lang = "haskell"> -- FormasNormales.hs -- Formas normales. -- --------------------------------------------------------------------- module FormasNormales where -- ----...'

<source lang = "haskell">
-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------

module FormasNormales where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import Data.List

-- ---------------------------------------------------------------------
-- Equivalencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
-- esEquivalente (p <--> q) ((p --> q) /\ (q --> p)) ==> True
-- esEquivalente (p --> q) ((no p) \/ q) ==> True
-- esEquivalente (p /\ q) (no ((no p) \/ (no q))) ==> True
-- esEquivalente (p \/ q) (no ((no p) /\ (no q))) ==> True
-- ---------------------------------------------------------------------

esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = esValida (Equi f g)

-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
-- eliminaEquivalencias (p <--> q)
-- ==> ((p --> q) /\ (q --> p))
-- eliminaEquivalencias ((p <--> q) /\ (q <--> r))
-- ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------

eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias (Atom f) =
(Atom f)
eliminaEquivalencias (Neg f) =
Neg (eliminaEquivalencias f)
eliminaEquivalencias (Conj f g) =
Conj (eliminaEquivalencias f) (eliminaEquivalencias g)
eliminaEquivalencias (Disj f g) =
Disj (eliminaEquivalencias f) (eliminaEquivalencias g)
eliminaEquivalencias (Impl f g) =
Impl (eliminaEquivalencias f) (eliminaEquivalencias g)
eliminaEquivalencias (Equi f g) =
Conj (Impl (eliminaEquivalencias f) (eliminaEquivalencias g))
(Impl (eliminaEquivalencias g) (eliminaEquivalencias f))

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
-- eliminaImplicaciones (p --> q)
-- ==> (no p \/ q)
-- eliminaImplicaciones (eliminaEquivalencias (p <--> q))
-- ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------

eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones (Atom f) =
(Atom f)
eliminaImplicaciones (Neg f) =
Neg (eliminaImplicaciones f)
eliminaImplicaciones (Conj f g) =
Conj (eliminaImplicaciones f) (eliminaImplicaciones g)
eliminaImplicaciones (Disj f g) =
Disj (eliminaImplicaciones f) (eliminaImplicaciones g)
eliminaImplicaciones (Impl f g) =
Disj (Neg (eliminaImplicaciones f)) (eliminaImplicaciones g)

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- interiorizaNegación :: Prop -> Prop
-- tal que (interiorizaNegación f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
-- interiorizaNegación (no (no p)) ==> p
-- interiorizaNegación (no (p /\ q)) ==> (no p \/ no q)
-- interiorizaNegación (no (p \/ q)) ==> (no p /\ no q)
-- interiorizaNegación (no (no (p \/ q))) ==> (p \/ q)
-- interiorizaNegación (no ((no p) \/ q)) ==> (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones.
-- ---------------------------------------------------------------------

interiorizaNegación :: Prop -> Prop
interiorizaNegación (Atom f) =
(Atom f)
interiorizaNegación (Neg f) =
interiorizaNegaciónAux f
interiorizaNegación (Conj f g) =
Conj (interiorizaNegación f) (interiorizaNegación g)
interiorizaNegación (Disj f g) =
Disj (interiorizaNegación f) (interiorizaNegación g)

interiorizaNegaciónAux :: Prop -> Prop
interiorizaNegaciónAux (Atom f) =
Neg (Atom f)
interiorizaNegaciónAux (Neg f) =
interiorizaNegación f
interiorizaNegaciónAux (Conj f g) =
Disj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g)
interiorizaNegaciónAux (Disj f g) =
Conj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g)

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
-- formaNormalNegativa (p <--> q)
-- ==> ((no p \/ q) /\ (no q \/ p))
-- formaNormalNegativa ((p \/ (no q)) --> r)
-- ==> ((no p /\ q) \/ r)
-- formaNormalNegativa ((p /\ (q --> r)) --> s)
-- ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------

formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f =
interiorizaNegación (eliminaImplicaciones (eliminaEquivalencias f))

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

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo,
-- literal p ==> True
-- literal (no p) ==> True
-- literal (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula.
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
-- complementario p ==> no p
-- complementario (no p) ==> p
-- ---------------------------------------------------------------------

complementario :: Literal -> Literal
complementario (Atom f) = Neg (Atom f)
complementario (Neg (Atom f)) = Atom f

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- literalesFórmulaFNN :: Prop -> [Literal]
-- tal que (literalesFórmulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
-- literalesFórmulaFNN (p \/ ((no q) \/ r)) ==> [p,no q,r]
-- literalesFórmulaFNN p ==> [p]
-- literalesFórmulaFNN (no p) ==> [no p]
-- ---------------------------------------------------------------------

literalesFórmulaFNN :: Prop -> [Literal]
literalesFórmulaFNN (Disj f g) =
(literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN (Conj f g) =
(literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN f = [f]

-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- interiorizaDisyunción :: Prop -> Prop
-- tal que (interiorizaDisyunción f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,
-- interiorizaDisyunción (p \/ (q /\ r)) ==> ((p \/ q) /\ (p \/ r))
-- interiorizaDisyunción ((p /\ q) \/ r) ==> ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaDisyunción :: Prop -> Prop
interiorizaDisyunción (Disj (Conj f1 f2) g) =
interiorizaDisyunción
(Conj (Disj (interiorizaDisyunción f1) (interiorizaDisyunción g))
(Disj (interiorizaDisyunción f2) (interiorizaDisyunción g)))
interiorizaDisyunción (Disj f (Conj g1 g2)) =
interiorizaDisyunción
(Conj (Disj (interiorizaDisyunción f) (interiorizaDisyunción g1))
(Disj (interiorizaDisyunción f) (interiorizaDisyunción g2)))
interiorizaDisyunción (Conj f g) =
Conj (interiorizaDisyunción f) (interiorizaDisyunción g)
interiorizaDisyunción f = f

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
-- formaNormalConjuntiva (p /\ (q --> r))
-- ==> (p /\ (no q \/ r))
-- formaNormalConjuntiva (no (p /\ (q --> r)))
-- ==> ((no p \/ q) /\ (no p \/ no r))
-- formaNormalConjuntiva (no(p <--> r))
-- ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------

formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f =
interiorizaDisyunción (formaNormalNegativa f)

-- ---------------------------------------------------------------------

-- Ejercicio 11.2: Definir la función
-- validaPorFNC:: Prop -> Bool
-- tal que (validaPorFNC f) comprueba si f es válida. Por ejemplo,
-- validaPorFNC ((p --> q) \/ (q --> p)) == True
-- validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
-- validaPorFNC (p --> p) == True
-- ---------------------------------------------------------------------

validaPorFNC:: Prop -> Bool
validaPorFNC f = all tieneParComplementario (listaLiterales f)
where tieneParComplementario xs = or [(complementario p) `elem` xs | p <- xs]

listaLiterales :: Prop -> [[Prop]]
listaLiterales f =
map listaLiteralesDisyuncion
(listaDisyuncionesFNC (formaNormalConjuntiva f))

listaDisyuncionesFNC :: Prop -> [Prop]
listaDisyuncionesFNC (Conj f g) = (listaDisyuncionesFNC f) `union`
(listaDisyuncionesFNC g)
listaDisyuncionesFNC f = [f]

listaLiteralesDisyuncion :: Prop -> [Prop]
listaLiteralesDisyuncion (Disj f g) = (listaLiteralesDisyuncion f) `union`
(listaLiteralesDisyuncion g)
listaLiteralesDisyuncion f = [f]

-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- interiorizaConjunción :: Prop -> Prop
-- tal que (interiorizaConjunción f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,
-- interiorizaConjunción (p /\ (q \/ r)) ==> ((p /\ q) \/ (p /\ r))
-- interiorizaConjunción ((p \/ q) /\ r) ==> ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaConjunción :: Prop -> Prop
interiorizaConjunción (Conj (Disj f1 f2) g) =
interiorizaConjunción
(Disj (Conj (interiorizaConjunción f1) (interiorizaConjunción g))
(Conj (interiorizaConjunción f2) (interiorizaConjunción g)))
interiorizaConjunción (Conj f (Disj g1 g2)) =
interiorizaConjunción
(Disj (Conj (interiorizaConjunción f) (interiorizaConjunción g1))
(Conj (interiorizaConjunción f) (interiorizaConjunción g2)))
interiorizaConjunción (Disj f g) =
Disj (interiorizaConjunción f) (interiorizaConjunción g)
interiorizaConjunción f = f

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
-- formaNormalDisyuntiva (p /\ (q --> r))
-- ==> ((p /\ no q) \/ (p /\ r))
-- formaNormalDisyuntiva (no (p /\ (q --> r)))
-- ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------

formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f =
interiorizaConjunción (formaNormalNegativa f)

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- satisfaciblePorFND:: Prop -> Bool
-- tal que (satisfaciblePorFND f) comprueba si f es satisfacible. Por
-- ejemplo,
-- satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
-- satisfaciblePorFND (p /\ (no p)) == False
-- satisfaciblePorFND ((p --> q) \/ (q --> p)) == True
-- ---------------------------------------------------------------------

satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = any noTieneParComplementario (listaLiterales' f)
where noTieneParComplementario xs =
and [not ((complementario p) `elem` xs) | p <- xs]

listaLiterales' :: Prop -> [[Prop]]
listaLiterales' f =
map listaLiteralesConjuncion
(listaConjuncionesFND (formaNormalDisyuntiva f))

listaConjuncionesFND :: Prop -> [Prop]
listaConjuncionesFND (Disj f g) = (listaConjuncionesFND f) `union`
(listaConjuncionesFND g)
listaConjuncionesFND f = [f]

listaLiteralesConjuncion :: Prop -> [Prop]
listaLiteralesConjuncion (Conj f g) = (listaLiteralesConjuncion f) `union`
(listaLiteralesConjuncion g)
listaLiteralesConjuncion f = [f]

</source>

Lógica matemática y fundamentos (2015-16)

2016-05-03T12:41:24Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 11 |Solución colaborativa]] y [[R11 sol | Una solución ]]).
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 14 |Solución colaborativa]] y [[R14 sol | Una solución ]]).

Relación 14

2016-05-03T12:39:04Z

Mjoseh: Página creada con '<source lang = "haskell"> -- ResolucionProposicional.hs -- Resolución proposicional. -- --------------------------------------------------------------------- module Resolucion...'

<source lang = "haskell">
-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Clausula -> Clausula -> Literal -> Clausula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
-- resolvente [no p,q] [no q,r] q ==> [no p,r]
-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]
-- resolvente [no p,q] [no p,no q] q ==> [no p]
-- ---------------------------------------------------------------------

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 l = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Clausula -> Clausula -> [Clausula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s = undefined

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautologia :: Clausula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautologia [p, q, no p] ==> True
-- esTautologia [p, q, no r] ==> False
-- esTautologia [] ==> False
-- ---------------------------------------------------------------------

esTautologia :: Clausula -> Bool
esTautologia c = undefined

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

eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias s = undefined

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolucion :: [Clausula] -> Bool
-- tal que (esInconsistentePorResolucion s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolucion [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolucion [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

esInconsistentePorResolucion :: [Clausula] -> Bool
esInconsistentePorResolucion s = undefined

-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------

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

esVálidaPorResolucion :: Prop -> Bool
esVálidaPorResolucion f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolucion s f = undefined

</source>

Archivo:ResolucionProposicional.hs

2016-05-03T12:38:05Z

Mjoseh:

R13

2016-05-03T12:37:33Z

Mjoseh: Protegió «R13» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

=== Relación 13: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

* Para toda fórmula F se tiene que si G es una forma de Skolem de F entonces ⊧ F ⇔ G.
----

'''Solución:'''

----
'''Ejercicio 2.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

----
'''Ejercicio 3.''' Dar una fórmula F satisfacible, tal que todos sus modelos sean necesariamante infinitos.

----

'''Solución:'''

----
'''Ejercicio 4.''' ¿Cuántos elementos han de tener los modelos de la fórmula F = ∀x f(f(x))= x ∧ ∀x f(x) ≠ x?
----

'''Solución:'''

Relación 13

2016-05-03T12:37:19Z

Mjoseh: Página creada con ' === Relación 13: Cuestiones === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: * Para toda fórmula F se tiene que si G es una forma de Skolem de F e...'

R13

2016-05-03T12:37:08Z

Lógica matemática y fundamentos (2015-16)

2016-05-03T12:36:47Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 11 |Solución colaborativa]]
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 14 |Solución colaborativa]] y [[R14 sol | Una solución ]]).

Relación 9

2016-05-02T16:27:52Z

Mjoseh:

=== Relación 9: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

* Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma normal disyuntiva de F₂. Si F₁ y F₂ son equivalentes, entonces G₁ y G₂ son fórmulas iguales.
* Para toda fórmula F se tiene que si G₁ es una forma normal conjuntiva de F y G₂ es una forma normal normal disyuntiva de F, entonces G₁ y G₂ son fórmulas distintas.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no es una tautología

----

'''Solución:'''

Relación 12

2016-04-29T08:05:55Z

Mjoseh: Página creada con '<source lang = "haskell"> -- Clausulas.hs -- Cláusulas. -- --------------------------------------------------------------------- module Clausulas where -- -------------------...'

<source lang = "haskell">
-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------

module Clausulas where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import FormasNormales
import Data.List

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Cláusula como una lista de
-- literales.
-- ---------------------------------------------------------------------

type Clausula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- clausula :: Prop -> Clausula
-- tal que (clausula f) es la clausula de la fórmula-clausal f. Por
-- ejemplo,
-- clausula p ==> [p]
-- clausula (no p) ==> [no p]
-- clausula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------

clausula :: Prop -> Clausula
clausula f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- clausulasFNC :: Prop -> [Clausula]
-- tal que (clausulasFNC f) es el conjunto de cláusulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- clausulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- clausulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------

clausulasFNC :: Prop -> [Clausula]
clausulasFNC = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- clausulas :: Prop -> [Clausula]
-- tal que (clausulas f) es un conjunto de cláusulas equivalente a
-- f. Por ejemplo,
-- clausulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- clausulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- clausulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------

clausulas :: Prop -> [Clausula]
clausulas f = undefined

-- ---------------------------------------------------------------------
-- Cláusulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- clausulasConjunto :: [Prop] -> [Clausula]
-- tal que (clausulasConjunto s) es un conjunto de cláusulas equivalente
-- a s. Por ejemplo,
-- clausulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- clausulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------

clausulasConjunto :: [Prop] -> [Clausula]
clausulasConjunto s = undefined

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- simbolosProposicionalesClausula :: Clausula -> [Prop]
-- tal que (simbolosProposicionalesClausula c) es el conjunto de los
-- símbolos proposicionales de c. Por ejemplo,
-- simbolosProposicionalesClausula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------

simbolosProposicionalesClausula :: Clausula -> [Prop]
simbolosProposicionalesClausula = undefined

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
-- tal que (simbolosProposicionalesConjuntoClausula s) es el conjunto de los
-- símbolos proposicionales de s. Por ejemplo,
-- simbolosProposicionalesConjuntoClausula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------

simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
simbolosProposicionalesConjuntoClausula s = undefined

-- ---------------------------------------------------------------------
-- Interpretaciones de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesClausula :: Clausula -> [Interpretacion]
-- tal que (interpretacionesClausula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesClausula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesClausula [] ==> [[]]
-- ---------------------------------------------------------------------

interpretacionesClausula :: Clausula -> [Interpretacion]
interpretacionesClausula c = undefined

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

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesConjuntoClausula :: [Clausula] -> [Interpretacion]
-- tal que (interpretacionesConjuntoClausula s) es el conjunto de
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjuntoClausula [[p, no q],[no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- interpretacionesConjuntoClausula []
-- ==> [[]]
-- ---------------------------------------------------------------------

interpretacionesConjuntoClausula :: [Clausula] -> [Interpretacion]
interpretacionesConjuntoClausula c = undefined

-- ---------------------------------------------------------------------
-- Modelos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretacion -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------

esModeloLiteral :: Interpretacion -> Literal -> Bool
esModeloLiteral = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloClausula :: Interpretacion -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [p,r] [p, q] ==> True
-- esModeloClausula [r] [p, no q] ==> True
-- esModeloClausula [q,r] [p, no q] ==> False
-- esModeloClausula [q,r] [] ==> False
-- ---------------------------------------------------------------------

esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- modelosClausula :: Clausula -> [Interpretacion]
-- tal que (modelosClausula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosClausula [no p, q] ==> [[p,q],[q],[]]
-- modelosClausula [no p, p] ==> [[p],[]]
-- modelosClausula [] ==> []
-- ---------------------------------------------------------------------

modelosClausula :: Clausula -> [Interpretacion]
modelosClausula c = undefined

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoClausulas :: Interpretacion -> [Clausula] -> Bool
-- tal que (esModeloConjuntoClausulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoClausulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoClausulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoClausulas [p] [] ==> True
-- ---------------------------------------------------------------------

esModeloConjuntoClausulas :: Interpretacion -> [Clausula] -> Bool
esModeloConjuntoClausulas i s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoClausulas :: [Clausula] -> [Interpretacion]
-- tal que (modelosConjuntoClausulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoClausulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoClausulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoClausulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

modelosConjuntoClausulas :: [Clausula] -> [Interpretacion]
modelosConjuntoClausulas s = undefined

-- ---------------------------------------------------------------------
-- Clausulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esClausulaValida :: Clausula -> Bool
-- tal que (esClausulaValida c) se verifica si la cláusula c es
-- válida. Por ejemplo,
-- esClausulaValida [p, q, no p] ==> True
-- esClausulaValida [p, q, no r] ==> False
-- esClausulaValida [] ==> False
-- ---------------------------------------------------------------------

esClausulaValida :: Clausula -> Bool
esClausulaValida c = undefined

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

esClausulaInsatisfacible :: Clausula -> Bool
esClausulaInsatisfacible c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esClausulaSatisfacible :: Clausula -> Bool
-- tal que (esClausulaSatisfacible c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo,
-- esClausulaSatisfacible [p, q, no p] ==> True
-- esClausulaSatisfacible [p, q, no r] ==> True
-- esClausulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------

esClausulaSatisfacible :: Clausula -> Bool
esClausulaSatisfacible c = undefined

-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoVálidoDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoVálidoDeClausulas s) se verifica si el conjunto de
-- cláusulas s es válido. Por ejemplo,
-- esConjuntoVálidoDeClausulas [[no p, q], [no q, p]] ==> False
-- esConjuntoVálidoDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoVálidoDeClausulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoVálidoDeClausulas :: [Clausula] -> Bool
esConjuntoVálidoDeClausulas s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoConsistenteDeClausulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeClausulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeClausulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoConsistenteDeClausulas s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoInconsistenteDeClausulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeClausulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeClausulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------

esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoInconsistenteDeClausulas s = undefined

-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esValidaPorClausulas :: Prop -> Bool
-- tal que (esValidaPorClausulas f) se verifica si el conjunto de
-- cláusulas de f es válido. Por ejemplo,
-- esValidaPorClausulas (p --> q) ==> False
-- esValidaPorClausulas (p --> p) ==> True
-- esValidaPorClausulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------

esValidaPorClausulas :: Prop -> Bool
esValidaPorClausulas f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
-- tal que (esConsecuenciaEntreClausulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreClausulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreClausulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
esConsecuenciaEntreClausulas s1 s2 = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorClausulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorClausulas s f) se verifica si las cláusulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorClausulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorClausulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorClausulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas s f = undefined

</source>

Relación 11

2016-04-29T08:05:09Z

<source lang = "haskell">
-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------

module FormasNormales where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import Data.List

-- ---------------------------------------------------------------------
-- Equivalencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
-- esEquivalente (p <--> q) ((p --> q) /\ (q --> p)) ==> True
-- esEquivalente (p --> q) ((no p) \/ q) ==> True
-- esEquivalente (p /\ q) (no ((no p) \/ (no q))) ==> True
-- esEquivalente (p \/ q) (no ((no p) /\ (no q))) ==> True
-- ---------------------------------------------------------------------

esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
-- eliminaEquivalencias (p <--> q)
-- ==> ((p --> q) /\ (q --> p))
-- eliminaEquivalencias ((p <--> q) /\ (q <--> r))
-- ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------

eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
-- eliminaImplicaciones (p --> q)
-- ==> (no p \/ q)
-- eliminaImplicaciones (eliminaEquivalencias (p <--> q))
-- ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------

eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- interiorizaNegacion :: Prop -> Prop
-- tal que (interiorizaNegacion f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
-- interiorizaNegacion (no (no p)) ==> p
-- interiorizaNegacion (no (p /\ q)) ==> (no p \/ no q)
-- interiorizaNegacion (no (p \/ q)) ==> (no p /\ no q)
-- interiorizaNegacion (no (no (p \/ q))) ==> (p \/ q)
-- interiorizaNegacion (no ((no p) \/ q)) ==> (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones.
-- ---------------------------------------------------------------------

interiorizaNegacion :: Prop -> Prop
interiorizaNegacion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
-- formaNormalNegativa (p <--> q)
-- ==> ((no p \/ q) /\ (no q \/ p))
-- formaNormalNegativa ((p \/ (no q)) --> r)
-- ==> ((no p /\ q) \/ r)
-- formaNormalNegativa ((p /\ (q --> r)) --> s)
-- ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------

formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f = undefined

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

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo,
-- literal p ==> True
-- literal (no p) ==> True
-- literal (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula.
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
-- complementario p ==> no p
-- complementario (no p) ==> p
-- ---------------------------------------------------------------------

complementario :: Literal -> Literal
complementario = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- literalesFormulaFNN :: Prop -> [Literal]
-- tal que (literalesFormulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
-- literalesFormulaFNN (p \/ ((no q) \/ r)) ==> [p,no q,r]
-- literalesFormulaFNN p ==> [p]
-- literalesFormulaFNN (no p) ==> [no p]
-- ---------------------------------------------------------------------

literalesFormulaFNN :: Prop -> [Literal]
literalesFormulaFNN = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- interiorizaDisyuncion :: Prop -> Prop
-- tal que (interiorizaDisyuncion f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,
-- interiorizaDisyuncion (p \/ (q /\ r)) ==> ((p \/ q) /\ (p \/ r))
-- interiorizaDisyuncion ((p /\ q) \/ r) ==> ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaDisyuncion :: Prop -> Prop
interiorizaDisyuncion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
-- formaNormalConjuntiva (p /\ (q --> r))
-- ==> (p /\ (no q \/ r))
-- formaNormalConjuntiva (no (p /\ (q --> r)))
-- ==> ((no p \/ q) /\ (no p \/ no r))
-- formaNormalConjuntiva (no(p <--> r))
-- ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------

formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f = undefined

-- ---------------------------------------------------------------------

-- Ejercicio 11.2: Definir la función
-- validaPorFNC:: Prop -> Bool
-- tal que (validaPorFNC f) comprueba si f es válida. Por ejemplo,
-- validaPorFNC ((p --> q) \/ (q --> p)) == True
-- validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
-- validaPorFNC (p --> p) == True

-- ---------------------------------------------------------------------

validaPorFNC:: Prop -> Bool
validaPorFNC = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- interiorizaConjuncion :: Prop -> Prop
-- tal que (interiorizaConjuncion f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,
-- interiorizaConjuncion (p /\ (q \/ r)) ==> ((p /\ q) \/ (p /\ r))
-- interiorizaConjuncion ((p \/ q) /\ r) ==> ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaConjuncion :: Prop -> Prop
interiorizaConjuncion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
-- formaNormalDisyuntiva (p /\ (q --> r))
-- ==> ((p /\ no q) \/ (p /\ r))
-- formaNormalDisyuntiva (no (p /\ (q --> r)))
-- ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------

formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- satisfaciblePorFND:: Prop -> Bool
-- tal que (satisfaciblePorFND f) comprueba si f es satisfacible. Por
-- ejemplo,
-- satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
-- satisfaciblePorFND (p /\ (no p)) == False
-- satisfaciblePorFND ((p --> q) \/ (q --> p)) == True

-- ---------------------------------------------------------------------

satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = undefined

</source>

Archivo:Clausulas.hs

2016-04-29T08:04:24Z

Mjoseh:

Archivo:FormasNormales.hs

2016-04-29T08:04:09Z

Mjoseh:

Lógica matemática y fundamentos (2015-16)

2016-04-29T07:56:36Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 11 |Solución colaborativa]]
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).

Relación 9

2016-04-28T07:16:33Z

Mjoseh:

Relación 10

2016-04-28T06:20:38Z

Mjoseh: Página creada con ' === Relación 10: Tableros semánticos en LPO === ---- '''Ejercicio 1.''' Decidir por tableros semánticos, si: ∀x (P(x) → Q(x)) ⊧ (∃x P(x)) → (∃ x Q(x)) ---- ...'

=== Relación 10: Tableros semánticos en LPO ===

----
'''Ejercicio 1.''' Decidir por tableros semánticos, si:

∀x (P(x) → Q(x)) ⊧ (∃x P(x)) → (∃ x Q(x))

----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir por tableros semánticos, si:

⊧ ∀x (P(x) → R(x,x)) → ∀x ∃ y (R(x,y) ∨ ¬ P(y))

----

'''Solución:'''

----
'''Ejercicio 3.''' Decidir por tableros semánticos, si:

∀x ∃ y (R(x,y) ∨ ¬ P(y)) ⊧ ∀x (P(x) → R(x,x))

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir por tableros semánticos, si:

∀x ∀ y (R(x,y) → R(y,x)) ⊧ ∀x ∀y ∀z (R(x,y) ∧ R(x,z) → ∃u (R(y,u) ∧ R(z,u)))

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por tableros semánticos, si:

* ⊧ (∃x P(x)) → P(a)
* {∀x(P(x) → Q(x)), ∀y(Q(a) ∨ R(y) → S(a))} ⊧ ∀x (P(x) → S(a))

----

'''Solución:'''

R10

2016-04-28T06:20:30Z

Mjoseh: Protegió «R10» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R10

2016-04-28T06:20:23Z

R9

2016-04-28T06:19:49Z

Mjoseh:

=== Relación 9: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

* Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma normal disyuntiva de F₂. Si
F₁ y F₂ son equivalentes, entonces G₁ y G₂ son fórmulas iguales.
* Para toda fórmula F se tiene que si G₁ es una forma normal conjuntiva de F y G₂ es una
forma normal normal disyuntiva de F, entonces G₁ y G₂ son fórmulas distintas.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no
es una tautología

----

'''Solución:'''

Relación 9

2016-04-28T06:19:35Z

Mjoseh: Página creada con ' === Relación 9: Cuestiones === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: * Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma normal...'

=== Relación 9: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

* Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma normal disyuntiva de F₂. Si
F₁ y F₂ son equivalentes, entonces G₁ y G₂ son fórmulas iguales.
* Para toda fórmula F se tiene que si G₁ es una forma normal conjuntiva de F y G₂ es una
forma normal normal disyuntiva de F, entonces G₁ y G₂ son fórmulas distintas.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no
es una tautología

----

'''Solución:'''

R9

2016-04-28T06:19:20Z

Mjoseh: Protegió «R9» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

=== Relación 10: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

* Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma normal disyuntiva de F₂. Si
F₁ y F₂ son equivalentes, entonces G₁ y G₂ son fórmulas iguales.
* Para toda fórmula F se tiene que si G₁ es una forma normal conjuntiva de F y G₂ es una
forma normal normal disyuntiva de F, entonces G₁ y G₂ son fórmulas distintas.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no
es una tautología

----

'''Solución:'''

R9

2016-04-28T06:19:13Z

Mjoseh: Página creada con ' === Relación 10: Cuestiones === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: * Sean G₁ una forma normal disyuntiva de F₁ y G₂ una forma norma...'

Lógica matemática y fundamentos (2015-16)

2016-04-28T06:18:28Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).

Relación 8

2016-04-21T11:51:41Z

Mjoseh: Página creada con ' === Relación 8: Cuestiones sobre tableros semánticos === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: Sea T un tablero de S₁, I un modelo de una ...'

=== Relación 8: Cuestiones sobre tableros semánticos ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

Sea T un tablero de S₁, I un modelo de una hoja abierta de T y S₂ ⊆ S₁. Entonces,
I ⊧ S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguiente afirmación:

Si S es un conjunto inconsistente de fórmulas, entonces el tablero semántico cerrado de
S obtenido aplicando las reglas α antes que las reglas β tiene menos nodos que el tablero
semántico cerrado de S obtenido aplicando las reglas β antes que las reglas α.

----

'''Solución:'''

R8

2016-04-21T11:51:28Z

Mjoseh: Protegió «R8» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R8

2016-04-21T11:51:11Z

Relación 7

2016-04-21T11:50:43Z

Mjoseh: Página creada con '<source lang = "haskell"> -- TablerosSemánticos.hs -- Tableros semánticos proposicionales. -- José A. Alonso Jiménez <jalonso@us.es> -- ------------------------------------...'

<source lang = "haskell">

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

module TablerosSemanticos where

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

import SintaxisSemantica
import Data.List

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

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo,
-- literal p ==> True
-- literal (no p) ==> True
-- literal (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal = undefined

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

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

dobleNegacion :: Prop -> Bool
dobleNegacion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------

alfa :: Prop -> Bool
alfa = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------

beta :: Prop -> Bool
beta = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- componentes :: Prop -> [Prop]
-- tal que (componentes ) es la lista de las componentes de la fórmula
-- f. Por ejemplo,
-- componentes (p /\ q --> r) ==> [no (p /\ q),r]
-- componentes (no (p /\ q --> r)) ==> [(p /\ q),no r]
-- ---------------------------------------------------------------------

componentes :: Prop -> [Prop]
componentes = undefined

-- ---------------------------------------------------------------------
-- Modelos mediante tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- conjuntoDeLiterales :: [Prop] -> Bool
-- tal que (conjuntoDeLiterales fs) se verifica si fs es un conjunto de
-- literales. Por ejemplo,
-- conjuntoDeLiterales [p --> q, no r, r /\ s, p] ==> False
-- conjuntoDeLiterales [p, no q, r] ==> True
-- ---------------------------------------------------------------------

conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales fs = undefined

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

tieneContradiccion :: [Prop] -> Bool
tieneContradiccion fs = undefined

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

expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = undefined

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

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = undefined

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

expansionBeta :: [Prop] -> Prop -> [[Prop]]
expansionBeta fs f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- sucesores :: [Prop] -> [[Prop]]
-- tal que (sucesores fs) es la lista de sucesores de fs. Por ejemplo,
-- sucesores [q \/ s, no(no r), p1 /\ p2] => [[r,(q \/ s),(p1 /\ p2)]]
-- sucesores [r,(q \/ s),(p1 /\ p2)] => [[p1,p2,r,(q \/ s)]]
-- sucesores [p1,p2,r,(q \/ s)] => [[q,p1,p2,r],[s,p1,p2,r]]
-- ---------------------------------------------------------------------

sucesores :: [Prop] -> [[Prop]]
sucesores = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- modelosTab :: [Prop] -> [[Prop]]
-- tal que (modelosTab fs) es el conjunto de los modelos de fs
-- calculados mediante el método de tableros semánticos. Por ejemplo,
-- modelosTab [p --> q, no(q --> p)]
-- ==> [[no p,q],[q,no p]]
-- modelosTab [p --> q, no q --> no p]
-- ==> [[q,no p],[no p],[q],[no p,q]]
-- ---------------------------------------------------------------------

modelosTab :: [Prop] -> [[Prop]]
modelosTab = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- subconjunto :: Eq a => [a] -> [a] -> Bool
-- tal que (subconjunto x y) se verifica si x es subconjunto de y. Por
-- ejemplo,
-- subconjunto [1,3] [3,2,1] ==> True
-- subconjunto [1,3,5] [3,2,1] ==> False
-- ---------------------------------------------------------------------

subconjunto :: Eq a => [a] -> [a] -> Bool
subconjunto xs ys = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- modelosGenerales :: [Prop] -> [[Prop]]
-- tal que (modelosGenerales fs) es el conjunto de los modelos generales
-- de fs calculados mediante el método de tableros semánticos. Por
-- ejemplo,
-- modelosGenerales [p --> q, no q --> no p] ==> [[no p],[q]]
-- ---------------------------------------------------------------------

modelosGenerales :: [Prop] -> [[Prop]]
modelosGenerales fs = undefined

-- ---------------------------------------------------------------------
-- Teoremas por tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- esTeoremaPorTableros :: Prop -> Bool
-- tal que (esTeoremaPorTableros f) se verifica si la fórmula f es
-- teorema (mediante tableros semánticos). Por ejemplo,
-- esTeoremaPorTableros (p --> p) ==> True
-- esTeoremaPorTableros (p --> q) ==> False
-- ---------------------------------------------------------------------

esTeoremaPorTableros :: Prop -> Bool
esTeoremaPorTableros f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia por tableros --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esDeduciblePorTableros :: [Prop] -> Prop -> Bool
-- tal que (esDeduciblePorTableros fs f) se verifica si la fórmula f es
-- consecuencia (mediante tableros) del conjunto de fórmulas fs. Por
-- ejemplo,
-- esDeduciblePorTableros [p --> q, q --> r] (p --> r) ==> True
-- esDeduciblePorTableros [p --> q, q --> r] (p <--> r) ==> False
-- ---------------------------------------------------------------------

esDeduciblePorTableros :: [Prop] -> Prop -> Bool
esDeduciblePorTableros fs f = undefined

</source>

Archivo:TablerosSemanticos.hs

2016-04-21T11:49:36Z

Mjoseh:

Lógica matemática y fundamentos (2015-16)

2016-04-21T11:48:50Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).

R2a sol

2016-04-21T11:48:21Z

Mjoseh:

<source lang="haskell">
-- SintaxisSemanticaProp.hs
-- Lógica proposicional: Sintaxis y semántica
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- 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
-- simbolosPropForm :: Prop -> [Prop]
-- tal que (simbolosPropForm f) es el conjunto formado por todos los
-- símbolos proposicionales que aparecen en f. Por ejemplo,
-- simbolosPropForm (p /\ q --> p) ==> [p,q]
-- ---------------------------------------------------------------------

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

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

significado :: Prop -> Interpretacion -> Bool
significado (Atom f) i = (Atom f) `elem` i
significado (Neg f) i = not (significado f i)
significado (Conj f g) i = (significado f i) && (significado g i)
significado (Disj f g) i = (significado f i) || (significado g i)
significado (Impl f g) i = significado (Disj (Neg f) g) i
significado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i

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

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

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

interpretacionesForm :: Prop -> [Interpretacion]
interpretacionesForm f = subconjuntos (simbolosPropForm f)

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

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

esModeloFormula :: Interpretacion -> Prop -> Bool
esModeloFormula i f = significado f i

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- modelosFormula :: Prop -> [Interpretacion]
-- tal que (modelosFormula f) es la lista de todas las interpretaciones
-- de f que son modelo de F. Por ejemplo,
-- modelosFormula ((p \/ q) /\ ((no q) \/ r))
-- ==> [[p,q,r],[p,r],[p],[q,r]]
-- ---------------------------------------------------------------------

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f =
[i | i <- interpretacionesForm f,
esModeloFormula i f]

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

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

esValida :: Prop -> Bool
esValida 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
-- ---------------------------------------------------------------------

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

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

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

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

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

uniónG :: Eq a => [[a]] -> [a]
uniónG = foldl union []

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

símbolosPropConj :: [Prop] -> [Prop]
símbolosPropConj s
= unionGeneral [simbolosPropForm f | f <- s]

símbolosPropConj2 :: [Prop] -> [Prop]
símbolosPropConj2 = uniónG . map simbolosPropForm

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

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- interpretacionesConjunto :: [Prop] -> [Interpretacion]
-- 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],[]]
-- ---------------------------------------------------------------------

interpretacionesConjunto :: [Prop] -> [Interpretacion]
interpretacionesConjunto s =
subconjuntos (símbolosPropConj s)

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

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esModeloConjunto :: Interpretacion -> [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
-- ---------------------------------------------------------------------

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s =
and [esModeloFormula i f | f <- s]

esModeloConjunto2 :: Interpretacion -> [Prop] -> Bool
esModeloConjunto2 i s = all (esModeloFormula i) s

-- --------------------g-------------------------------------------------
-- Ejercicio 19: Definir la función
-- modelosConjunto :: [Prop] -> [Interpretacion]
-- 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]]
-- ---------------------------------------------------------------------

modelosConjunto :: [Prop] -> [Interpretacion]
modelosConjunto s =
[i | i <- interpretacionesConjunto s,
esModeloConjunto i 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
-- ---------------------------------------------------------------------

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

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 =
null [i | i <- interpretacionesConjunto (f:s),
esModeloConjunto i s,
not (esModeloFormula i f)]

esConsecuencia2 :: [Prop] -> Prop -> Bool
esConsecuencia2 s f =
and [esModeloFormula i f | i <- interpretacionesConjunto (f:s),
esModeloConjunto i s]

</source>

Lógica matemática y fundamentos (2015-16)

2016-04-21T11:47:20Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]], [[Relación 2a |Solución colaborativa]] y [[R2a sol | Una solución]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]). [http://www.cs.us.es/~mjoseh/R4.thy]
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]][http://www.cs.us.es/~mjoseh/R5.thy]
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]], [[Relación 7 |Solución colaborativa]] y [[R7 sol | Una solución ]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).

R6

2016-04-19T10:57:38Z

Mjoseh:

Relación 6

2016-04-19T10:57:19Z

Mjoseh:

=== Relación 6: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.'''
Sea F la fórmula P(x) → P ( a ) , donde a es un símbolo de constante. ¿Es
F satisfacible? ¿Tiene modelos? ¿Es F una fórmula válida?

----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de
aridad 1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I ) la
estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
Decidir cuáles de las siguientes fórmulas de L son válidas en I :
* P ( x ) → ∃ yQ ( y, x ) .
* ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''
1. No es válida pues existe una asignación que hace a la fórmula falsa. Tomando A(x) = a

P(a) = 1

Q(y,a) = 0 para cualquier asignación de y

Luego la implicación es falsa.

2. No es válida pues existe una asignación que hace a la fórmula falsa.

Tomando de nuevo A(x)=a

Q(f(a),a)=Q(b,a)=0

Luego hemos encontrado un x que no satisface Q(f(x),x) y

por tanto la fórmula es falsa.

3. Si es válida pues para toda asignación de x se verifica la fórmula.

Si A(x)=a entonces Q(f(a),a)=Q(b,a)=0 y Q(a,a)=0 luego la implicación es verdadera.

Si A(x)=b entonces Q(f(b),b)=Q(b,b)=1 y Q(b,b)=1 luego la implicación es verdadera.

Si A(x)=c entonces Q(f(c),c)=Q(a,c)=0 y Q(c,c)=0 luego la implicación es verdadera.

Si A(x)=d entonces Q(f(d),d)=Q(c,d)=0 y Q(d,d)=0 luego la implicación es verdadera.

4. No es válida pues existe una asignación que hace a la fórmula falsa.

Tomando A(x)=c y A(y)=b tenemos que Q(c,b)=1 y P(c)=0 luego es falsa la implicación.
----
'''Ejercicio 3.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
F_1 : = ∀ x [ f ( x ) ≠ a ] ,
F_2 : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
F_3 : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de las tres fórmulas es consecuencia de las dos restantes.
----

'''Solución:'''

Relación 6

2016-04-07T06:44:40Z

Mjoseh:

Relación 6

2016-04-07T06:44:26Z

Mjoseh: Página creada con '=== Relación 6: Sintaxis y semántica de la Lógica de primer orden === ---- '''Ejercicio 1.''' Sea F la fórmula P(x) → P ( a ) , donde a es un símbolo de constante. ¿Es...'

R6

2016-04-07T06:44:18Z

Mjoseh: Protegió «R6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R6

2016-04-07T06:44:10Z