|Title||Reasoning About Agent Types and the Hardest Logic Puzzle Ever|
|Affiliation||Tsinghua Univ, Dept Philosophy, Beijing 100084, Peoples R China.|
Peking Univ, Dept Philosophy, Beijing 100871, Peoples R China.
Peking Univ, Inst Foreign Philosophy, Beijing 100871, Peoples R China.
Public announcement logic
Knight and Knaves
The hardest logic puzzle ever
|Publisher||minds and machines|
|Citation||MINDS AND MACHINES.2013,23,(1,SI),123-161.|
|Abstract||In this paper, we first propose a simple formal language to specify types of agents in terms of necessary conditions for their announcements. Based on this language, types of agents are treated as 'first-class citizens' and studied extensively in various dynamic epistemic frameworks which are suitable for reasoning about knowledge and agent types via announcements and questions. To demonstrate our approach, we discuss various versions of Smullyan's Knights and Knaves puzzles, including the Hardest Logic Puzzle Ever (HLPE) proposed by Boolos (in Harv Rev Philos 6:62-65, 1996). In particular, we formalize HLPE and verify a classic solution to it. Moreover, we propose a spectrum of new puzzles based on HLPE by considering subjective (knowledge-based) agent types and relaxing the implicit epistemic assumptions in the original puzzle. The new puzzles are harder than the previously proposed ones in the literature, in the sense that they require deeper epistemic reasoning. Surprisingly, we also show that a version of HLPE in which the agents do not know the others' types does not have a solution at all. Our formalism paves the way for studying these new puzzles using automatic model checking techniques.|
|Appears in Collections:||哲学系（宗教学系）|