K-STRIPS
Modal Operator K :
We are familiar with the use of connectives ∧ and V in logics. Thinking of these connectives as operators that construct more complex formulas from simpler components. Here, we want to construct a formula whose intended meaning is that a certain agent knows a certain proposition.
The components consist of a term denoting the agent and a formula denoting a proposition that the agent knows. To accomplish this, modal operator K is introduced.
For example, to say that Robot (name of agent) know that block A is on block B, then write,
K( Robot, On(A,B))
The sentence formed by combining K with the term Robot and the formula On(A,B) gets a new formula, the intended meaning of which is “Robot knows that block A is on block B”.
The words “knows” and “belief” is different in meaning. That means an agent can believe a false proposition, but it cannot know anything that is false.
Some examples,
K(Agent1, K(Agent2, On(A,B) ) ], means Agent1 knows that Agent1 knows that A is on B.
K(Agent1, On(A,B)) V K(Agent1, On(A,C) ) means that either Agent1 knows that A is on B or it knows that A is on C.
K(Agent1, On(A,B)) V K(Agent1, ¬On(A,B) ) means that either Agent1 knows whether or not A is on B.
Knowledge Axioms:
The operators ∧ and V have compositional semantics (depends on truth value) , but the semantics of K are not compositional. The truth value of K(Agent1, On(A,B) ) for example, cannot necessarily be determined from the properties of K, the denotation of Agent1 and the truth value of On(A,B). K Operator is said to be referentially opaque.
Example in Planning Speech Action:
We can treat speech acts just like other agent systems. Our agent can use a plan-generating system to make plans comprising speech acts and other actions. To do so, it needs a model of the effects of these actions.
Consider for example, Tell( A, φ ) , where A is Agent and φ is true.
We could model the effects of that action by the STRIPS rule :
Tell( A, φ ) :
Precondition : Next_to(A) ∧ φ ∧ ¬K(A, φ)
Delete : ¬K(A, φ)
Add : K(A, φ)
The precondition Next_to(A) ensures that our agent is close to agent A to enable communication.
The precondition φ is imposed to ensure that our agent actually believes φ before it can inform another agent about the truth.
The precondition ¬K(A, φ) ensure that our agent does not communicate redundant information.
professorguide 