https://www.glc.us.es/~jalonso/DAO2011/index.php?action=history&feed=atom&title=Tema_3_ej
Tema 3 ej - Historial de revisiones
2026-07-19T01:04:09Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/DAO2011/index.php?title=Tema_3_ej&diff=78&oldid=prev
Jalonso en 18:18 15 jul 2018
2018-07-15T18:18:20Z
<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:18 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 {* Deducción natural 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 {* Deducción natural 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/DAO2011/index.php?title=Tema_3_ej&diff=36&oldid=prev
Jalonso: Protegió «Tema 3 ej» ([edit=sysop] (indefinido) [move=sysop] (indefinido))
2011-03-29T11:46:43Z
<p>Protegió «<a href="/~jalonso/DAO2011/index.php/Tema_3_ej" title="Tema 3 ej">Tema 3 ej</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 11:46 29 mar 2011</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/DAO2011/index.php?title=Tema_3_ej&diff=35&oldid=prev
Jalonso: Página creada con '<source lang="isar"> header {* Deducción natural proposicional *} theory Tema_3_ej imports Main begin text {* Los ejercicios de esta relación deben de resolverse usando s...'
2011-03-29T11:46:34Z
<p>Página creada con '<source lang="isar"> header {* Deducción natural proposicional *} theory Tema_3_ej imports Main begin text {* Los ejercicios de esta relación deben de resolverse usando s...'</p>
<p><b>Página nueva</b></p><div><source lang="isar"><br />
header {* Deducción natural proposicional *}<br />
<br />
theory Tema_3_ej<br />
imports Main <br />
begin <br />
<br />
text {* Los ejercicios de esta relación deben de resolverse usando sólo<br />
las reglas básicas de la deducción natural proposicional: <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 />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
lemma ejercicio_1:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
oops<br />
<br />
lemma ejercicio_2:<br />
assumes 1: "p⟶q" and <br />
2: "q⟶r" and <br />
3: "p" <br />
shows "r"<br />
oops<br />
<br />
lemma ejercicio_3:<br />
assumes 1: "p⟶(q⟶r)" and <br />
2: "p⟶q" and <br />
3: "p"<br />
shows "r"<br />
oops<br />
<br />
lemma ejercicio_4:<br />
assumes 1: "p⟶q" and <br />
2: "q⟶r" <br />
shows "p⟶r"<br />
oops<br />
<br />
lemma ejercicio_5:<br />
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"<br />
oops<br />
<br />
lemma ejercicio_6:<br />
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"<br />
oops <br />
<br />
lemma ejercicio_7:<br />
"p ⟹ q⟶p"<br />
oops<br />
<br />
lemma ejercicio_8:<br />
"p⟶(q⟶p)"<br />
oops<br />
<br />
lemma ejercicio_9:<br />
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"<br />
oops<br />
<br />
lemma ejercicio_10:<br />
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"<br />
oops<br />
<br />
lemma ejercicio_11:<br />
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"<br />
oops<br />
<br />
lemma ejercicio_12:<br />
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"<br />
oops<br />
<br />
lemma ejercicio_13:<br />
"⟦p; q⟧ ⟹ p∧q"<br />
oops<br />
<br />
lemma ejercicio_14:<br />
"p∧q ⟹ p"<br />
oops<br />
<br />
lemma ejercicio_15:<br />
"p∧q ⟹ q"<br />
oops<br />
<br />
lemma ejercicio_16:<br />
"p∧(q∧r) ⟹ (p∧q)∧r"<br />
oops<br />
<br />
lemma ejercicio_17:<br />
"(p∧q)∧r ⟹ p∧(q∧r)"<br />
oops<br />
<br />
lemma ejercicio_18:<br />
"p∧q ⟹ p⟶q"<br />
oops<br />
<br />
lemma ejercicio_19:<br />
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"<br />
oops<br />
<br />
lemma ejercicio_20:<br />
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"<br />
oops<br />
<br />
lemma ejercicio_21:<br />
"p⟶(q⟶r) ⟹ p∧q⟶r"<br />
oops<br />
<br />
lemma ejercicio_22:<br />
"p∧q⟶r ⟹ p⟶(q⟶r)"<br />
oops<br />
<br />
lemma ejercicio_23:<br />
"(p⟶q)⟶r ⟹ p∧q⟶r"<br />
oops<br />
<br />
lemma ejercicio_24:<br />
"p∧(q⟶r) ⟹ (p⟶q)⟶r"<br />
oops<br />
<br />
lemma ejercicio_25:<br />
"p ⟹ p∨q"<br />
oops<br />
<br />
lemma ejercicio_26:<br />
"q ⟹ p∨q"<br />
oops<br />
<br />
lemma ejercicio_27:<br />
"p∨q ⟹ q∨p"<br />
oops<br />
<br />
lemma ejercicio_28:<br />
"q⟶r ⟹ p∨q⟶p∨r"<br />
oops<br />
<br />
lemma ejercicio_29:<br />
"p∨p ⟹ p"<br />
oops<br />
<br />
lemma ejercicio_30:<br />
"p ⟹ p∨p"<br />
oops<br />
<br />
lemma ejercicio_31:<br />
"p∨(q∨r) ⟹ (p∨q)∨r"<br />
oops<br />
<br />
lemma ejercicio_32:<br />
"(p∨q)∨r ⟹ p∨(q∨r)"<br />
oops<br />
<br />
lemma ejercicio_33:<br />
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"<br />
oops<br />
<br />
lemma ejercicio_34:<br />
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"<br />
oops<br />
<br />
lemma ejercicio_35:<br />
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"<br />
oops<br />
<br />
lemma ejercicio_36:<br />
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"<br />
oops<br />
<br />
lemma ejercicio_37:<br />
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"<br />
oops<br />
<br />
lemma ejercicio_38:<br />
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"<br />
oops<br />
<br />
lemma ejercicio_39:<br />
"p ⟹ ¬¬p"<br />
oops<br />
<br />
lemma ejercicio_40:<br />
"¬p ⟹ p⟶q"<br />
oops<br />
<br />
lemma ejercicio_41:<br />
"p⟶q ⟹ ¬q⟶¬p"<br />
oops<br />
<br />
lemma ejercicio_42:<br />
"⟦p∨q; ¬q⟧ ⟹ p"<br />
oops<br />
<br />
lemma ejercicio_43:<br />
"⟦p∨q; ¬p⟧ ⟹ q"<br />
oops<br />
<br />
lemma ejercicio_44:<br />
"p∨q ⟹ ¬(¬p∧¬q)"<br />
oops<br />
<br />
lemma ejercicio_45:<br />
"p∧q ⟹ ¬(¬p∨¬q)"<br />
oops<br />
<br />
lemma ejercicio_46:<br />
"¬(p∨q) ⟹ ¬p∧¬q"<br />
oops<br />
<br />
lemma ejercicio_47:<br />
"¬p∧¬q ⟹ ¬(p∨q)"<br />
oops<br />
<br />
lemma ejercicio_48:<br />
"¬p∨¬q ⟹ ¬(p∧q)"<br />
oops<br />
<br />
lemma ejercicio_49:<br />
"¬(p∧¬p)"<br />
oops<br />
<br />
lemma ejercicio_50:<br />
"p∧¬p ⟹ q"<br />
oops<br />
<br />
lemma ejercicio_51:<br />
"¬¬p ⟹ p"<br />
oops<br />
<br />
lemma ejercicio_52:<br />
"p∨¬p"<br />
oops<br />
<br />
lemma ejercicio_53:<br />
"((p⟶q)⟶p)⟶p"<br />
oops<br />
<br />
lemma ejercicio_54:<br />
"¬q⟶¬p ⟹ p⟶q"<br />
oops<br />
<br />
lemma ejercicio_55:<br />
"¬(¬p∧¬q) ⟹ p∨q"<br />
oops<br />
<br />
lemma ejercicio_56:<br />
"¬(¬p∨¬q) ⟹ p∧q"<br />
oops<br />
<br />
lemma ejercicio_57:<br />
"¬(p∧q) ⟹ ¬p∨¬q"<br />
oops<br />
<br />
lemma ejercicio_58:"(p⟶q)∨(q⟶p)"<br />
oops<br />
<br />
end <br />
</source></div>
Jalonso