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

Relación 10

2013-05-20T09:45:09Z

Alebalher:

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

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

--Alejandro Ballesteros

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

</source>

Ejercicio 3

2013-05-08T13:31:16Z

Alebalher: Deshecha la edición 487 de Alebalher (disc.)

== 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: Alejandro Alfaro Martínez
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3: Salvador Joaquín Franco Peña
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5: Pedro Ros Reina
* Ejercicio 6: Carmen Martinez Navarro
* Ejercicio 7: Ana Rocío del Valle
* Ejercicio 8:
* Ejercicio 9: Francisco Nieto Rueda
* 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:
* Ejercicio 15: Elena Villalba Calderón
* Ejercicio 16: Miguel Ángel Terrón Morgado
* Ejercicio 17: Jesús Horno Cobo
* Ejercicio 18: Lourdes Díaz Mena
* 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: Miriam Núñez-Romero Olmo

Ejercicio 3

2013-05-08T13:30:50Z

Alebalher: Deshecha la edición 486 de Alebalher (disc.)

== 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: Alejandro Alfaro Martínez
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3: Salvador Joaquín Franco Peña
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5: Pedro Ros Reina
* Ejercicio 6: Carmen Martinez Navarro
* Ejercicio 7: Ana Rocío del Valle
* Ejercicio 8:
* Ejercicio 9: Francisco Nieto Rueda
* 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: Alejandro Ballesteros Hernandez
* Ejercicio 15: Elena Villalba Calderón
* Ejercicio 16: Miguel Ángel Terrón Morgado
* Ejercicio 17: Jesús Horno Cobo
* Ejercicio 18: Lourdes Díaz Mena
* 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: Miriam Núñez-Romero Olmo

Ejercicio 3

2013-05-08T13:27:30Z

Alebalher: /* Selección del ejercicio */

Ejercicio 3

2013-05-08T12:57:12Z

Alebalher: /* 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: Alejandro Alfaro Martínez
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3: Salvador Joaquín Franco Peña
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5: Pedro Ros Reina
* Ejercicio 6: Carmen Martinez Navarro
* Ejercicio 7: Ana Rocío del Valle
* Ejercicio 8:
* Ejercicio 9: Francisco Nieto Rueda
* 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: Alejandro Ballesteros Hernandez
* Ejercicio 15: Elena Villalba Calderón
* Ejercicio 16: Miguel Ángel Terrón Morgado
* Ejercicio 17: Jesús Horno Cobo
* Ejercicio 18: Lourdes Díaz Mena
* 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: Miriam Núñez-Romero Olmo

Ejercicio 2

2013-04-25T14:24:33Z

Alebalher:

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

== Selección del ejercicio ==

* Ejercicio 1: Francisco Vilches Chacón
* Ejercicio 2: Ana Rocío del Valle Benavides
* Ejercicio 3: Salvador Joaquín Franco Peña
* Ejercicio 4: Alejandro Ballesteros Hernández
* Ejercicio 5: Concepción García Vidal
* Ejercicio 6: Mª Carmen Delgado Muñoz
* Ejercicio 7: Jesús Horno Cobo
* Ejercicio 8: Inmaculada Arjona Arjona
* Ejercicio 9: Francisco Nieto Rueda
* Ejercicio 10: Carmen Martínez Navarro
* Ejercicio 11: Pedro José Perea Rojo
* Ejercicio 12: José Antonio Jaime Sabín
* Ejercicio 13: Gonzalo José Muñoz González-Meneses
* Ejercicio 14: Alejandro Alfaro Martínez
* Ejercicio 15: Elena Villalba Calderón
* Ejercicio 16:
* Ejercicio 17: Miriam Núñez-Romero Olmo
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20: Miguel Ángel Terrón Morgado
* Ejercicio 21: Lourdes Díaz Mena
* Ejercicio 22: Erlinda Menéndez Pérez
* Ejercicio 23: Irene Araujo Guijo
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José Mª Contreras Beltrán
* Ejercicio 27: FºJavier Sanz Gil
* Ejercicio 28: Isabel Duarte Tosso
* Ejercicio 29:
* Ejercicio 30:
* Ejercicio 31: Antonio Jesús Molero del Río
* Ejercicio 32: Mª de los Remedios Sillero Denamiel
* Ejercicio 33: Pedro Ros Reina

Relación 8

2013-04-24T11:26:43Z

Alebalher:

<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 0: 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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = False

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

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- dobleNegación :: Prop -> Bool
-- tal que (dobleNegación f) se verifica si f es una doble negación. Por
-- ejemplo,
-- dobleNegación (no (no p)) ==> True
-- dobleNegación (no (p --> q)) ==> False
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = False

-- ---------------------------------------------------------------------
-- 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
else False

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

-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]

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

expansiónDN :: [Prop] -> Prop -> [[Prop]]
expansiónDN fs f = undefined

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

expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
expansiónAlfa fs f = undefined

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

expansiónBeta :: [Prop] -> Prop -> [[Prop]]
expansiónBeta 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 fs = 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 fs = 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>

Relación 8

2013-04-24T11:24:32Z

Alebalher:

<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 0: 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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = False

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

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- dobleNegación :: Prop -> Bool
-- tal que (dobleNegación f) se verifica si f es una doble negación. Por
-- ejemplo,
-- dobleNegación (no (no p)) ==> True
-- dobleNegación (no (p --> q)) ==> False
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = False

-- ---------------------------------------------------------------------
-- 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
else False

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

-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]

-- Alejandro ballesteros
tieneContradiccion :: [Prop] -> Bool
tieneContradiccion []= False
tieneContradiccion (x:xs) =(elem (no (x)) xs)||(tieneContradiccion xs)
tc :: [Prop] -> Bool
tc xs = tieneContradiccion xs || tieneContradiccion (reverse xs)

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

expansiónDN :: [Prop] -> Prop -> [[Prop]]
expansiónDN fs f = undefined

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

expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
expansiónAlfa fs f = undefined

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

expansiónBeta :: [Prop] -> Prop -> [[Prop]]
expansiónBeta 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 fs = 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 fs = 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>

Relación 6

2013-03-21T17:53:18Z

Alebalher:

<source lang="isar">
text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}
-- "En clase"

lemma ejercicio_1a:
assumes "∀x. (H(x) ⟶ M(x))"
"H(s)"
shows "M(s)"
proof -
have 0: "H(s) ⟶ M(s)" using assms(1) ..
thus "M(s)" using assms(2) ..
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_2a:
assumes 0:"(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. (I(x)∧T(x))"
oops
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor

------------------------------------------------------------------ *}
-- "Alejandro Ballesteros"
lemma ejercicio_3a:
assumes 0: "(∀x.(P(x)⟶V(x))"
1: "(∃x.(V(x)∧∀y.(V(y)⟶x=y))"
shows "∃x.(P(x)∧∀y.(P(y)⟶x=y))"
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}
-- "Alejandro Ballesteros"
lemma ejercicio_4a:
assumes 0: "(∀x.(E(x)∧¬V(x)⟶∃y.(Ca(y,x)∧A(y)))"
1: "(∃x.(Co(x)∧E(x)∧∃y.(Ca(y,x)∧Co(y)))"
2: "(∀x.(Co(x)⟶¬V(x)))"
shows "∃x.(A(x)∧Co(x))"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

-- Antonio Jesús Molero

lemma
assumes "T(j,m)"
"T(j,p)"
shows "∃ x. ( T(x,m) ∧ T(x,p)) "
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
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.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}
-- "Reme Sillero"

lemma
assumes "∀ x. ∀ y. ((Af(x) & E(y))⟶ Ap(x,y)) "
"∀y. (E(y) ⟶ (¬Ap(j,y)))"
shows "(∃x. (E(x) ∧ N(x))) ⟶(¬Af(j))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

-- Antonio Jesús Molero

lemma
assumes " ∀ x. (¬R(x) ⟶ R(P(x)))"
shows "∃x. (R(x) ∧ R(P (P(x))))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}
-- "Reme Sillero"
lemma
assumes "∀x. ∀y. ((H(x) ∧ P(x) ∧ P(y))⟶ A(x,y))"
shows "∀x. ((H(x)∧ P(x))⟶A(x,x))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 6

2013-03-21T17:08:21Z

Alebalher:

<source lang="isar">
text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}
-- "En clase"

lemma ejercicio_1a:
assumes "∀x. (H(x) ⟶ M(x))"
"H(s)"
shows "M(s)"
proof -
have 0: "H(s) ⟶ M(s)" using assms(1) ..
thus "M(s)" using assms(2) ..
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_2a:
assumes 0:"(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. (I(x)∧T(x))"
oops
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor

------------------------------------------------------------------ *}
-- "Alejandro Ballesteros"
lemma ejercicio_3a:
assumes 0: "(∀x.(P(x)⟶V(x))"
1: "(∃x.(V(x)∧∀y.(V(y)⟶x=y))"
shows "∃x.(P(x)∧∀y.(P(y)⟶x=y))"
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

-- Antonio Jesús Molero

lemma
assumes "T(j,m)"
"T(j,p)"
shows "∃ x. ( T(x,m) ∧ T(x,p)) "
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
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.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}
-- "Reme Sillero"

lemma
assumes "∀ x. ∀ y. ((Af(x) & E(y))⟶ Ap(x,y)) "
"∀y. (E(y) ⟶ (¬Ap(j,y)))"
shows "(∃x. (E(x) ∧ N(x))) ⟶(¬Af(j))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

-- Antonio Jesús Molero

lemma
assumes " ∀ x. (¬R(x) ⟶ R(P(x)))"
shows "∃x. (R(x) ∧ R(P (P(x))))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}
-- "Reme Sillero"
lemma
assumes "∀x. ∀y. ((H(x) ∧ P(x) ∧ P(y))⟶ A(x,y))"
shows "∀x. ((H(x)∧ P(x))⟶A(x,x))"
using assms by auto

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>