El problema del barbero
Decidir si es cierto que
Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie.
Se usará la siguiente simbolización:
- A(x,y) para x afeita a y
- C(x) para x es un habitante de Las Chinas
- c para Carlos
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 9 10 |
theory El_problema_del_barbero imports Main begin lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" oops end |
Soluciones con Isabelle/HOL
|
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 |
theory El_problema_del_barbero imports Main begin ― ‹La demostración automática es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" using assms by auto ― ‹La demostración estructurada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) .. have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" .. with 1 have "A(c,c)" .. with ‹¬A(c,c)› show False .. qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› .. then show "¬A(c,c)" .. qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› .. qed ― ‹La demostración detallada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE) have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI) with 1 have "A(c,c)" by (rule iffD2) with ‹¬A(c,c)› show False by (rule notE) qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› by (rule iffD1) then show "¬A(c,c)" by (rule conjunct2) qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› by (rule notE) qed end |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>
