Name
Abstract | ||
|---|---|---|
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 an interpretation of the problem using indexicals, axiomatize it, and prove the desired result. We conclude by suggesting a broader context for dealing with ‘self-utterances’ in automatic theorem-proving. |
Year | DOI | Venue |
|---|---|---|
1987 | 10.1007/BF00243796 | J. Autom. Reasoning |
Keywords | Field | DocType |
knowledge representation,first-order log!c,indexicals,situated logic,proving self-utterances,utterances.,theorem proving,first order logic,indexation,natural language processing,first order | Discrete mathematics,Knowledge representation and reasoning,Programming language,Computer science,Algorithm,First-order logic,Artificial intelligence,Knights and Knaves | Journal |
Volume | Issue | Citations |
3 | 3 | 1 |
PageRank | References | Authors |
0.43 | 5 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Miller | 1 | 7 | 0.85 |
| Donald Perlis | 2 | 306 | 54.22 |