https://www.glc.us.es/~jalonso/RA2013/index.php?action=history&feed=atom&title=R10 2026-07-17T14:41:20Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/RA2013/index.php?title=R10&diff=654&oldid=prev 2018-07-16T15:46:08Z

<p>Texto reemplazado: «isar» por «isabelle»</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 15:46 16 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>&lt;source lang=&quot;<del class="diffchange diffchange-inline">isar</del>&quot;&gt;</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>&lt;source lang=&quot;<ins class="diffchange diffchange-inline">isabelle</ins>&quot;&gt;</div></td></tr> <tr><td class='diff-marker'>&#160;</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 {* R10: Deducción natural proposicional *}</div></td><td class='diff-marker'>&#160;</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 {* R10: Deducción natural proposicional *}</div></td></tr> <tr><td class='diff-marker'>&#160;</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'>&#160;</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>

WikiSysop https://www.glc.us.es/~jalonso/RA2013/index.php?title=R10&diff=465&oldid=prev 2014-01-24T06:03:33Z

<p>Protegió «<a href="/~jalonso/RA2013/index.php/R10" title="R10">R10</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 06:03 24 ene 2014</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/RA2013/index.php?title=R10&diff=464&oldid=prev 2014-01-24T06:03:15Z

<p>Página creada con &#039;&lt;source lang=&quot;isar&quot;&gt; header {* R10: Deducción natural proposicional *} theory R10 imports Main begin text {* --------------------------------------------------------------...&#039;</p> <p><b>Página nueva</b></p><div>&lt;source lang=&quot;isar&quot;&gt;<br /> header {* R10: Deducción natural proposicional *}<br /> <br /> theory R10<br /> imports Main <br /> begin<br /> <br /> text {*<br /> --------------------------------------------------------------------- <br /> El objetivo de esta relación es lemas usando sólo las reglas básicas<br /> de deducción natural de la lógica proposicional. <br /> <br /> Los ejercicios son los de la asignatura de &quot;Lógica informática&quot; que se<br /> encuentran en http://goo.gl/yrPLn<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 /> · excluded_middle: ¬P ∨ 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: &quot;P ⟹ ¬¬ P&quot;<br /> by auto<br /> <br /> lemma mt: &quot;⟦F ⟶ G; ¬G⟧ ⟹ ¬F&quot;<br /> by auto<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 1. Demostrar<br /> p ∨ q, ¬q ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 2. Demostrar<br /> p ∧ q ⊢ ¬(¬p ∨ ¬q)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 3. Demostrar<br /> ¬(p ∨ q) ⊢ ¬p ∧ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 4. Demostrar<br /> ¬p ∧ ¬q ⊢ ¬(p ∨ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 5. Demostrar<br /> ¬p ∨ ¬q ⊢ ¬(p ∧ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 6. Demostrar<br /> ⊢ ((p ⟶ q) ⟶ p) ⟶ p<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 7. Demostrar<br /> ¬q ⟶ ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 8. Demostrar<br /> ¬(¬p ∧ ¬q) ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 9. Demostrar<br /> ¬(¬p ∨ ¬q) ⊢ p ∧ q<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 10. Demostrar<br /> ¬(p ∧ q) ⊢ ¬p ∨ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 11. Demostrar<br /> ⊢ (p ⟶ q) ∨ (q ⟶ p)<br /> ------------------------------------------------------------------ *}<br /> <br /> end<br /> &lt;/source&gt;</div>

Jalonso