La dama o el tigre
En el libro de Raymond Smullyan ¿La dama o el tigre? (en inglés, The lady or the tiger? se plantea el siguiente problema
Un rey somete a un prisionero a la siguiente prueba: lo enfrenta a dos
puertas, de las que el prisionero debe elegir una, y entrar la habitación correspondiente. Se informa al prisionero que en cada una de las habitaciones puede haber un tigre o una dama. Como es natural, el prisionero debe elegir la puerta que le lleva a la dama (entre otras cosas, para no ser devorado por el tigre). Para ayudarle, en cada puerta hay un letrero. El de la puerta 1 dice «en esta habitación hay una dama y en la otra un tigre» y el de la puerta 2 dice «en una de estas habitaciones hay una dama y en una de estas habitaciones hay un tigre».Sabiendo que uno de los carteles dice la verdad y el otro no, demostrar que la dama se encuentra en la segunda habitación.
Para la formalización del problema se usarán los siguientes símbolos
- c1 que representa el contenido del cartel de la puerta 1,
- c2 que representa el contenido del cartel de la puerta 2 ,
- dp que representa hay una dama en la primera habitación,
- tp que representa hay un tigre en la primera habitación,
- ds que representa hay una dama en la segunda habitación y
- ts que representa hay un tigre en la segunda habitación.
Demostrar con Isabelle/HOL que el argumento anterior es correcto.
Soluciones con Isabelle/HOL
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>
