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

Lógica matemática y fundamentos (2014-15)

2015-06-03T15:26:19Z

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]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 5 (resuelta)''':[[Relación 5 (resuelta) |Solución]].
* '''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]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 9 |Solución colaborativa]] y [[Una solución | una solución]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.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''': Argumentación y Deducción natural en lógica de primer orden.([[R14 |Enunciado]] y [[Relación 14 |Solución colaborativa]]).
* '''Relación 15''': Tableros semánticos en lógica de primer orden.([[R15 |Enunciado]] y [[Relación 15 |Solución colaborativa]]).
* '''Relación 16''': Resolución en lógica de primer orden.([[R16 |Enunciado]] y [[Relación 16 |Solución colaborativa]]).
* '''Segundo examen (resuelto)''':([[Ejercicio 4 (a) |Solución_4a]], [[Ejercicio 4 (b)|Solución_4b]],[[Ejercicio 5 (a) |Solución_5a]] y [[Ejercicio 5 (b) |Solución_5b]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

Lógica matemática y fundamentos (2014-15)

2015-06-03T15:25:53Z

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]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 5 (resuelta)''':[[Relación 5 (resuelta) |Solución]].
* '''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]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 9 |Solución colaborativa]] y [[Una solución | una solución]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.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''': Argumentación y Deducción natural en lógica de primer orden.([[R14 |Enunciado]] y [[Relación 14 |Solución colaborativa]]).
* '''Relación 15''': Tableros semánticos en lógica de primer orden.([[R15 |Enunciado]] y [[Relación 15 |Solución colaborativa]]).
* '''Relación 16''': Resolución en lógica de primer orden.([[R16 |Enunciado]] y [[Relación 16 |Solución colaborativa]]).
* '''Segundo examen (resuelto)''':([[Ejercicio 4 (a) |Solución_4a]], [[Ejercicio 4 (b)|Solución_4b]],[[Ejercicio 5 (a) |Solución_5a]] y [[Ejercicio 5 (b) |Solución_5b]]).
* '''Relación 17''': Resolución.([[R17 |Enunciado]] y [[Relación 17 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

2015-05-22T07:43:08Z

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 ∀...'

2015-05-17T07:59:18Z

Mjoseh:

=== Relación 15: 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:'''

Lógica matemática y fundamentos (2014-15)

2015-05-11T12:32: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]] y [[Relación 2a |Solución colaborativa]]).
* '''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]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 5 (resuelta)''':[[Relación 5 (resuelta) |Solución]].
* '''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]] y [[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''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 9 |Solución colaborativa]] y [[Una solución | una solución]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Argumentación y Deducción natural en lógica de primer orden
([[Rel_14 |Enunciado]] y [[Relación 14 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

Relación 13

2015-05-10T15:32:53Z

Mjoseh:

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

2015-05-10T15:32:21Z

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

=== 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:'''

R13

2015-05-10T15:32:09Z

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

R13

2015-05-10T15:31:52Z

=== 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:'''

Lógica matemática y fundamentos (2014-15)

2015-05-10T15:31:22Z

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]] y [[Relación 2a |Solución colaborativa]]).
* '''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]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 5 (resuelta)''':[[Relación 5 (resuelta) |Solución]].
* '''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]] y [[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''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 9 |Solución colaborativa]] y [[Una solución | una solución]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]] y [[Relación 13 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

Relación 12

2015-04-29T10:24:49Z

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

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

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

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

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = undefined

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

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = undefined

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

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = undefined

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

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

esTautología :: Cláusula -> Bool
esTautología c = undefined

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

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = undefined

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

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

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = undefined

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

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

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = undefined

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

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

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = undefined

</source>

Relación 11

2015-04-29T10:24:05Z

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 Cláusula = [Literal]

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

cláusula :: Prop -> Cláusula
cláusula f = undefined

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

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

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

cláusulas :: Prop -> [Cláusula]
cláusulas f = undefined

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- ---------------------------------------------------------------------
-- Cláusulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

</source>

Archivo:ResolucionProposicional.hs

2015-04-29T10:23:17Z

Mjoseh:

Archivo:Clausulas.hs

2015-04-29T10:23:03Z

Mjoseh:

Una solución

2015-04-29T10:22:29Z

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 = esVálida (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)

----

interiorizaNegacion :: Prop -> Prop
interiorizaNegacion (Atom p) = Atom p
interiorizaNegacion (Neg (Atom p)) = Neg (Atom p)
interiorizaNegacion (Conj p q) = Conj (interiorizaNegacion p)
(interiorizaNegacion q)
interiorizaNegacion (Disj p q) = Disj (interiorizaNegacion p)
(interiorizaNegacion q)
interiorizaNegacion (Neg (Neg p)) = interiorizaNegacion p
interiorizaNegacion (Neg (Conj p q)) = Disj (interiorizaNegacion(Neg p))
(interiorizaNegacion(Neg q))
interiorizaNegacion (Neg (Disj p q)) = Conj (interiorizaNegacion(Neg p))
(interiorizaNegacion(Neg q))

----

-- ---------------------------------------------------------------------
-- 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 (2014-15)

2015-04-29T10:12:14Z

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]] y [[Relación 2a |Solución colaborativa]]).
* '''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]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 5 (resuelta)''':[[Relación 5 (resuelta) |Solución]].
* '''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]] y [[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''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]],[[Relación 9 |Solución colaborativa]] y [[Una solución | una solución]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]], [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]], [[Relación 12 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].