Proving facts about I
Michael J. Miller, Donald R. Perlis · International Joint Conference on Artificial Intelligence · 1987
We study the Knights and Knaves problem, and find that for a proper treatment via theorem-proving, an interaction with natural language processing research is helpful. In particular, we discuss Ohlbach's claim that first-order logic is not well suited to handling this problem. Then we provide another interpretation of the problem using indexicals, and axiomatize it so that the desired result follows. We conclude by suggesting a broader context for dealing with self-utterances in automatic theorem-proving. Fuller details of automated proofs are given in a longer paper.