Proving Self-Utterances

摘要

The Knights and Knaves problem is studied, and for a proper treatment via theorem-proving, an interaction with natural language processing research is helpful. In particular, discussed is Ohlbach's claim that first-order logic is not well suited to handling this problem. Then an interpretation is provided of the problem using indexicals, it is axiomatized and the desired result proved. A broader context for dealing with 'self-utterances' in automatic theorem-proving is suggested. Keywords: Indexicals, Knowledge representations, First order logic, Reprints, Situated logic, Utterances. (jhd)