{"id":4210,"date":"2014-03-14T19:04:45","date_gmt":"2014-03-14T18:04:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4210"},"modified":"2014-03-26T19:07:03","modified_gmt":"2014-03-26T18:07:03","slug":"lmf2014-primer-examen","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-primer-examen\/","title":{"rendered":"LMF2014: Primer examen"},"content":{"rendered":"<p>En la  clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a>  se ha realizado el primer examen.<\/p>\n<p>Las soluciones de los ejercicios de la primera parte, de programci\u00f3n con Haskell, son<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\n-- ---------------------------------------------------------------------\r\n-- \u00a7 Librer\u00edas auxiliares                                             --\r\n-- ---------------------------------------------------------------------\r\n\r\nimport Data.List \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Gram\u00e1tica de f\u00f3rmulas prosicionales                                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Se definen los siguientes tipos de datos:\r\n-- * SimboloProposicional para representar los s\u00edmbolos de proposiciones\r\n-- * Prop para representar las f\u00f3rmulas proposicionales usando los\r\n--   constructores Atom, Neg, Conj, Disj, Impl y Equi para las f\u00f3rmulas\r\n--   at\u00f3micas, negaciones, conjunciones, implicaciones y equivalencias,\r\n--   respectivamente.  \r\n-- ---------------------------------------------------------------------\r\n\r\ntype SimboloProposicional = String\r\n\r\ndata Prop = Atom SimboloProposicional\r\n          | Neg Prop \r\n          | Conj Prop Prop \r\n          | Disj Prop Prop \r\n          | Impl Prop Prop \r\n          | Equi Prop Prop \r\n          deriving (Eq,Ord)\r\n\r\ninstance Show Prop where\r\n    show (Atom p)   = p\r\n    show (Neg p)    = \"no \" ++ show p\r\n    show (Conj p q) = \"(\" ++ show p ++ \" \/\\\\ \" ++ show q ++ \")\"\r\n    show (Disj p q) = \"(\" ++ show p ++ \" \\\\\/ \" ++ show q ++ \")\"\r\n    show (Impl p q) = \"(\" ++ show p ++ \" --> \" ++ show q ++ \")\"\r\n    show (Equi p q) = \"(\" ++ show p ++ \" <--> \" ++ show q ++ \")\"\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Se definen las siguientes f\u00f3rmulas proposicionales\r\n-- at\u00f3micas: p, p1, p2, q, r, s, t y u.\r\n-- ---------------------------------------------------------------------\r\n\r\np, p1, p2, q, r, s, t, u :: Prop\r\np  = Atom \"p\"\r\np1 = Atom \"p1\"\r\np2 = Atom \"p2\"\r\nq  = Atom \"q\"\r\nr  = Atom \"r\"\r\ns  = Atom \"s\"\r\nt  = Atom \"t\"\r\nu  = Atom \"u\"\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Se define la funci\u00f3n\r\n--    no :: Prop -> Prop\r\n-- tal que (no f) es la negaci\u00f3n de f.\r\n-- ---------------------------------------------------------------------\r\n\r\nno :: Prop -> Prop\r\nno = Neg\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Se definen los siguientes operadores\r\n--    (\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\r\n-- tales que\r\n--    f \/\\ g      es la conjunci\u00f3n de f y g\r\n--    f \\\/ g      es la disyunci\u00f3n de f y g\r\n--    f --> g     es la implicaci\u00f3n de f a g\r\n--    f <--> g    es la equivalencia entre f y g\r\n-- ---------------------------------------------------------------------\r\n\r\ninfixr 5 \\\/\r\ninfixr 4 \/\\\r\ninfixr 3 -->\r\ninfixr 2 <-->\r\n(\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\r\n(\/\\)   = Conj\r\n(\\\/)   = Disj\r\n(-->)  = Impl\r\n(<-->) = Equi\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir la funci\u00f3n \r\n--    subformulas:: Prop -> [Prop]\r\n-- tal que (subformulas f) es la lista con las subf\u00f3rmulas de f. Por\r\n-- ejemplo, \r\n--    subformulas ((p \\\/ q) \/\\ ((no q) \\\/ r)) ==\r\n--    [((p \\\/ q) \/\\ (no q \\\/ r)),(p \\\/ q),p,q,(no q \\\/ r),no q,r]\r\n-- ---------------------------------------------------------------------\r\n\r\nsubformulas :: Prop -> [Prop]\r\nsubformulas (Atom f)   = [Atom f]\r\nsubformulas (Neg f)    = Neg f : subformulas f\r\nsubformulas (Conj f g) = Conj f g : union (subformulas f) (subformulas g)\r\nsubformulas (Disj f g) = Disj f g : union (subformulas f) (subformulas g)\r\nsubformulas (Impl f g) = Impl f g : union (subformulas f) (subformulas g)\r\nsubformulas (Equi f g) = Equi f g : union (subformulas f) (subformulas g) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Interpretaciones                                                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Se define el tipo de datos Interpretaci\u00f3n para representar las\r\n-- interpretaciones como listas de pares (\u00e1tomo,booleano).\r\n-- ---------------------------------------------------------------------\r\n\r\ntype Interpretacion = [(Prop,Bool)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Significado de una f\u00f3rmula en una interpretaci\u00f3n                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir la funci\u00f3n\r\n--    significado :: Prop -> Interpretacion -> Bool\r\n-- tal que (significado f i) es el significado de f en i. Por ejemplo,\r\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [(r,True),(p,False),(q,False)]    \r\n--    ==>  False\r\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [(r,True),(p,True),(q,False)]  \r\n--    ==>  True\r\n-- ---------------------------------------------------------------------\r\n\r\nsignificado :: Prop -> Interpretacion -> Bool\r\nsignificado (Atom f) i = head [b |(a,b) <- i, a == Atom f]\r\nsignificado (Neg f) i    = not (significado f i)\r\nsignificado (Conj f g) i = significado f i &#038;&#038; significado g i\r\nsignificado (Disj f g) i = significado f i || significado g i\r\nsignificado (Impl f g) i = significado (Disj (Neg f) g) i\r\nsignificado (Equi f g) i = (significado (Impl f g) i) &#038;&#038; (significado (Impl f g) i)\r\n<\/pre>\n<p>Las soluciones de los ejercicios de la segunda parte, de demostraci\u00f3n con Isabelle, son<\/p>\n<pre lang=\"isar\">\r\ntheory  examen_1\r\nimports Main\r\nbegin\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Las reglas b\u00e1sicas de la deducci\u00f3n natural son las siguientes:\r\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \r\n  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\r\n  \u00b7 notnotI:    P \u27f9 \u00ac\u00ac P\r\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \r\n  \u00b7 mt:         \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \r\n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\r\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \r\n  \u00b7 FalseE:     False \u27f9 P\r\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\r\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\r\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\r\n  . excluded_middel: \u00acP \u2228 P \r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\ntext {*\r\n  Se pueden usar las reglas notnotI y mt que demostramos a continuaci\u00f3n. *}\r\n\r\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\r\nby auto\r\n\r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n\r\ntext {* --------------------------------------------------\r\n  Ejercicio 1: Demostrar \r\n     (p1 \u27f6 p2) \u2227 (q1 \u27f6 q2) \u22a2 (p1 \u2227 q1 \u27f6 p2 \u2227 q2)\r\n  -------------------------------------------------------- *}\r\n\r\nlemma e1:\r\n  assumes \"(p1 \u27f6 p2) \u2227 (q1 \u27f6 q2)\"\r\n  shows \"(p1 \u2227 q1) \u27f6 (p2 \u2227 q2)\"\r\nproof (rule impI)\r\n  assume \"p1 \u2227 q1\"\r\n  then have \"p1\" by (rule conjunct1)\r\n  have \"p1 \u27f6 p2\" using assms by (rule conjunct1)\r\n  then have \"p2\" using `p1` by (rule mp)\r\n  have \"q1\" using `p1 \u2227 q1` by (rule conjunct2)\r\n  have \"q1 \u27f6 q2\" using assms by (rule conjunct2)\r\n  then have \"q2\" using `q1` by (rule mp)\r\n  with `p2` show \"p2 \u2227 q2\" by (rule conjI)\r\nqed\r\n   \r\ntext {* --------------------------------------------------\r\n  Ejercicio 2: Demostrar\r\n     p \u27f6 r, r \u27f6 \u00acq  \u22a2 \u00ac(p\u2227q)\r\n  -------------------------------------------------------- *}\r\n\r\nlemma e2:\r\n  assumes \"p \u27f6 r\"\r\n          \"r \u27f6 \u00acq\"\r\n  shows \"\u00ac(p\u2227q)\"\r\nproof \r\n  assume \"p\u2227q\"\r\n  then have \"q\" by (rule conjunct2)\r\n  have \"p\" using `p\u2227q` by (rule conjunct1)\r\n  with `p \u27f6 r` have \"r\" by (rule mp)\r\n  with `r \u27f6 \u00acq` have \"\u00acq\" by (rule mp)\r\n  then show False using `q` by (rule notE)\r\nqed\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha realizado el primer examen. Las soluciones de los ejercicios de la primera parte, de programci\u00f3n con Haskell, son<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[234],"tags":[270,144,303,189],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4210"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4210"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4210\/revisions"}],"predecessor-version":[{"id":4211,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4210\/revisions\/4211"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4210"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4210"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4210"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}