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

Relación 11

2013-05-22T18:57:29Z

Pedperroj:

<source lang = "haskell">

-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

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

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

--Jose M Contreras

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 x = union (delete x c1) (delete (complementario x) c2)
--La función complementario se define en el fichero importado FormasNormales

--Miriam Núñez-Romero

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

--Jose M Contreras

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

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

--Jose M Contreras

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

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

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

--Jose M Contreras

esTautologia :: Clausula -> Bool
esTautologia c = or[elem (complementario x) (delete x c)|x<-c]

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

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

--Jose M Contreras

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

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

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

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

esInconsistentePorResolución' :: [Cláusula] -> [Cláusula] -> Bool
esInconsistentePorResolución' soporte usables
| null soporte = False
| elem [] soporte = True
| otherwise =
esInconsistentePorResolución' soporte' usables'
where actual = head soporte
usables' = union [actual] usables
soporte' = union (tail soporte)
[c
| c <- resolventesCláusulaConjunto
actual
usables'
, not (esTautología c)
, notElem c soporte
, notElem c usables']

-- ---------------------------------------------------------------------
-- 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 =
esInconsistentePorResolucion (eliminaTautologias (clausulas (Neg f)))

-- ---------------------------------------------------------------------
-- 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 =
esInconsistentePorResolucion (eliminaTautologias (clausulasConjunto ((Neg f):s)))

</source>

Relación 10

2013-05-22T17:52:41Z

Pedperroj:

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

module Clausulas where

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

import SintaxisSemantica
import FormasNormales
import Data.List

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

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

type Cláusula = [Literal]

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

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

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

--José M Contreras

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

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

--José M Contreras

clausulas :: Prop -> [Clausula]
clausulas = clausulasFNC . formaNormalConjuntiva

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

--Miriam Núñez-Romero

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

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

--Miriam Núñez-Romero

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

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

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

--Miriam Núñez-Romero

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

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

--Alejandro Ballesteros

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

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

--Alejandro Ballesteros

esCláusulaSatisfacible :: Cláusula -> Bool
esCláusulaSatisfacible c = not (null c)

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

--Alejandro Ballesteros

esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
esConjuntoVálidoDeCláusulas s = and [ esClausulaValida c|c<-s]

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

--Alejandro Ballesteros

esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoConsistenteDeCláusulas s = not( null (modeloConjuntoClausulas s))

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

--Alejandro Ballesteros

esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoInconsistenteDeCláusulas s = null (modeloConjuntoClausulas s))

-- ---------------------------------------------------------------------
-- 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 = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro José Perea Rojo

esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
esConsecuenciaEntreClausulas s1 s2 = null [k | k <- interpretacionesConjuntoClausula (s1++s2)
, esModeloConjuntoClausulas k s1
, not ((esModeloConjuntoClausulas k s2))]

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

--Alejandro Ballesteros

esConsecuenciaPorCláusulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorCláusulas s f = esConjuntoInconsistenteDeClausulas (clausulasConjunto((Neg f):s))

--Pedro José Perea Rojo
esConsecuenciaPorClausulas2 :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas2 s f = esConsecuenciaEntreClausulas (clausulasConjunto s) (clausulas f)

</source>

Ejercicio 3

2013-04-29T18:38:45Z

Pedperroj: /* Selección del ejercicio */

== Enunciado ==
El tercer ejercicio evaluable consiste en la realización de un ejercicio de argumentación en lógica de primer orden, haciendo la demostración por deducción natural con Isabelle/HOL y por tableros semánticos.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[E3|E3]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* Se enviará a mjoseh@us.es antes del viernes 10 de mayo de 2013, dos ficheros: uno usuario_3a.thy con la prueba por deducción natural y otro con la prueba por tableros.
* Los lemas que se usen en una demostración tendrán que ser probados de forma no automática.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1:
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3:
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8:
* Ejercicio 9:
* Ejercicio 10: Gonzalo José Muñoz González-Meneses
* Ejercicio 11: José Antonio Jaime Sabín
* Ejercicio 12: Erlinda Menéndez Pérez
* Ejercicio 13: Concepción García Vidal
* Ejercicio 14: Carmen Martínez Navarro
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17: Jesús Horno Cobo
* Ejercicio 18:
* Ejercicio 19: Mª de los Remedios Sillero Denamiel
* Ejercicio 20: Antonio Jesús Molero del Río
* Ejercicio 21: Irene Araujo Guijo
* Ejercicio 22: FºJavier Sanz Gil
* Ejercicio 23:
* Ejercicio 24:
* Ejercicio 25: Pedro José Perea Rojo
* Ejercicio 26: José María Contreras Beltrán
* Ejercicio 27: Isabel Duarte Tosso
* Ejercicio 28:

Ejercicio 2

2013-04-15T10:49:28Z

Pedperroj: /* Selección del ejercicio */

== Enunciado ==
El segundo ejercicio evaluable consiste en la realización de una demostración por deducción natural en la Lógica de primer orden, con Isabelle/HOL.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[T2|T2]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* El ejercicio resuelto se enviará a mjoseh@us.es en un fichero usuario_2.thy antes del viernes 26 de abril de 2013.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1: Francisco Vilches Chacón
* Ejercicio 2: Ana Rocío del Valle Benavides
* Ejercicio 3:
* Ejercicio 4:
* Ejercicio 5: Concepción García Vidal
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8: Inmaculada Arjona Arjona
* Ejercicio 9:
* Ejercicio 10: Carmen Martínez Navarro
* Ejercicio 11: Pedro José Perea Rojo
* Ejercicio 12:
* Ejercicio 13:
* Ejercicio 14:
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17:
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20:
* Ejercicio 21:
* Ejercicio 22: Erlinda Menéndez Pérez
* Ejercicio 23: Irene Araujo Guijo
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José Mª Contreras Beltrán
* Ejercicio 27: FºJavier Sanz Gil
* Ejercicio 28: Isabel Duarte Tosso
* Ejercicio 29:
* Ejercicio 30:
* Ejercicio 31: Antonio Jesús Molero del Río
* Ejercicio 32: Mª de los Remedios Sillero Denamiel
* Ejercicio 33: Pedro Ros Reina