https://www.glc.us.es/~jalonso/RA2013/index.php?action=history&feed=atom&title=R9 2026-07-17T08:12:47Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/RA2013/index.php?title=R9&diff=664&oldid=prev 2018-07-16T15:46:11Z

<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 {* R9: Deducción natural proposicional (1) *}</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 {* R9: Deducción natural proposicional (1) *}</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=R9&diff=422&oldid=prev 2014-01-16T19:03:41Z

<p>Protegió «<a href="/~jalonso/RA2013/index.php/R9" title="R9">R9</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 19:03 16 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=R9&diff=420&oldid=prev 2014-01-16T19:02:24Z

<p>Página creada con &#039;&lt;source lang=&quot;isar&quot;&gt; header {* R9: Deducción natural proposicional (1) *} theory R9 imports Main begin text {* ------------------------------------------------------------...&#039;</p> <p><b>Página nueva</b></p><div>&lt;source lang=&quot;isar&quot;&gt;<br /> header {* R9: Deducción natural proposicional (1) *}<br /> <br /> theory R9<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 /> Las reglas básicas de la deducción natural necesarias son las<br /> 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 /> --------------------------------------------------------------------- <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 /> section {* Implicaciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 1. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 2. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 3. Demostrar<br /> ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 4. Demostrar<br /> (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> section {* Conjunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 5. Demostrar<br /> (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 6. Demostrar<br /> p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 7. Demostrar<br /> p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> section {* Disyunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 8. Demostrar<br /> q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 9. Demostrar<br /> (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 10. Demostrar<br /> p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> end<br /> &lt;/source&gt;</div>

Jalonso