An Impossible Asylum

TL;DR

This paper uses automated reasoning to analyze a complex logic puzzle about an asylum, demonstrating that the puzzle's hypotheses are inconsistent and such an asylum cannot exist.

Contribution

It introduces a novel application of automated reasoning to validate and analyze classic logic puzzles, revealing inconsistencies in the hypotheses.

Findings

The hypotheses of the puzzle are inconsistent.

Automated reasoning confirms the impossibility of the asylum.

The puzzle's assumptions cannot all be true simultaneously.

Abstract

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.