In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle's hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist.
翻译:1982年,雷蒙德·斯穆利扬发表了一篇题为“塔尔博士和费瑟教授的庇护”的文章,由一系列谜题组成。这些谜题后来被重印在文理学中,“夫人还是老虎?”和其他逻辑谜题中。最后一个谜题描述了标题中提到的庇护,其设计特别困难。在自动化推理的帮助下,我们证明谜题的假设事实上是不一致的,也就是说,不可能存在这样的庇护。