TitleReasoning About Agent Types and the Hardest Logic Puzzle Ever
AuthorsLiu, Fenrong
Wang, Yanjing
AffiliationTsinghua 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.
KeywordsAgent types
Public announcement logic
Questioning strategy
Knight and Knaves
The hardest logic puzzle ever
Issue Date2013
Publisherminds and machines
CitationMINDS AND MACHINES.2013,23,(1,SI),123-161.
AbstractIn 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:哲学系(宗教学系)

Web of Science®

Checked on Last Week


Checked on Current Time


Checked on Current Time

Google Scholar™

License: See PKU IR operational policies.