LMF2014: Primer examen
En la clase de hoy del curso Lógica matemática y fundamentos se ha realizado el primer examen.
Las soluciones de los ejercicios de la primera parte, de programción con Haskell, son
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 |
-- --------------------------------------------------------------------- -- § Librerías auxiliares -- -- --------------------------------------------------------------------- import Data.List -- --------------------------------------------------------------------- -- Gramática de fórmulas prosicionales -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Se definen los siguientes tipos de datos: -- * SimboloProposicional para representar los símbolos de proposiciones -- * Prop para representar las fórmulas proposicionales usando los -- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas -- atómicas, negaciones, conjunciones, implicaciones y equivalencias, -- respectivamente. -- --------------------------------------------------------------------- type SimboloProposicional = String data Prop = Atom SimboloProposicional | Neg Prop | Conj Prop Prop | Disj Prop Prop | Impl Prop Prop | Equi Prop Prop deriving (Eq,Ord) instance Show Prop where show (Atom p) = p show (Neg p) = "no " ++ show p show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")" show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")" show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")" show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")" -- --------------------------------------------------------------------- -- Se definen las siguientes fórmulas proposicionales -- atómicas: p, p1, p2, q, r, s, t y u. -- --------------------------------------------------------------------- p, p1, p2, q, r, s, t, u :: Prop p = Atom "p" p1 = Atom "p1" p2 = Atom "p2" q = Atom "q" r = Atom "r" s = Atom "s" t = Atom "t" u = Atom "u" -- --------------------------------------------------------------------- -- Se define la función -- no :: Prop -> Prop -- tal que (no f) es la negación de f. -- --------------------------------------------------------------------- no :: Prop -> Prop no = Neg -- --------------------------------------------------------------------- -- Se definen los siguientes operadores -- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop -- tales que -- f /\ g es la conjunción de f y g -- f \/ g es la disyunción de f y g -- f --> g es la implicación de f a g -- f <--> g es la equivalencia entre f y g -- --------------------------------------------------------------------- infixr 5 \/ infixr 4 /\ infixr 3 --> infixr 2 <--> (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop (/\) = Conj (\/) = Disj (-->) = Impl (<-->) = Equi -- --------------------------------------------------------------------- -- Ejercicio 1: Definir la función -- subformulas:: Prop -> [Prop] -- tal que (subformulas f) es la lista con las subfórmulas de f. Por -- ejemplo, -- subformulas ((p \/ q) /\ ((no q) \/ r)) == -- [((p \/ q) /\ (no q \/ r)),(p \/ q),p,q,(no q \/ r),no q,r] -- --------------------------------------------------------------------- subformulas :: Prop -> [Prop] subformulas (Atom f) = [Atom f] subformulas (Neg f) = Neg f : subformulas f subformulas (Conj f g) = Conj f g : union (subformulas f) (subformulas g) subformulas (Disj f g) = Disj f g : union (subformulas f) (subformulas g) subformulas (Impl f g) = Impl f g : union (subformulas f) (subformulas g) subformulas (Equi f g) = Equi f g : union (subformulas f) (subformulas g) -- --------------------------------------------------------------------- -- Interpretaciones -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Se define el tipo de datos Interpretación para representar las -- interpretaciones como listas de pares (átomo,booleano). -- --------------------------------------------------------------------- type Interpretacion = [(Prop,Bool)] -- --------------------------------------------------------------------- -- Significado de una fórmula en una interpretación -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 2: Definir la función -- significado :: Prop -> Interpretacion -> Bool -- tal que (significado f i) es el significado de f en i. Por ejemplo, -- significado ((p \/ q) /\ ((no q) \/ r)) [(r,True),(p,False),(q,False)] -- ==> False -- significado ((p \/ q) /\ ((no q) \/ r)) [(r,True),(p,True),(q,False)] -- ==> True -- --------------------------------------------------------------------- significado :: Prop -> Interpretacion -> Bool significado (Atom f) i = head [b |(a,b) <- i, a == Atom f] significado (Neg f) i = not (significado f i) significado (Conj f g) i = significado f i && significado g i significado (Disj f g) i = significado f i || significado g i significado (Impl f g) i = significado (Disj (Neg f) g) i significado (Equi f g) i = (significado (Impl f g) i) && (significado (Impl f g) i) |
Las soluciones de los ejercicios de la segunda parte, de demostración con Isabelle, son
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 |
theory examen_1 imports Main begin text {* --------------------------------------------------------------------- Las reglas básicas de la deducción natural son las siguientes: · conjI: ⟦P; Q⟧ ⟹ P ∧ Q · conjunct1: P ∧ Q ⟹ P · conjunct2: P ∧ Q ⟹ Q · notnotD: ¬¬ P ⟹ P · notnotI: P ⟹ ¬¬ P · mp: ⟦P ⟶ Q; P⟧ ⟹ Q · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F · impI: (P ⟹ Q) ⟹ P ⟶ Q · disjI1: P ⟹ P ∨ Q · disjI2: Q ⟹ P ∨ Q · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R · FalseE: False ⟹ P · notE: ⟦¬P; P⟧ ⟹ R · notI: (P ⟹ False) ⟹ ¬P · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q · iffD1: ⟦Q = P; Q⟧ ⟹ P · iffD2: ⟦P = Q; Q⟧ ⟹ P · ccontr: (¬P ⟹ False) ⟹ P . excluded_middel: ¬P ∨ P --------------------------------------------------------------------- *} text {* Se pueden usar las reglas notnotI y mt que demostramos a continuación. *} lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text {* -------------------------------------------------- Ejercicio 1: Demostrar (p1 ⟶ p2) ∧ (q1 ⟶ q2) ⊢ (p1 ∧ q1 ⟶ p2 ∧ q2) -------------------------------------------------------- *} lemma e1: assumes "(p1 ⟶ p2) ∧ (q1 ⟶ q2)" shows "(p1 ∧ q1) ⟶ (p2 ∧ q2)" proof (rule impI) assume "p1 ∧ q1" then have "p1" by (rule conjunct1) have "p1 ⟶ p2" using assms by (rule conjunct1) then have "p2" using `p1` by (rule mp) have "q1" using `p1 ∧ q1` by (rule conjunct2) have "q1 ⟶ q2" using assms by (rule conjunct2) then have "q2" using `q1` by (rule mp) with `p2` show "p2 ∧ q2" by (rule conjI) qed text {* -------------------------------------------------- Ejercicio 2: Demostrar p ⟶ r, r ⟶ ¬q ⊢ ¬(p∧q) -------------------------------------------------------- *} lemma e2: assumes "p ⟶ r" "r ⟶ ¬q" shows "¬(p∧q)" proof assume "p∧q" then have "q" by (rule conjunct2) have "p" using `p∧q` by (rule conjunct1) with `p ⟶ r` have "r" by (rule mp) with `r ⟶ ¬q` have "¬q" by (rule mp) then show False using `q` by (rule notE) qed end |