Reasoning About Knowledge and Action
Proceedings of the Fifth International Joint Conference on Artificial Intelligence. Representation of Knowledge. Pages 223-226.
© 1977 International Joint Conferences on Artificial Intelligence
Abstract
This paper discusses the problems of representing and reasoning with Information about knowledge and action. The first section discusses the Importance of having systems that understand the concept of knowledge, and how knowledge Is related to action. Section 2 points out some of the special problems that are Involved In reasoning about knowledge, and section S presents a logic of knowledge based on the Idea of possible worlds. Section i Integrates this with a logic of actions and gives an example of reasoning In the combined system. Section 5 makes some concluding comments.
- Given: True(At(John,Sf)) True(Exists(X I,Know(John,ls•comb-of(X l,Sf)))) Prove: True(Can(John,Open(Sf)))
- I . True (Exists (X I,Know(John,ls•comb•of (X I,Sf))))
- T(WO,Exists(XI,Know(John,ls-comb-of(X l,Sf))))
- T(WO,Know(John,ls-comb-of(C,Sf)))
- K(John,WO,wl) => T(wl,ls-comb-of(C,Sf)) 5. True(At(John,Sf))
- T(WO,At(John,Sf)) 7 . T(WO,Know(John,At(John,Sf)))
- K(John,WO,wl) => T(wl,At(John,Sf))
- K(John,WO,wl) I 0 . T(wl,ls-comb-of(C,Sf)) 11. T(wi,Comb(C)) 12. T(wl ,Safe(Sf))
- T(w2,At(John,Sf))
- Jw2(R(Oo(John,Diai(C,Sf)),w l,w2)
- R(Oo(John,Diai(C,Sf)),wl,w2)
- T(wl,ls-comb-of(C,Sf)) => T(w2,0pen(Sf))
- T(w2,0pen(Sf))
- R(Oo(John,Oiai(C,Sf)),wl,w2) => T(w2,0pen(Sf))
- T(wl ,Res(Oo(John,Diai(C,Sf)),Open(Sf)))
- K(John,WO,wl) => T(wl,Res(Oo(John,Diai(C,Sf)),Open(Sf)))
- T(WO,Know(John,Res(Oo(John,Oiai(C,Sf)),Open(Sf))))
- T(WO,Can(John,Open(Sf))) 23. True(Can(John,Open(Sf)))
- References Hintikka, ]. (1963) Knowledge and Belief. Ithica, New York: Cornell University Press.
- Hintikka, ]. (1969) Semantics for Propositional Attitudes, in Linsky (1971), 115-167.
- Kripke, S. (1963) Semantical Considerations on Modal Logic, in Linsky (1971), 63-72.
- Linsky, L. (ed.) (1971) Reference and Modality. London: Oxford University Press.
- McCarthy, ]. and Hayes, P. ]. (1969) Some Philosophical Problems from the Standpoint of Artificial Intelligence, in B.
- Meltzer and D. Michie (eds.) Machine Intelligence 4, 463-502. Edinburgh: Edinburgh University Press.
- Moore, R. C. (1973) D-SCRIPT: A Computational Theory of Descriptions. Advance Papers of the Third International Joint Conferenct on Artificial Intelligence, 223-229.
- Moore, R. C . (1975) Reasoning from Incomplete Knowledge ln a Procedural Deduction System. MIT Artificial Intelligence Laboratory, AI-TR-347. Knowle~~e RePr.-2: Moore
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.
1. Introduction
One of the most Important concepts an Intelligent system needs to und.erstand Is the concept of knowledge. AI systems need to understand what knowledge they and the systems or people they Interact with have, what knowledge Is needed to achieve particular goals, and how that knowledge can be obtained. This paper develops a formalism that provides a framework for stating and solving problems like these. For example, suppose that there Is a safe that John wants to open. The common sense Inferences that we would like to make might Include:
If John knows the combination, he can immediately open the safe.
If John does not know the combination, he cannot Immediately open the safe.
If John knows where the combination Is written, he can read the combination and then open the safe.
In thinking about this example, consider how Intimately the concept of knowledge Is tied up with action. Reasoning about knowledge alone Is of limited value. We may want to conclude from the fact that John knows A and B that he must also know C and D, but the real importance of such information Is usually that It tells us something about what John can do or is likely to do. A major goal of my research has been to work out some of the Interactions of knowing and doing.
That this area has received little attention In AI Is somewhat surprising. It Is frequently stated that good Interactive AI programs will require good models of the people they are communicating with. Surely, one of the most Important aspects of a model of another person Is a model of what he knows. The only serious work on these problems in AI which I am aware of Is a brief dlsscusslon In McCarthy and H·wes (1969), and some more recent unpublished writings of McCarthy. In philosophy there Is a substantial literature on the logic of knowledge and belief. A good Introduction to this is Hintikka (1962) and papers by Q..ulne, Kaplan, and Hlntlkka In Linsky (1971). Many of the ideas I will use come from these papers.
In representing facts about knowledge and actions, I will use first-order predicate calculus, a practice which is currently unfashionable. It seems to be widely believed that use of
REASONING ABOUT KNOWLEDGE AND ACTION
Robert C. Moore Artificial Intelligence Laboratory Stanford University Stanford, California 94305
predicate calculus necessarily leads to Inefficient reasoning and Information retrieval programs. I believe that this Is an over reaction to earlier attempts to build domain-independent theorem provers based on resolution. More recent research, Including my own M.S. thesis (Moore, 1975), suggests that predicate calculus can be treated In a more natural manner than resolution and combined with domain-dependent control Information for greater efficiency. Furthermore, the problems of reasoning about knowledge seem to require the full ability to handle quantifiers and logical connectives which only predicate calculus posseses.
Section 2 of this paper attempts to bring out some of the special problems Involved In reasoning about knowledge. Section 3 presents a formalism which I believe solves these problems, and Section i Integrates this with a formalism for actions. Section 5 makes some concluding comments.
2. Problems in Reasonin~ about Knowledn
Reasoning about knowled~e presents special difficulties. It turns out that we cannot treat know" as just another relation. If we can represent "Biockl Is on Block2" by On(Biocki,Biock2), we might be tempted to represent "John knows that P" simply by Know(John,P). This approach glosses over a number of problems. We might be suspicious from the first, since P is not the name of an object but Is rather a sentence (or proposition). The semantics of predicate calculus forbid the arbitrary intermingling of sentences and terms for good reason. For one thing, the second argument position of Know is a referentially opaque context. Ordinarily In logic we can freely substitute an expression for one that Is extensionally equivalent (I.e., one that has the same referent or truth value), without affecting the truth of the formula that contains the expression. This is called referential transparenCJ. For example, If X · Y · 7 and X · 3, then 3 · Y · 7. This pattern of reasoning Is not valid with Know. We cannot Infer from Know(John,(X · Y · 7)) and X · 3 that Know(John,(3 · Y · 7)) is true, since John might not know the value of X.
One possible solution to this problem is to make the second argument of Know the name of a formula rather than the formula Itself. This is essentially the same idea as Goede! numbering, although It Is not necessary to use such an obscure encoding as the natural numbers. We won't specify exactly how the encoding is done, but simply use "P" to represent a term denoting the formula P. The representation of "John knows that P" now becomes Know(John,"P"). We are no longet in any danger of infering Know(John,"P(A)") from Know(John,"P(B)") and A · B, because A Is not contained In "P(A)". Only the name of A, i.e. "A", Is contained, and since "A" does not equal "B", there Is no problem.
There Is, however, a more serious problem, the fact that people can reason with their knowledge. We would expect a reasoning system to have built into it the ability to conclude B from A and A ::o B. But If we treat Know as just an ordinary predicate, we will have no reason to suppose that Know(John,"A") and Know(John,"A ::o B") might suggest Know(John,"B"). This problem Is emphasised by the fact that there Is no formal connection between a formula and Its name. The fact that we regard "P" as the name of P is entirely outside the system. To get around this, It Is necessary to re-axiomatize the rules of logic within the system, e.g. Ve,p,q(Know(a,"p ::) q") " Know(a,"p") ::) Know(a,"q")). But if we hope to do automated reasoning, this amounts to re-programming the deductive system in first-order logic, and using the top-level inference routines as the interpreter. When we consider the complexities of quantification and matching, it seems likely that this would be an inefficient process.
A different idea which initially seems very appealing is to use the multiple data-base capabilities of advanced AI languages to set up a separate data base for each person whose knowledge we have some information about. We then can record what we know about his knowledge in that data base, and simulate his reasoning by running our standard Inference routines In that data base. This idea seems to have wide currency in AI circles, and I advocated It myself in an earlier paper (Moore, 1973).
Unfortunately, It doesn't work very well. It can handle simple statements of the form "John knows that P," but more complicated expressions cause trouble. Consider "John knows that P or John kn.ows that Q · We can't represent this by simply adding ·p or Q to the data base representing John's knowledge, because this would mean "John knows that P or ()y" - something quite different. We could try setting up two data bases, DB I and DB2, add "P" to one and "Q" to the other, and then assert in the main data base "DB I represents John's knowledge, or DB2 represents John's knowledge." However, if we also wanted to assert "John knows that C, or John knows that D, or John knows that E," we would need six data bases to represent all the possibilites for . 'John's knowledfe ·one for each of the combinations "A" and "C", B" and "C", A" and "D", etc. As we add more disjunctive assertions, we get a combinatorial explosion in the number of data bases.
We also hav.e a problem in representing "John doesn't know that P." We can't add "not P" to John's data base, because this would be asserting "John knows that not P," and simply omitting "P" from John's data base means that we don't know whether John knows that P. So it seems that what John doesn't know has to be kept separate from what he does know. But there are Inferences that require looking at both. For example, If we have "John doesn't know that P," and "John knows that Q.. implies P," we might want to conclude that "John doesn't know that ()y" Is probably true. This Is representative of a class of inferences that the data base approach doesn't capture. There seems to be a fundamental problem in saying things about a person's knowledge that go beyond simply enumerating what he knows.
ll. Reasonln~ about Knowled~e via Possible Worlds
While there may be ways to directly attack the difficulties we have been discussing, there is a way to avoid them entirely by reformulating the problem in terms of possible worlds. When we want to reason about someone's knowledge, rather than talking about what facts he knows, we will talk about which of the various possible worlds might be, so far as he knows, the real world. A person is never completely sure which possible world (or possible state of tltt world) he is in, because his knowledge is Incomplete. We will be willing to conclude that a person knows a particular fact, If the fact is true in all the worlds that are possible according to what he knows. This idea is due to Hintikka (1969), and Is an adaptation of the semantics for modal logic developed chiefly by Kripke (1963).
Hintikka uses these ideas about possible worlds to provide a model theory for a modal logic of knowledge. In order to use this theory directly for reasoning, we will axiomatize it in first-order logic. To do this, we must encode a language that talks about knowing facts (which we will call the object language) into term expressions of a first-order language that talks about possible worlds (which we will call the meta-language). Then we will have a relation T, such that T(W,P) means the object-language formula denoted by P is true in the possible world denoted by W. So that we can talk more easily about truth in the actual world, we will have a predicate True, such that True(P) 1 T(WO,P), where WO Is a constant which refers to the actual world. We will also have a relation K(A,WI,W2), which means that W2 is a world which is possible according to what A knows in WI. The fundamental axiom of knowledge Is then Vwl,a,p(T(wl,Know(a,p) 1 Vw2(K(a,wl,w2) ::) T(w2,p)). This simply says that a person. knows the facts that are true In every world that is possible according to what he knows.
One problem with this axiom is that it is not universally true. For a person to know everything that is true in all worlds which are possible as far as he knows, he would have to know all the logical consequences of his knowledge." Of course, he can know only some of them. But In any particular case, if we can see that a certain conclusion follows from someone's knowledge, we are probably justified in assuming that he can see this also. So we can regard this axiom as a rule of plausible inference, using it when needed, but being prepared to retract our conclusions if they generate contradictions. I will not attempt here to devlop a general theory of plausible reasoning, but I believe that a theory can be worked out that will allow us to use this axiom in essentially its current form.
I should clarify what type of possible worlds I have in mind. Rather than all logically possible worlds, we will consider only those worlds which are possible according to "common knowledge". So, I will feel free to say that facts like "Fish live In water," are true In all possible worlds. This gives us an easy way of saying that not only does everyone know something, but everyone knows that everyone knows It, and everyone knows that everyone knows that everyone knows, etc.
We can now give the full axiomatlzation of knowledge in terms of possible worlds:
Ll . True(pl) 1 T(WO,pl)
L2. T(wl,(pl And p2)) 1 (T(wl,pl) 1\ T(wl,p2))
L3. T(wl,(pl Or p2)) 1 (T(wl,pl) v T(wl,p2))
L4. T(wl,(pl ·> p2)) 1 (T(wl,pl)::) T(wl,p2))
LS. T(wl,(pl <·> p2)) 1 (T(wl,pl) 1 T(wl,p2))
L6. T(wi,Nol(pl)) 1 ~T(wl,pl)
Kl. T(wi,Know(al,pl)) · Vw2(K(al,wl,w2)::) T(w2,pl))
K2. K(al,wl,wl)
K3. K(al,wl,w2)::) (K(al,w2,w3)::) K(al,wl,w3))
K4. K(al,wl,w2)::) (K(al,wl,w3)::) K(el,w2,w3))
Axioms L I - L6 just translate the logical connectives from the object language to the meta-language, using the ordinary Tarskl definition of truth. For instance, according to L2, (A And B) is true In a world if and only if A is true in the world and B is true in the world. K I is the fundamental axiom of knowledge which we already looked at. K2 says that each world is possible as far as anyone in that world can tell, which is another way of saying that If something Is known then It is true. Although it may not be obvious, K3 and K-. imply that everyone knows whether he knows a certain fact. K2- K-. imply that for fixed A, K(A,wl,w2) Is an equivalence relation. This makes our logic of knowledge Isomorphic to the modal logic 55. The correspondence between various modal logics and and possible-worlds models for them Is discussed in Kripke( 1963).
This representation gives us what we need. The metalanguage translations of the object-language statements have a structure that reflects their logical properties. To illustrate the use of these axioms, we can prove that people can do simple Inferences:
Given: True(Know(A,P) And Know(A,(P ·> Q)))
Prove: True(Know(A,Q))
| I. True(Know(A,P) And Know(A,(P •> Q))) 2. T(WO,(Know(A,P) And Know(A,(P •> Q)))) 3. T(WO,Know(A,P)) 11 T(WO,Know(A,(P •> Q))) 4. T(WO,Know(A,P)) 5. K(A,WO,wl);:, T(wi,P) 6. T(WO,Know(A,(P •> Q))) 7. K(A,WO,wl) ;:, T(wl ,(P •> Q)) 8. K(A,WO,wl) 9. T(wi,P) 10. T(wi,(P•>Q)) II. T(wi,P);:, T(wi,Q) 12. T(wi,Q) 13. K(A,WO,wl);:, T(wi,Q) 14. T(WO,Know(A,Q)) 15. True(Know(A,Q)) | Given Ll,l L2,2 3 K1,4 3 Kl,6 Ase 5,8 7,8 L4,10 11,9 Ois(8,12) 1<1,13 Ll,l4 |
Proofs In this paper use natural deduction. The right hand column gives the axioms and preceding lines which justify each step. Indented sections are subordinate proofs, and Ass marks the assumptions on which these subordinate proofs are based. Oia Indicates the discharge of an assumption.
This proof Is completely straight-forward. Lines I - 7 simply expand the given facts Into possible-worlds notation. Then we pick wl . as a typical world which is possible according to what A knows. In lines 9 - 12, we do the Inference that we want to attribute to A. Since this inference can be done in an abitrarily chosen member of the set of worlds which are possible for A, it must be valid in all of them (line 13). From this we conclude that A can probably do the Inference also (lines 14- 15).
So far I have avoided dealing with the problem of quantifiers. · Exactly what do expressions like 3x(Know(A,P(x))). mean? This Is not a simple assertion that someone knows a certain fact, so its intuitive meaning may not be clear. The best paraphrase seems to be "There Is something that . A knows has property P." It Is a matter of great dispute in philosophy exactly how to handle this. I will take a pragmatic approach. To say that a person knows of something that it has property P means that he can name something that has property P. Furthermore, just any sort of name won't do. "The thing that has property P" Is no good, for Instance. We will say that A must know the standard name of the thing that has P. This is, of course, a simplification. Not all things have standard names, and some things have different standard names in different contexts, but we will Ignore these difficulties to preserve the simplicity of the ordinary case. Abstract entitles usually have unproblematical standard names - "23" Is th.e standard name of 23, "15 + 8" is not.
Turning to the model theory, the interpretation of the formula we are considering would be that there is something that is P In all worlds compatible with what A knows. That means that standard names must refer to the same thing in all possible worlds. There is a term for this in philosophy, rigid designator. We can greatly simplify our formalism if we require that all ordinary terms In the object language be rigid designators. We would then have to have a special notation for non-rigid designators, but this will not come up in our examples, so I will not develop that Idea here. We can now give the axioms for quantifiers and equality:
- L7. T(w I ,Exist(vl ,P)) · 3x(T(w I ,P[x/v I])) provided x Is not free in P
- L8. T(wi,AII(vi,P)) · Vx(T(wi,P[x/vl])) provided x is not free in P
- L9. T(wl ,Eq(xl ,x2)) · (xi · x2)
L 7 and L8 are axiom schemas relative to P and x, and vi is a meta-language variable that ranges over object-language variables. P[x/vl] means the result of substituting x for vi in P.
These three axioms may seem somewhat peculiar In that they appear to say that individuals In the world can be part of object language expressions. In L 7 and LS, we took x, a variable ranging over real objects, and inserted it into P, the name of a sentence, Implying that objects can be contained in sentences. To preserve the simplicity of the notation, without this apparent absurdity, we will make the interpretation that all functions which represent atomic predicates In the object language (e.g. Eq) take Individuals as arguments and return expressions containing the standard names of those individuals.
4. Inte~ratin~ Knowled~e and Action
In order to Integrate knowledge with actions, we need to formalize a logic of actions in terms comparable to our logic of knowledge. Happily, the standard AI way of looking at actions does just that. Most AI programs that reason about actions view the world as a set of possible situations, and each action determines a binary relation on situations, one situation being the outcome of performing the action in the other situation. We will Integrate knowledge and action by identifying the possible worlds In our logic of knowledge with the possible situations in our logic of actions.
First, we need to define our formalism for actions exactly parallel to our formalism for knowledge. We will have an object language relation Res(E,P) which says that it is possible for event E to occur, and P would be true in the resulting situation. In the meta-language, we will have the corresponding relation R(E,WI ,W2) which says that W2 is a possible situation/world which could result from event E happening in WI. These two concepts are related In the following way:
(3w2(R(el,wl,w2)) 11 Vw2(R(el,wl,w2);:, T(w2,pl)))
The existential clause on the right side of R I says that It is possible for the event to occur,. and the universal clause says that In every possible outcome the condition of interest is true. There Is a direct parallel here with concepts of program correctness, the first clause expressing termination, and the second, partial correctness.
We can extend the parallel with programming-language semantics to the structure of actions. We will have a type of event which is an actor performing an action, Oo(A,C). (C stands for "command".) Actions can be built up from simpler actions using loops, conditionals, and sequences:
R2. T(wl ,Res(Do(al ,Loop(pl ,cl )),p2) · T(wl ,Res(Do(al ,lf(pl ,(el ;Loop(pl ,el )),Nil)),p2))
- R3. T(wl,Res(Oo(al,lf(pl,el,e2)),p2) · ((T(wi,Know(al,pl)) 11 T(wl,Res(Oo(al,el),p2))) v (T(wl ,Know(el ,Not(pl))) 11 T(wl ,Res(Oo(al ,e2),p2))))
R4. T(wl,Res(Oo,al,(el;c2)),pl)) 1 T(w I ,Res(Do(al ,cl ),Res(Oo(al ,c2),pl )))
Nl. R(Oo(al,Nil),wl,w2) 1 (wl · w2)
R2 defines the step-by step expansion of while-loops: if the test Is true, execute the body and repeat the loop, else do nothing. To prove general results we would need some sort of Induction axiom. R3 defines the execution of a conditional action. Notice that being able to execute a conditional requires knowing whether the test condition Is true. This differs from ordinary program conditionals, where the test condition is either assumed to be a decidable primitive, or Is itself a piece of code to be executed. R4 says that the result of carrying out a sequence of actions Is the result of executing the first action, and then executing the rest. N I simply defines the no-op action we need for the definition of Loop.
One of the most Important problems we want to look at Is how knowledge affects the ability to achieve a goal. Part of the answer Is given In the definition of the notion Can. We will say that a person can bring about a condition if and only if there Is an action which he knows will achieve the condition:
Cl. T(wi,Can(al,pl)) 1 Jel(T(wl,Know(al,Res(Oo(al,el),p))))
The idea is that to achieve something, a person must know of a plan for achieving It, and then be able to carry out the plan.
We have seen a couple of ways that knowledge affects the possibility of action in R3 and C I. We now want to describe how actions affect knowledge. For actions that are not information acquiring, we can simply say that the actor knows that he has performed the action. Since our axiomatization of particular actions implies that everyone knows what their effects are, this Is sufficient. For Information-acquiring actions, like looking at something, we will also add that the Information has been acquired. This is best explained by a concrete example. Below, we will work out an example about opening safes, so we will now look at the facts about dialing combinations:
01. Jw2(R(Oo(ai,Oial(xl,x2)),wl,w2) 1 (T(wl,Comb(xl))" T(wi,Safe(x2)) "T(wi,AI(al,x2))) 02. R(Oo(al,Oial(xl,x2)),wl,w2) => ((T(wl ,ls-comb-of(xl ,x2)) => T(w2,0pen(x2)))" ((-T(wl,ls-comb-of(xl,x2))" -T(wl,Open(x2)) => -T(w2,0pen(x2)))" (T(wl ,Open(x2)) => T(w2,0pen(x2))) 03. R(Oo(ai,Dial(xl,x2)),wl,w2) => (K(al ,w2,w3) 1 ((T(w2,0pen(x2)) · T(w3,0pen(x2))) 1\ Jw4(K(al ,wl,w4)" R(Oo(al ,Oial(xl ,x2)),w4,w3)))
0 I says that an actor can perform a dialing action If the thing he is dialing Is a combination, the thing he is dialing it on Is a safe, and he is at the same place as the safe. 02 tells how dialing a combination affects whether the safe is open: if the combination is the combination of the safe, then the safe will be open; If it Is not the combination of the safe and the safe was locked, the safe stays locked; If the safe was already open, it stays open.
03 describes how dialing affects the knowledge of the dialer. Roughly it says that the actor knows he has done the dialing, and he now knows whether the safe is open. More precisely, It says that the worlds that are now possible as far as he knows are exactly those which are the result of doing the action In some previously possible world and in which the information acquired matches the actual world. Notice that by making the consequent of 03 a bi-conditional, we have said that the actor has not that 03 is more subtle than just saying that whatever he knew before he knows now. This Is not strictly true. He might have known before that the safe was locked, and now know that the safe Is open. According to 03, if the actor knew before the action "P is true", after the action he knows "P was true before I did this action."
Having presented the basic formalism, I would now like to work out a simple example to illustrate its use. Simply stated, what I will show Is that If a person knows the combination of a safe, and he Is where the safe is, he can open the safe. Besides the axioms for Dial, we will need two more domain-specific axioms:
AI. T(wl ,ls·comb-of(xl,x2)) => (T(wi,Comb(xl))" T(wl,Safe(x2)))
A2. T(wi,At(al,xl)) => T(wi,Know(al,At(al,xl))
A I says that If one thing is the combination of another, the first thing Is a combination and the second thing is a safe. A2 says that a person knows what is around him. The proof is as follows:
Given: True(At(John,Sf)) True(Exists(X I,Know(John,ls·comb-of(X l,Sf))))
Prove: True(Can(John,Open(Sf)))
| I . True (Exists (X I,Know(John,ls·comb·of (X I,Sf)))) | Given |
|---|---|
| 2. T(WO,Exists(XI,Know(John,ls-comb-of(X l,Sf)))) | Ll,l |
| 3. T(WO,Know(John,ls-comb-of(C,Sf))) | L7,2 |
| 4. K(John,WO,wl) => T(wl,ls-comb-of(C,Sf)) | K1,3 |
| 5. True(At(John,Sf)) | Given |
| 6. T(WO,At(John,Sf)) | L1,5 |
| 7. T(WO,Know(John,At(John,Sf))) | A2,6 |
| 8 . K(John,WO,wl) => T(wl,At(John,Sf)) | K1,7 |
| 9. K(John,WO,wl) | Ass |
| I 0 . T(wl,ls-comb-of(C,Sf)) | 4,9 |
| 11. T(wi,Comb(C)) | Al,IO |
| 12. T(wl ,Safe(Sf)) | Al,IO |
| T(w2,At(John,Sf)) | 8,9 |
| 13. 14. Jw2(R(Oo(John,Diai(C,Sf)),w l,w2) | 01,11,12,13 |
| 15. R(Oo(John,Diai(C,Sf)),wl,w2) | Ass |
| 16. T(wl,ls-comb-of(C,Sf)) => T(w2,0pen(Sf)) | 02,15 |
| T(w2,0pen(Sf)) | 16,10 |
| 17. 18. R(Oo(John,Oiai(C,Sf)),wl,w2) => T(w2,0pen(Sf)) | Ois(15,17) |
| 19. T(wl ,Res(Oo(John,Diai(C,Sf)),Open(Sf))) | Rl,l4,18 |
| 20. K(John,WO,wl) => T(wl,Res(Oo(John,Diai(C,Sf)),Open(Sf))) | Dis(9,19) |
| 21 . T(WO,Know(John,Res(Oo(John,Oiai(C,Sf)),Open(Sf)))) | Kl,20 |
| 22. T(WO,Can(John,Open(Sf))) | Cl,21 |
| 23. True(Can(John,Open(Sf))) | Ll,22 |
The proof is actually simpler than it may look. The real work is done in the ten steps between 10 and 19; the other steps are the overhead involved In translating between the object language and the meta language. Notice that we did not have to say explictly that someone needs to know the combination in order to open a safe. Instead we said something more general, that it is necessary to know a procedure In order to do anything. In this case, the combination is part of that procedure. It may also be Interesting to point out what would have happened if we had said only that John knew the safe had a combination, but not that he knew what It was. If we had done that, the existential quantifier In the second assertion would have been inside the scope of Know. Then the Skolem constant C would have depended on the variable wl, and the step from 20 to 21 would have failed.
5. Conclusions
In summary, the possible-worlds approach seems to have two acquired any other Information by doing the action. Also notice major advantages as a tool for reasoning about knowledge. First, it allows "lifting" reasoning in knowledge contexts Into the basic deductive system, eliminating the need for separate axioms or rules of inference for these contexts. Second, it permits a very elegant Integration of the logic of knowledge with the logic of actions.
This approach seems to work very well as far as we have taken it, but there are some major issues we have not discussed. I have said nothing so far about procedures for reasoning automatically about knowledge. I have some results in this area which appear very promising, but they are too fragmentary for Inclusion here. I have also avoided bringing up the frame problem, by not looking at any sequences of action. I am also working in this area, and I ~onsider it one of the largest lOU's generated by this paper. However, the possible-worlds approach has an important advantage here. Whatever method is used to handle the frame problem, whether procedural or axiomatic, knowledge contexts will be handled automatically, simply by applying the method uniformly to all possible worlds. This should eliminate any difficulties of representing what someone knows about the frame problem.
6. References
- Hintikka, ]. (1963) Knowledge and Belief. Ithica, New York: Cornell University Press.
- Hintikka, ]. (1969) Semantics for Propositional Attitudes, in Linsky (1971), 115-167.
- Kripke, S. (1963) Semantical Considerations on Modal Logic, in Linsky (1971), 63-72.
- Linsky, L. (ed.) (1971) Reference and Modality. London: Oxford University Press.
- McCarthy, ]. and Hayes, P. ]. (1969) Some Philosophical Problems from the Standpoint of Artificial Intelligence, in B. Meltzer and D. Michie (eds.) Machine Intelligence 4, 463-502. Edinburgh: Edinburgh University Press.
- Moore, R. C. (1973) D-SCRIPT: A Computational Theory of Descriptions. Advance Papers of the Third International Joint Conferenct on Artificial Intelligence, 223-229.
- Moore, R. C. (1975) Reasoning from Incomplete Knowledge ln a Procedural Deduction System. MIT Artificial Intelligence Laboratory, AI-TR-347.
@inproceedings{ijcai1977p49,
title = {Reasoning About Knowledge and Action},
author = {Moore, Robert C.},
booktitle = {Proceedings of the Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-77}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Raj Reddy},
pages = {223--226},
year = {1977},
note = {Representation of Knowledge},
url = {https://ijcai.org/proceedings/1977/49},
}
TY - CPAPER TI - Reasoning About Knowledge and Action AU - Moore, Robert C. T2 - Proceedings of the Fifth International Joint Conference on Artificial Intelligence, IJCAI-77 PB - International Joint Conferences on Artificial Intelligence PY - 1977 SP - 223 EP - 226 UR - https://ijcai.org/proceedings/1977/49 ER -Copied
Machine-readable versions of this paper, for tools and AI agents: