Rel 4 - Historial de revisiones

https://www.glc.us.es/~jalonso/DAO2012/index.php?action=history&feed=atom&title=Rel_4 Rel 4 - Historial de revisiones 2026-07-17T13:11:06Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_4&diff=123&oldid=prev Jalonso en 18:55 15 jul 2018 2018-07-15T18:55:30Z

<p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 18:55 15 jul 2018</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td> <td colspan="2" class="diff-lineno">Línea 1:</td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="<del class="diffchange diffchange-inline">isar</del>"></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="<ins class="diffchange diffchange-inline">isabelle</ins>"></div></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 4: Argumentación proposicional *}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 4: Argumentación proposicional *}</div></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> </table>

Jalonso https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_4&diff=64&oldid=prev Jalonso: Protegió «Rel 4» ([edit=sysop] (indefinido) [move=sysop] (indefinido)) 2012-12-18T21:55:47Z

<p>Protegió «<a href="/~jalonso/DAO2012/index.php/Rel_4" title="Rel 4">Rel 4</a>» ([edit=sysop] (indefinido) [move=sysop] (indefinido))</p> <table class="diff diff-contentalign-left" data-mw="interface"> <tr class="diff-title" lang="es"> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">Revisión del 21:55 18 dic 2012</td> </tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div> </td></tr></table>

Jalonso https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_4&diff=62&oldid=prev Jalonso en 21:54 18 dic 2012 2012-12-18T21:54:21Z

<p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 21:54 18 dic 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td> <td colspan="2" class="diff-lineno">Línea 1:</td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="isar></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="isar<ins class="diffchange diffchange-inline">"</ins>></div></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 4: Argumentación proposicional *}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 4: Argumentación proposicional *}</div></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> </table>

Jalonso https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_4&diff=61&oldid=prev Jalonso: Página creada con '<source lang="isar> header {* Relación 4: Argumentación proposicional *} theory R4 imports Main begin text {* ------------------------------------------------------------...' 2012-12-18T21:54:05Z

<p>Página creada con '<source lang="isar> header {* Relación 4: Argumentación proposicional *} theory R4 imports Main begin text {* ------------------------------------------------------------...'</p> <p><b>Página nueva</b></p><div><source lang="isar><br /> header {* Relación 4: Argumentación proposicional *}<br /> <br /> theory R4<br /> imports Main <br /> begin<br /> <br /> text {*<br /> --------------------------------------------------------------------- <br /> El objetivo de esta relación formalizar y demostrar la corrección de<br /> los argumentos usando sólo las reglas básicas de deducción natural de<br /> la lógica proposicional (sin usar el método auto). <br /> <br /> Las reglas básicas de la deducción natural son las siguientes:<br /> · conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br /> · conjunct1: P ∧ Q ⟹ P<br /> · conjunct2: P ∧ Q ⟹ Q <br /> · notnotD: ¬¬ P ⟹ P<br /> · notnotI: P ⟹ ¬¬ P<br /> · mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br /> · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br /> · impI: (P ⟹ Q) ⟹ P ⟶ Q<br /> · disjI1: P ⟹ P ∨ Q<br /> · disjI2: Q ⟹ P ∨ Q<br /> · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br /> · FalseE: False ⟹ P<br /> · notE: ⟦¬P; P⟧ ⟹ R<br /> · notI: (P ⟹ False) ⟹ ¬P<br /> · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br /> · iffD1: ⟦Q = P; Q⟧ ⟹ P <br /> · iffD2: ⟦P = Q; Q⟧ ⟹ P<br /> · ccontr: (¬P ⟹ False) ⟹ P<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {*<br /> Se usarán las reglas notnotI y mt que demostramos a continuación.<br /> *}<br /> <br /> lemma notnotI: "P ⟹ ¬¬ P"<br /> by auto<br /> <br /> lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br /> by auto<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Cuando tanto la temperatura como la presión atmosférica permanecen<br /> contantes, no llueve. La temperatura permanece constante. Por lo<br /> tanto, en caso de que llueva, la presión atmosférica no permanece<br /> constante. <br /> Usar T para "La temperatura permanece constante",<br /> P para "La presión atmosférica permanece constante" y<br /> L para "Llueve".<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_1:<br /> assumes "T ∧ P ⟶ ¬L" and<br /> "T"<br /> shows "L ⟶ ¬P"<br /> proof<br /> assume "L"<br /> show "¬P"<br /> proof<br /> assume "P"<br /> have "T ∧ P" using `T` `P` ..<br /> have "¬L" using assms(1) `T ∧ P` ..<br /> thus "False" using `L` .. <br /> qed<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Siempre que un número x es divisible por 10, acaba en 0. El número<br /> x no acaba en 0. Por lo tanto, x no es divisible por 10. <br /> Usar D para "el número es divisible por 10" y<br /> C para "el número acaba en cero".<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> En cierto experimento, cuando hemos empleado un fármaco A, el<br /> paciente ha mejorado considerablemente en el caso, y sólo en el<br /> caso, en que no se haya empleado también un fármaco B. Además, o se<br /> ha empleado el fármaco A o se ha empleado el fármaco B. En<br /> consecuencia, podemos afirmar que si no hemos empleado el fármaco<br /> B, el paciente ha mejorado considerablemente. <br /> Usar A: Hemos empleado el fármaco A.<br /> B: Hemos empleado el fármaco B.<br /> M: El paciente ha mejorado notablemente.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente<br /> argumento<br /> Si no está el mañana ni el ayer escrito, entonces no está el mañana<br /> escrito. <br /> Usar M: El mañana está escrito.<br /> A: El ayer está escrito.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Me matan si no trabajo y si trabajo me matan. Me matan siempre me<br /> matan. <br /> Usar M: Me matan.<br /> T: Trabajo.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si te llamé por teléfono, entonces recibiste mi llamada y no es<br /> cierto que no te avisé del peligro que corrías. Por consiguiente,<br /> como te llamé, es cierto que te avisé del peligro que corrías.<br /> Usar T: Te llamé por teléfono.<br /> R: Recibiste mi llamada.<br /> P: Te avisé del peligro que corrías.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si no hay control de nacimientos, entonces la población crece<br /> ilimitadamente; pero si la población crece ilimitadamente,<br /> aumentará el índice de pobreza. Por consiguiente, si no hay control<br /> de nacimientos, aumentará el índice de pobreza. <br /> Usar N: Hay control de nacimientos. <br /> P: La población crece ilimitadamente,<br /> I: Aumentará el índice de pobreza. <br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si el general era leal, hubiera obedecido las órdenes, y si era<br /> inteligente las hubiera comprendido. O el general desobedeció las<br /> órdenes o no las comprendió. Luego, el general era desleal o no era<br /> inteligente. <br /> Usar L: El general es leal.<br /> O: El general obedece las órdenes.<br /> I: El general es inteligente.<br /> C: El general comprende las órdenes.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo<br /> haría. Si Dios fuera incapaz de evitar el mal, no sería<br /> omnipotente; si no quisiera evitar el mal sería malévolo. Dios no<br /> evita el mal. Si Dios existe, es omnipotente y no es<br /> malévolo. Luego, Dios no existe. <br /> Usar C: Dios es capaz de evitar el mal.<br /> Q: Dios quiere evitar el mal.<br /> O: Dios es omnipotente.<br /> M: Dios es malévolo.<br /> P: Dios evita el mal.<br /> E: Dios existe.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Nadie más que Pedro, Quintín y Raúl están bajo sospecha y al menos<br /> uno es traidor. Pedro nunca trabaja sin llevar al menos un cómplice<br /> (que puede ser Quintín o Raúl). Raúl es leal. Por lo tanto,<br /> Pedro es traidor.<br /> Usar p: Pedro es traidor.<br /> q : Quintín es traidor.<br /> r : Raúl es traidor. <br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si la válvula está abierta o la monitorización está preparada,<br /> entonces se envía una señal de reconocimiento y un mensaje de<br /> funcionamiento al controlador del ordenador. Si se envía un mensaje <br /> de funcionamiento al controlador del ordenador o el sistema está en <br /> estado normal, entonces se aceptan las órdenes del operador. Por lo<br /> tanto, si la válvula está abierta, entonces se aceptan las órdenes<br /> del operador. <br /> Usar A: La válvula está abierta.<br /> P : La monitorización está preparada.<br /> R : Envía una señal de reconocimiento.<br /> F : Envía un mensaje de funcionamiento.<br /> N : El sistema está en estado normal.<br /> O : Se aceptan órdenes del operador.<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente<br /> argumento <br /> Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin<br /> embargo, si trabajo no gozo de la vida, mientras que si no trabajo<br /> no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano<br /> dinero. <br /> Usar p: Trabajo<br /> q: Gano dinero.<br /> r: Gozo de la vida.<br /> ------------------------------------------------------------------ *}<br /> <br /> end<br /> </source></div>

Jalonso