Proving Facts about " "
Proceedings of the Tenth International Joint Conference on Artificial Intelligence. Knowledge Representation. Pages 499-500.
© 1987 International Joint Conferences on Artificial Intelligence
Abstract
We study the Knight1. and Knave~ 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 "selfutterances" in automatic theorem-proving. Fuller details of automated proofs are · given in a longer paper.
- Allen, J. [1984] Toward a general theory of action and time, Artificial Intelligence, Vol. 23, 123-154.
- Allen, J . and Perrault, R. [1980] Analyzing intentions in utterances, Artificial Intelligence, Vol. 15, 143-178.
- Barwise, J. and Perry, J. [1983] Situation• and Attitudea. MIT Press, Cambridge, Mas- sachusetts.
- Harper, M. and Charniak, E. [1986], Proceed- ing•, ACL Annual Meeting.
- Miller, M. and Perlis, D. (1987] Proving self- utterances. Submitted for publication, Journal of Automated Reuoning.
- Ohlbach, H. J. [1985] Predicate logic hacker tricks, J. of Automated Reaaoning Vol. 1, No. 4, 435-440.
- Perlis, D. [1985] Languages with self reference I, Artificial Intelligence, Vol. 25, 301-322.
- Smith, B. [1985] Varieties of self-reference. Proceeding•, Theoretical Aapecta of Reuoning About Knowledge, ed. J . Halpern. (9)
- Smullyan, R. [1978] What ia tile Name of thia BooH. Prentice-Hall, Englewood Cliffs, N.J.
References were extracted automatically from the PDF and may contain errors.
Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.
PROVING FACTS ABOUT "I"
Michael Millera,b and Donald Perlisa.·
-computer Science Department bSystems Research Center
·Institute for Advanced Computer Studies
University -of Maryland College,Park, Maryland USA 20742
ABSTRACT
We study the Knight1. and Knave~ 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 han dling this problem. Then we provide another interpre tation 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.
I. INTRODUCTION
The Knighte and Knaves problem [Smullyan 1978J can be stated as follows: An island exists whose only inhabitants are knights, knaves, and a princess. The knights on the island always tell the truth, while the knaves always lie. Some of the knights are poor and the rest of them are rich. The same holds for the knaves. The princess is looking for a husband who must be a rich knave. In uttering one statement, how can a rich knave convince the princess that he is indeed a prospective husband for her?'
[Ohlbach 1985J is devoted to the framing and solution of this problem in a formal theorem-proving context using first-order logic (FOL ). Though trying to write the problem in FOL may not appear to be difficult at first, it is shown by Ohlbach not to be entirely elementary. He examines, and finds inade quate, two different approaehes before he finally settles on a third. This final approach, though successful in that it gets the desired "solution", is unsatisfactory because it involves constructs not faithfully related to the original problem.
This research hu been supported in part by the followina in stitutions:
National Science Foundation Grant *OIR-8500108
The U.S. Army Research Oft'lce (DAA�~S&-K-0177)
The Martin Marietta Corporation
'The Intended solution is the statement "I am a poor tnan" (or aa used below, "I am not-rich and a knave"). The reader can readily verify that this indeed is a aolution. Note the self-referential nature of the statement; this feature is a special cue or indexict.lity, which we addreaa below. For aeneral treatments of self-reference, see iPerlis 19861, where another of Smullyan's puzzles is treated, and !Smith 111861.
We contend that there is a straightforward treat ment of the problem that is faithful to its intent and that does allow a formal proof of the desired result. However, it requires employing concepts into the for malism that are not usually found in the context of problem-solving via resolution theorem-provers, namely ideas from natural language processing. Nevertheless, we are not replacing one trick by another, but rather introducing a well-understood and general formalism for problems of this sort.
D. PROBLEM REPRESENTATION
Finding a suitable representation for problems in artificial intelligence (AI) is often a difficult task . . However, the formo.liem used to represent a problem is not necessarily the cause of the difficulty, though we grant that sometimes it is. Often it is the problem itself that is resisting representation and, when this occurs further insight into the problem is necessary.
The Knighte and Knavee problem is a prime example of this. Ohlbach's interpretation of the prob lem results in him asking "Is there a statement x that I (being a rich knave) can say to convince the princess that I am indeed a rich knave?" Formally this might look like (and does in Ohlbach's second treatment):
OHL: (::Jx)[CanSay(l,x} +-+ T(and(knave(I) ,rich(I)))]"
where T is the predicate meaning True and "and" although a function symbol, intuitively takes two statements as arguments and returns another single conjunctive statement. ···
This may appear to be a reasonable interpreta tion given the English statement of the problem. But as Ohlbach discusses, this representation (along with other associated axioms) is not sufficient to derive the intended result. Indeed, it is not hard to see the prob lem. The constant "I" stands for a fixed person (who is a rich knave). The point of the biconditional in OHL, and espe~ially of the right-hand side, is to test whether the sp~aker is a rich knave, based on the ability to say x. That is, the problem really seems to be asking, "What statement, when made by anrone, will convince the princess that the perton making the atatement is a rich knave." This then is the first prob lem with that representation: "I" should not be bound to a flXed individual, but should represent any "man in the street" who might state x. We then suggest the alternative version:
"Ohlbach's ftrst treatment involved the aoal Sx)ICanSa.y(I,x) -+ T{a.nd{tnave(I),rich{I)))I which (in addition to yielding a trivial and unh.elpful answer) does not seem to correspond to his English interpretation "There exists a statement which I can say a.nd which implies that I am really a rich kna.ve." In fact, it seems to us that
the aoal statement
{3y)iCanSay{l,y) 8& {\fx)ICanSay(x,y)-+ T{a.nd{rich(x),knave(x)))ll cornea much cloeer to the English.
"'Actually, a name or the statement.
Gt 8x)(\fy)!CanSay(y,x) ++ T(and(rieh(y),knave(y)))]
We claim to have now adequately represented the goal statement; but this is still not enough. For although this goal statement expresses what we want, there are other problema arising from the truth condi tions of utterances which enter into other axioms in the problem representation.
ill. UTTERANCEINSTANCES
This brings us to what we think is the key issue in this puzzle, and which has broader significance as well . Specifically, it is that utterances are instances of statement uses, and it is these instances that, in gen eral, have truth-values, rather than the statement in and of itself. In particular, terms in a statement may have no definite reference outside of the context of an utterance. Although this is familiar to linguists· and philosophers (it is the so-called problem of indexieals) it is worth going into detail in the current paper, since the issue of representing knowledge in the Knighta and Knavea problem hinges on this very phenomenon.
Typically, we think of a statement as being either true or false . This, however, is not always the ease. For example, the statement:
"I am a knave"
will have a truth-value dependent upon who the speaker is; and so would be falsely uttered by any knight and truly by any knave. ·· Thus statements that contain indexieals (the word "I" in the above example) have meanings, and hence truth-values, that depend upon context.
Because of the indeterminacy of truth-values of sentences that contain indexieale, we will only refer to the truth-value of utterance-instances of such state ments. An utterance-instance of a statement contains a context in which the statement was (or is) made including who the utterer is.
IV. "WHO AM IT"
0 1ncludin& those wbo wort In n&tural lanauaae proeeeain&; see for instance !Allen 111841, !Allen and Perrault 1111101, !Harper and Charniat 111861.
0 "Hence, this statement can be uttered by neither ltniahte nor ltnans, in the Kniflllo ·nil Kn111t1 problem!
If we look closely at any of Ohlbaeh'e representa tions of the Knighta and Knavea problem, we notice that the constant "I" seems to be playing two different roles. In all of his goal statements "I" is presumably used as a particular person. For example Ohlbaeh's second goal statement, OHL, illustrates this usage. On the other hand, in the intended solution to the problem, the "x" of the goal statement is bound to anriki:···
and( not( rieh(l) ),knave(l))
where, the same symbol "I" appears as before but now what is of interest is its presence inside the "x" in CanSay(l,x); i.e., as part of a potential utterance whose truth value depends upon who the speaker is. That is, any number of people might utter anriki, and its meaning would be different in each ease. We now have an utterance-instance and need to know who "l" is before assigning a truth-value. Thus, "I" must be viewed as a pronoun and not a person here. In partic ular, it .is the knighthood or "knavehood" of "I" which determines the truth of anriki. or course, in the world in question, only knaves (and rich ones at that) could utter anriki. But that is the point; the princess· must be able to deduce precisely that fact: that anyone at all who utters anriki must consequently be a rich knave.
In what follows, we have removed this ambiguity by introducing a new predicate (TU) into the language of Knighta and Knave~. TU is used as a 2-place predi cate expression with its first argument being a person and its second an utterance. Intuitively, TU(p,t) is true if and only if t is true when uttered by person p. More precisely, we say TU(p,t) is true if and only if the substitution-instance of t resulting from replacing all occurrences of "I" in t by "p" is true. Thus the statement:
TU(John,"l am six feet tall")
is true if and only if John (the utterer) is indeed six feet tall.····
V. NOTATION AND AXIOMS
We now introduce our notation for representing the problem. We use a first-order theory which con tains the following:
1: constant (the word "I") knave: function letter (knave(x) stands for the term "x is a knave") rich: function letter
.. 'Throuahout the remainder or thia paper we use "anriti" u a abort-hand for: and(not.(rich(l)),tnan(l)) .
.. "'Thia ia somewhat comparable to the formulation or Bar wiae and Perr1 1111831 when they apeak or an utterance in a "situa. tion" concernin& "1": ull am six feet tallle ia true (where u ia the utterance "I am aix feet tall" and e ia a situation in which John Ia present and matee utterance u) if John ia indeed six feet tall in si tuation e.
knight: function letter
not: function letter
and: 2-place function letter
CanSay: 2-place predicate letter (CanSay(x,y) means
"x can say y")
TU: 2-place predicate expreeeion (TU(p,t) means term t would be true if occurrences of "I" in t are replaced by p)
T: predicate expression (T(t) means the term t is true)
Given the above notation, we can now present the axioms which will capture the Knight· and Knavu problem as we see it. For simplicity, we suppose all variables range over knights, knaves, the princeee, and utterances. ·
We require only three first-order axioms and one functional schema in order to sufficiently represent the needed facts about the world in which the knights, knaves, and princess live, namely,
- (\fp)(\tu){T(knave(p)) ++ (CanSay(p,u) ++ -.TU(p,u)]} I.e., u is a knave iff the things t that u can say are precisely those which would be false if u
- uttered them.
- (\fy)(\tz)[T(and(y,z)) ++ T(y)&T(z)J This captures the meaning of the function Jetter 'and'.
- (3} (\is)[T(s) ++ -.T(not(s))J This axiom captures the meaning of the func tion letter 'not'.
- ( 4} (\fp )[TU(p,/ (I)) ++ T(/ (I))J For example, this intuitively corresponds to TU(Bill,rich(I)) ++ Rich(Bill), where f is "rich".""
If, in line with our earlier discussion, we take G to be our goal statement, then in using the above axioms we have been able . to use resolution to give us the desired solution.""" A version of ~ur resolution proof can be found in the longer paper [Miller and Perlis 1987].
"Thia rollowa the convention or Ohlbach. Tbe uae or either typed or relativized variables would eliminate unusual readings &t the expense or more complex rormult.e.
00 Note that tbia replaces Taraki'a Convention T1 T"a" ... a , in cuea or a having tbe indexical "I".
··· Aa diaculaed axiom 4 Ia really a runctional acbema. Aa such, our axiomatization or Kniflll· and Knovei ia not one that ia computationally prt.ctict.ble without a mechanism ror supplying aub· atitution inat&ncea to the theorem-prover. An alternt.tive represen tation or the problem at band that requires no auch mechanism but nonethelesa rollowa closely our uae or indexicala, ia given in !Miller t.nd Perlia 10871. Namely, this alternative approach introduces a finite axiomatization or "TU". In that pt.per we recursively estab lish o// posaible inatancea or axiom 4 in terms or the lertmoet runc tion symbol occurring in TU's second argument . Thia in conjunc· tion with our resolution proor !Miller and Perlia 10871 gives a com putational solution to tbe Kniflll· and KnatJel problem.
VI. DISCUSSION
Ohlbach has pointed out an interesting problem for knowledge representation. We agree in principle with his conclusion that knowledge representation is hard. In fact, if someone has to invent a new trick each time they wished to represent a problem, the task would become hopeless. Furthermore, if the language used by the AI practitioner forced the need for tricks, then there would certainly be an argument for select ing another language.
·we feel, however, that neither first-order logic nor automatic theorem-proving imposes any such res triction on the Knighta and Knave. problem. The complexity that Ohlbach discovered in trying to represent this problem is due to indexicals. In fact, his second argument to "T" might be dealing with indexical-binding in some way. We have found that a proper treatment of indexical-binding makes for a natural and correct (in that a proper solution is found) representation of Knight· and Knave~.
Furthermore, we feel that this problem is indica tive of a whole class or problems that can be handled in a similar fashion, i.e., not dependent upon isolated or ad hoc tricks. In Knighta and Knave· we defined TU in terms of the indexical "I" only. This is because "I" is the only indexical of importance in this prob lem. In broader contexts, however, this would be insufficient. It will be interesting to see how well gen eralizations of TU handle other indexicals and other problems.
@inproceedings{ijcai1987p98,
title = {Proving Facts about " "},
author = {Miller, Michael J. and Perlis, Donald},
booktitle = {Proceedings of the Tenth International Joint Conference on
Artificial Intelligence, {IJCAI-87}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {John McDermott},
pages = {499--500},
year = {1987},
note = {Knowledge Representation},
url = {https://ijcai.org/proceedings/1987/98},
}
TY - CPAPER TI - Proving Facts about " " AU - Miller, Michael J. AU - Perlis, Donald T2 - Proceedings of the Tenth International Joint Conference on Artificial Intelligence, IJCAI-87 PB - International Joint Conferences on Artificial Intelligence PY - 1987 SP - 499 EP - 500 UR - https://ijcai.org/proceedings/1987/98 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
Welcome
Future Conferences
AI Journal Division
IJCAI Proceedings
About IJCAI
IJCAI Awards