This paper proposes an integration of the situation calculus with justification logic. Justification logic can be seen as a refinement of a modal logic of knowledge and belief to one in which knowledge (and belief) not only is something that holds in all possible worlds, but also is justified. The work is an extension of that of Scherl and Levesque's integration of the situation calculus with a modal logic of knowledge. We show that the solution developed here retains all of the desirable properties of the earlier solution while incorporating the enhanced expressibility of having justifications. Additionally, the approach incorporates a notion of thinking. This addresses the logical omniscience problem as the knowledge of the agent depends on the number of inference steps it has performed.
the first two elements of the tripartite analysis; p is known The situation calculus is at the core of one major approach if it is believed (i.e., true in all accessible worlds) and if it to cognitive robotics as it enables the representation and is true in the actual world. The component of justification reasoning about the relationship between knowledge, per- has recently been added with the development of justiception, and action of an agent [1, 2]. Axioms are used to ifcation logic [ 17, 18, 19, 20, 21]. In justification logic, specify the prerequisites of actions as well as their effects, there is in addition to formulas, a category of terms called that is, the fluents that they change [ 3]. By using succes- justifications . If t is a justification term and X is a formula, sor state axioms [4], one can avoid the need to provide then t:X is a formula which is read as “t is a justification frame axioms [5] to specify what particular actions do not for X.” If the formula X is also true and believed to be true, change. This approach to dealing with the frame problem one can then write []: for X is known with justification and the resulting style of axiomatization has proven useful t. as the foundation for the high-level robot programming One of the examples used in the philosophical literature language GoLog [6, 7]. mentioned above is the Red Barn Example [11, 19, 22,
Knowledge and knowledge-producing actions have 14, 16]. Henry is driving through the countryside and been incorporated into the situation calculus [8, 9] by perceptually identifies an object as a barn. Normally, treating knowledge as a fluent that can be affected by one would then say that Henry knows that it is a barn. actions. Situations from the situation calculus are iden- But Henry does not know there are expertly made papiertified with possible worlds from the semantics of modal mâché barns. Then we would not want to say that Henry logics of knowledge. It has been shown that knowledge- knows it is a barn unless he has some evidence against it producing actions can be handled in a way that avoids being a papier-mâché barn. But what if in the area where the frame problem: knowledge-producing actions do not Henry is traveling, there are no papier-mâché red barns. affect fluents other than the knowledge fluent, and that Then if Henry perceives a red barn, he can then be said to actions that are not knowledge-producing only affect the know there is a red barn and therefore a barn. knowledge fluent as appropriate. The apparent problem here is only a problem within
Within epistemology, the traditional analysis of knowl- a modal logic of knowledge. There are two ways of the
edge (dating back to Plato) is tripartite [
CPWrEooUrckReshdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g ACttEribUutiRon 4W.0Iontrekrnsathioonapl(CPCrBoYc4e.0e)d.ings (CEUR-WS.org)
Within justification logic [ 17, 19, 20] there is no contra- An action precondition axiom for the action drop is given diction because the justifications differ. The modality of below. knowledge is an existential assertion that there is a justification of a proposition. In one case, there is a justification POSS(DROP(), ) ≡ HOLDING(, ) (2) for the object being a barn via a barn perception and in the other case a justification for it being a barn via the Furthermore, the axiomatizer has provided for each red barn perception and propositional reasoning. Later in lfuent , two general effect axioms of the form given in 3 this paper, the example will be worked out in the situation and 4. calculus with justified knowledge. General Positive Effect Axiom for Fluent F
Goldman [15] has argued that the tripartite analysis of knowledge needs to be augmented with the requirement F+(, ) → F(DO(, )) (3) that there is a causal chain from the truth of the proposition General Negative Effect Axiom for Fluent F known to the knowledge of the proposition. Only in the case of knowledge via the red barn perception is this F− (, ) → ¬F(DO(, )) (4) condition met. The justification of knowing that the object is a barn via the red barn perception can be seen as meeting Here F+(, ) is a formula describing under what conthis further condition, while the justification via the barn ditions doing the action in situation leads the fluent perception does not meet this condition [17, 19]. F to become true in the successor situation DO(, ) and
The author is not aware of any previous work on in- similarly F− (, ) is a formula describing the conditions tegrating the situation calculus with a notion of justified under which performing action in situation results in knowledge other than an earlier version of this work [23] the fluent F becoming false in situation DO(, ). which did not include thinking about justifications. There For example, ( 5) is a positive effect axiom for the fluent has been some work on integrating justifications into dy- BROKEN. namic epistemic logic [24, 25, 26].
[( = DROP() ∧ FRAGILE())
∨ (∃ = EXPLODE() ∧ NEXTO(, , ))] → BROKEN(, DO(, )) (5)
The situation calculus (following the presentation in [4]) is a first-order language for representing dynamically chang- = REPAIR() → ¬BROKEN(, DO(, )) (6) ing worlds in which all of the changes are the result of named actions performed by some agent. Terms are used It is also necessary to add frame axioms that specify to represent states of the world, i.e., situations. If is when fluents remain unchanged. The frame problem arises an action and a situation, the result of performing because the number of these frame axioms in the general in is represented by DO(, ). The constant S0 is used case is 2 × × ℱ , where is the number of actions to denote the initial situation. Relations whose truth val- and ℱ is the number of fluents. ues vary from situation to situation, called fluents , are The approach to handling the frame problem [4, 27, 28] denoted by a predicate symbol taking a situation term as rests on a completeness assumption. This assumption is the last argument. For example, BROKEN (, ) means that axioms (3) and (4) characterize all the conditions that object is broken in situation . Functions whose under which action can lead to a fluent F’s becoming denotations vary from situation to situation are called true (respectively, false) in the successor situation. Therefunctional fluents . They are denoted by a function sym- fore, if action is possible and F’s truth value changes bol with an extra argument taking a situation term, as in from false to true as a result of doing , then F+(, ) PHONE-NUMBER(BILL,). must be true and similarly for a change from true to false
It is assumed that the axiomatizer has provided for each ( F− (, ) must be true). Additionally, unique name axaction (⃗), an action precondition axiom of the form1 ioms are added for actions and situations. given in ( 1), where (⃗, ) is the formula for (⃗)’s Reiter[4] shows how to derive a set of successor state action preconditions. axioms of the form given in 7 from the axioms (positive Action Precondition Axiom effect, negative effect and unique name) and the completeness assumption.
POSS( (⃗), ) ≡ (⃗, ) (1) Successor State Axiom 1By convention, variables are indicated by lower-case letters in italic font. When quantifiers are not indicated, the variables are implicitly universally quantified.
F(DO(, )) ≡ F+(, ) ∨ (F() ∧ ¬ F− (, ))
(7) Now note for example that if ¬BROKEN(OBJ1, S0) holds, then it also follows (given the unique name axioms) that ¬BROKEN(OBJ1, DO(DROP(OBJ2), S0)) holds as well.
tional logic (or quantifier free first-order logic) justification terms that are built with justification variables , , , . . . and justification constants , , , . . . (using indices = 1, 2, 3, . . . whenever needed) using the operations ‘· ’ and ‘+.’
The logic of justifications includes (in addition to the classical propositional axioms and the rule of Modus Ponens), the following axioms Application Axiom : ( → ) → ( : → [ · ] : ), Sum Axioms : → [ + ] : , : → [ + ] :
Factivity : → Positive Introspection : →! : ( : ) Negative Introspection ¬ : →? : (¬ : ) Similar successor state axioms may be written for func- specifying which propositions are true in which worlds. tional fluents. A successor state axiom is needed for each In the work here, we assume that a particular element of lfuent F, and an action precondition axiom is needed for is specified as the actual world. each action . The unique name axioms need not be There is the evidence function ℰ that maps justification explicitly represented as their effects can be compiled. terms and formulas to sets of worlds. The idea is that if Therefore only ℱ + axioms are needed. a possible world Γ ∈ ℰ (, ) then is relevant evidence
From (5) and (6), the following successor state axiom for at world Γ . for BROKEN is obtained. Given a Fitting model ℳ = ⟨, ℛ, ℰ , ⟩, the truth of a formula at a possible world Γ , i.e., ℳ, Γ |= is given as follows: 1. ℳ, Γ |= if Γ ∈ ( ) for a propositional
letter; 2. It is not the case that ℳ, Γ |=⊥; 3. ℳ, Γ |= → iff it is not the case that
ℳ, Γ |= or ℳ, Γ |= ; 4. ℳ, Γ |= (:) iff Γ ∈ ℰ (, ) and for every
∆ ∈ , with Γ ℛ∆ , ℳ, ∆ |= .
something to be known, it both needs to be believed in the sense that it is true in every accessible world and that is relevant evidence for at that world. So, : holds iff is believable and is relevant evidence for .
The following conditions need to be placed on the Evidence function: • ℰ (, → ) ∩ ℰ (, ) ⊆ ℰ ( · , ) • ℰ (, ) ∪ ℰ (, ) ⊆ ℰ ( + , )
Additionally, the issue of a constant specification needs to be mentioned. All axioms of propositional logic that are used need to have justifications. Degrees of logical awareness can be distinguished through the constant specification. The constant specification (CS) is a set of justified formulas (axioms of propositional logic). A model ℳ meets the constant specification as long as the following condition is met: if : ∈ then ℰ (, ) =
BROKEN(, DO(, )) ≡ ( = DROP() ∧ FRAGILE())∨ (∃ = EXPLODE() ∧ NEXTO(, , )) ∨ (BROKEN(, ) ∧ ̸= REPAIR()) (8)
Factivity is used in all logics of knowledge. The Positive worlds.
Introspection operator ‘!’ is a proof checker, that given Within justification logic, the derivation of a justified produces a justification ! of : . The negative introspec- formula such as : is the derivation of being known. tion operator ‘?’ verifies that a justification assertion is The justifications distinguish different ways of knowing. false [17, 19, 29]. Additionally, they represent how difficult it is to know
The standard semantics for justification logics [ 30] are something and therefore a mechanism for addressing the called Fitting models or possible world justification mod- logical omniscience problem [32]. The size of a justifiels. This is a combination of the usual Kripke/Hintikka cation term corresponds to the amount of effort needed possible world models with the necessary features to han- to derive the term. Only with unlimited computational dle justifications [ 31]. A model for justification logic is effort (“thinking”) are our agents logically omniscient. a structure ℳ = ⟨, ℛ, ℰ , ⟩. Here, ⟨, ℛ⟩ is a stan- The omniscience also depends on a complete constant dard frame for modal logic with being a set of possible specification. If the agent has a limited knowledge of worlds and ℛ being a relation on the elements of . The propositional axioms then it’s reasoning powers are also element is a mapping from ground propositions to limited.
For clarity, a number of sorts4 are gradually introduced.
The sort SIT is used to distinguish between situations and other objects. It is assumed that we have axioms asserting that the initial situation S0 is of type SIT and that everything of the form DO(, ) is of type SIT. The letter , possibly with subscripts, is used to as indication that the variable is of type SIT, without explicit use of the sort predicate.
The approach we take to formalizing knowledge2 is to adapt the semantics of justification logic described in the previous section to the situation calculus. Following [33, 9], we think of there being a binary accessibility relation over situations, where a situation ′ is understood as being accessible from a situation if as far as the agent 5. Integrating Justified knows in situation , he might be in situation ′. Knowledge and Action
To handle the accessibility relation between situations (possible worlds), we introduce a binary relation K(′, ), The approach being developed here rests on the specifica(representing ℛ) read as “′ is accessible from s” and tion of a successor state axiom for the K relation and the treat it the same way we would any other fluent. In other E relation This successor state axiom for the K relation words, from the point of view of the situation calculus, will ensure that for all situations DO(, ), the K relation the last argument to K is the official situation argument will be completely determined by the K relation at and (expressing what is known in situation ), and the first the action . This successor state axiom for the E relation argument is just an auxiliary like the in BROKEN(, ).3 will ensure that for all situations DO(, ), the E relation
A fluent is introduced to represent the function ℰ . This on justification terms will be completely determined by is the relation E(, , ), where is an evidence term, the E relation at and the action . is a formula and is a situation. There is no need to Here only knowledge of propositional (or quantifier free represent the evidence function as a function from justi- ground ) formulae is handled. The extension to knowledge ifcations and formulas to a set of situations. Since each of first-order logic with variables and quantifiers is a topic lfuent already contains a situation argument, a relational for future work. lfuent naturally represents the justifications for formulas The successor state axioms for both K and E will be at that situation. developed in several steps through an illustration of pos
We can now introduce the notation Knows(, P, ) ( sible models for an axiomatization. First, we illustrate is justification for knowing P in situation ) as an abbrevi- the initial picture, without any actions. Then, we add a ation for a formula that uses K and E. For example: successor state axiom for K that works with ordinary nonknowledge-producing actions. Finally, we add knowledgeproducing actions.
Knows(, BROKEN(), ) d=ef E(, BROKEN(), )∧
∀′ K(′, ) → BROKEN(, ′).
Note that this notation supplies the appropriate situation argument to the fluent on expansion. It is implicitly requiring the existence of a justification term for the expression that is a candidate for knowledge.
Turning now to knowledge-producing actions imagine a SENSEP action for a fluent P, such that after doing a SENSEP, the truth value of P is known. We introduce the notation Kwhether(P, ) as an abbreviation for a formula indicating that the truth value of a fluent P is known.
Kwhether(, P, ) d=ef
Knows(, P, ) ∨ Knows(, ¬P, ) It will follow from our specification in the next section that ∃ Kwhether(, P, DO(SENSEP, )) holds.
that we are modeling is a knowledge of propositional or quantifierfree first-order formulas. 3Note that using this convention means that the arguments to K are reversed from their normal modal logic use.
For illustration, consider a model for an axiomatization of the initial situation (without any actions) We can imagine that the term S0 denotes the situation S1 (an object in a model). Three situations (S1, S2 and S3) are accessible via the K relation from S1. Proposition ¬BROKEN is true in all of these situations5, while proposition Q is true in S1 and S3, but is false in S2. We also, have in S0 that 1 is evidence for ¬BROKEN(OBJ1). Hence, E(1, ¬BROKEN(OBJ1), S0) holds. Therefore6 the agent in S0 knows ¬BROKEN(obj1), but does not know Q. In other words, we have 4Here sorts or types are simply one place predicates. But commonly ∀:SIT is used an abbreviation for ∀ SIT() → 5For expository purposes we speak informally of a proposition being true in a situation rather than saying that the situation is in the relation denoted by the predicate symbol P. 6Note that the the justification is needed for the agent to know a proposition. In [9], anything true in all accessible worlds is known. a model of Knows(1, ¬BROKEN(obj1), S0) and ∀¬Knows(, Q, S0). 5.1.1. Setting up the Initial Picture Restrictions need to be placed on the K relation so that it correctly models the accessibility relation of a particular justification logic. The problem is to do this in a way that does not interfere with the successor state axioms for K, which must completely specify the K relation for non-initial situations. The solution is to axiomatize the restrictions for the initial situation and then verify that the restrictions are then obeyed at all situations.
The sort INIT is used to restrict variables to range only over S0 and those situations accessible from S0. It is necessary to stipulate that: used to indicate that the variable ranges over justifications, at times without explicit indication of the sort. Both of these will be explained shortly. We also need a sort FORM to range over formulas of propositional logic. Variables and are used to range over formulas without explicit use of the sort predicate.
Additionally, for every : ∈ , we need to have: ∀:INIT E(, , ) (9)
Now the language includes more terms describing situations. In addition to S0, there is the DO function along
INIT(S0) with the presence of actions in the language. More sit∀, 1INIT(1) → (K(, 1) → INIT()) uations are added to the model described earlier. The ∀, 1¬INIT(1) → (K(, 1) → ¬INIT()) function denoted by DO maps the initial set of situations INIT() → ¬∃′( = DO(, ′)) to these other situations. (These in turn are mapped to yet other situations, and so on). These situations intuWe want to require that the situation S0 is a member itively represent the occurrence of actions. The situations of the sort INIT, everything K-accessible from an INIT S1, S2, and S3 are mapped by DO and the action terms situation is also INIT, and that everything K-accessible MOVE, PICKUP, or DROP to various other situations. The from a situation that is not INIT is also not INIT. Also it is question is what is the K relation between these situations. necessary to require that none of the situations that result Our axiomatization of the K relation places constraints from the occurrence of an action are INIT. We also need on the K relation in the models. We first cover the simto specify that everything of type INIT is also of type SIT. pler case of non-knowledge-producing actions and then
Given the decision that we are to use a particular modal discuss knowledge-producing actions. logic of knowledge, it is necessary to axiomatize the corre- For non-knowledge-producing actions (e.g. DROP()), sponding restrictions that need to be placed on the K rela- the specification is as follows: tion. These are listed below and are merely first-order representations of the conditions on the accessibility relations K(′′, DO(DROP(), )) ≡ for the standard modal logics of knowledge discussed in ∃′ (POSS(DROP(), ′) ∧ K(′, ) ∧ (10) the literature [34, 35, 36, 37]. All of these modal logics ′′ = DO(DROP(), ′)) have corresponding justification logics [ 17, 19, 20, 21].
The reflexive restriction is always added as we want a The idea here is that as far as the agent at world knows, modal logic of knowledge. Some subset of the other re- he could be in any of the worlds ′ such that K(′, ). strictions are then added to semantically define a particular At DO(DROP(), ) as far as the agent knows, he can be modal logic7. in any of the worlds DO(DROP(), ′) for any ′ such that both K(′, ) and POSS(DROP(), ′) hold. So the Reflexive ∀1:INIT K(1, 1) only change in knowledge (given only 10) that occurs in Euclidean ∀1:INIT, 2:INIT, 3:INIT moving from to DO(DROP(), ) is the knowledge that K(2, 1) ∧K(3, 1) → K(3, 2) the action DROP has been performed.
To continue our example of the initial arrangement Symmetric ∀1:INIT, 2:INIT K(2, 1) → K(1, 2) of situations and the fluents ¬ BROKEN(OBJ1) and Q, we imagine that an action named DROP(OBJ1) makes Transitive ∀1:INIT, 2:INIT, 3:INIT BROKEN(OBJ1) true, but does not change the truth value
K(2, 1) ∧ K(3, 2) → K(3, 1) of Q.
For clarity a sort JUST is used to specify which objects We now utilize a simpler version of the previously given are justifications. The letter t, possibly with subscripts, is positive effect and negative effect axioms for BROKEN. Now 11 is a positive effect axiom for the uflent BROKEN. 7As in [9] it can be shown that these properties persist through all successor situations. [( = DROP() → BROKEN(, DO(, ))
(11) ∧ . . . ∧ . . . We now have additional situations resulting from the DO function applied to DROP(OBJ1) and the successor state axiom for K fully specifies the K relation between these situations. Here we have the situation do(drop(obj1,S0), denoted by DO(DROP(OBJ1, S0), which represents the result of performing a drop action in the situation denoted by S0.
Our axiomatization requires that this situation be K related only to the situations do(drop(obj1),S1), do(drop(obj1),S2) and do(drop(obj1),S3).
The DROP(OBJ1) action does not affect the truth of Q, but makes BROKEN(OBJ1) true. So, we see that proposition BROKEN is true in each of do(drop,S1), do(drop,S2) and do(drop,S3), while proposition Q is true in do(drop,S1) and do(drop,S3), but is false in do(drop,S2). Therefore in do(drop,S1) the fluent BROKEN(OBJ1) holds in all K accessible situations, but this is not the case for the fluent Q.
Corresponding to all the successor-state axioms of the form given in (7), there must be a single successor-state axiom for E that specifies all the possible ways a formula is justified in a situation resulting from an action in terms of the action that occurred as well as the justifications for formulae in the prior situation. Most justifications will be passed onto the resulting situation resulting from the action occurring. Some will not when they are replaced by new justifications. The successor-state axiom for E is given in equation 15. Here MKJUST is a gensym like function that creates a justification out of the action that has occurred. The intuition is that the occurrence of the action is the justification for the knowledge of the changes that are caused by the action.
In general, we assume that there are fluents ( P1 through P), each of which has a positive and negative effect axiom and a compiled successor-state axiom. The successor-state axiom for E needs to allow justifications that are present at available at DO(, ), unless it is the case that the action alters the truth value of a fluent in which case there is a new justification that overrides any ∧ ((¬ P+ (, ) ∨ ( ̸= P)) ∧ (¬ P− (, ) ∨ ( ̸= ¬P)))]
∧ [(( = MKJUST(DO(, )) ∧ = P1 → P+1 (, ))
∧ ( = MKJUST(DO(, )) ∧ = ¬P1 → P+1 (, )))
∧ (( = MKJUST(DO(, )) ∧ = P → P+ (, ))
∧ ( = MKJUST(DO(, )) ∧ = ¬P → P+ (, )))
∧ (( = MKJUST(DO(, )) ∧ = P → P+ (, ))
∧ ( = MKJUST(DO(, )) ∧ = ¬P → P+ (, )))]
(15) The first part of equation 15 ensures that if none of the conditions for creating a new justification for a fluent are met then the justification for a formula that is present at is also present at DO(, ). So, this means for every fluent for which it is not the case that the positive effect axiom is true at and the formula is the fluent and it is not the case that the negative effect axiom is true at and the formula is not the negation of the fluent. Otherwise, one of the positive or negative effect formulae must be true and the formula instantiating must be either the positive fluent or negation of the fluent. Under this second case, a new justification is created for DO(, ). To return to our running example, we have
have as the successor state axiom for : ∀:JUST, :JUST E(, , DO(, )) ≡ [(E(, , ) ∧ = ∧ = ∧ ((¬( = DROP()) ∨ ( ̸= BROKEN()))
We need the following to handle the application axiom and the sum axiom.
∀:JUST ∀:JUST ∀:SIT E(, → , ) ∧ E(, , )
→ E( · , , DO(THINK1, ))
∀:JUST :JUST ∀:SIT E(, , )
→ E( + , , DO(THINK2, ) and ∀:JUST, :JUST ∀:SIT E(, , )
→ E( + , , DO(THINK2,, ) Note that one act of thinking THINK1 , does each possible execution of the rule of modus ponens. Both THINK2 and THINK2 are needed for each possible application of the sum rule. To return to our running axiomatization, we (17) (18) (19)
Now consider the simple case of a knowledge-producing action SENSE that determines whether or not the fluent Q is true (following Moore [33, 8]). There may also be ordinary actions, which are not knowledge-producing.
We imagine that the action has an associated sensing result function. This result is “YES” if “Q” is true and “NO” otherwise. The symbols are given in quotes to indicate that they are not fluents. We axiomatize the sensing result as follows:
SR(SENSE, ) = ≡ ( = “YES” ∧ Q()) ∨ ( = “NO” ∧ ¬Q()) The question that we need to consider is what situations are K accessible from DO(SENSE, 0).
K(′′, DO(SENSEQ, )) ≡ ∃′ (POSS(SENSEQ, ′) ∧ K(′, ) ∧ ′′ = DO(SENSE, ′) ∧
SR(SENSEQ, ) = SR(SENSE, ′)) (21) (22) Again, as far as the agent at world knows, he could be in any of the worlds ′ such that K(′, ) holds. At DO(SENSE, ) as far as the agent knows, he can be in any of the worlds DO(SENSE, ′) such that K(′, ) and POSS(SENSE, ′) hold by (22), and also Q() ≡ Q(′) by the combination of (21) and (22) holds. The idea here is that in moving from to DO(SENSE, ), the agent not only knows that the action SENSE has been performed (since every accessible situation results from the DO function and the SENSE action), but also the truth value of the predicate Q. Observe that the successor state axiom for Q (sentence 14) guarantees that Q is true at DO(SENSE, ) if and only if Q is true at , and similarly for ′ and DO(SENSE, ′). Therefore, Q has the same truth value in all worlds ′′ such that K(′′, DO(SENSE, )), and so Kwhether(Q, DO(SENSE, )) is true.
To return to our running example, which is the illustration of the result of a SENSE action, note that the only situations accessible via the K relation from do(sense,S1) (denoted by DO( SENSE, 0)) are do(sense, S1) and do(sense,S3). The situation do(sense,S2) is not K accessible. Therefore Knows(, P, DO(SENSE, S0)) is true as it was before the action was executed, but also now Knows(′, Q, DO(SENSE, S0)) is true where ′ is a new justification as introduced in the successor state axiom for E given below. The knowledge of the agent being modeled has increased.
In general, there may be many knowledge-producing actions, as well as many ordinary actions. To characterize all of these, we have a function SR (for sensing result), and for each action , a sensing-result axiom of the form: SR( (⃗), ) = ≡ (⃗, , ) (23) For ordinary actions, the result is always the same, with the specific result not being significant. For example, we could have:
SR(PICKUP(), ) = ≡ = “OK” (24)
Successor State Axiom for K (′′, DO(, )) ≡ (∃ ′ ′′ = DO(, ′) ∧ (′, ) ∧ POSS(, ′)
∧ SR(, ) = SR(, ′)) The relation K at a particular situation DO(, ) is completely determined by the relation at and the action .
We need a successor state axiom for E and the sensing action.
Consider the red barn example mentioned earlier8. We have two sensing actions; SENSE∧ and SENSE . The ifrst represents the action of sensing whether there is a red barn and the second is the sensing of whether there is a barn. Note that by the problem description only the (25) first is a causal justification for knowledge. This is metainformation, not available to the agent.
The sensing result axioms are as follows:
SR(SENSE∧, ) = ≡ ( = “YES” ∧ (RED() ∧ BARN()) ∨ ( = “NO” ∧ ¬(RED() ∧ BARN()) SR(SENSE , ) = ≡ ( = “YES” ∧ BARN()) ∨ ( = “NO” ∧ ¬BARN()) (27) (28)
∀:JUST1:JUST2:JUST E(, , DO(, )) ≡ [(( = 1 · 2 ∧ E(1, → , )∧
E(2, , ) ∧ ¬(1 · 2, , ))
→ = THINK1] ∧ [( = MKJUST(DO(SENSE , )) ∧ ( = BARN ∨ = ¬BARN))
→ = SENSE ∧ ( = MKJUST(DO(SENSE∧())) ∧ ( = BARN ∧ RED ∨ = ¬BARN ∧ RED)) → = SENSE∧] (29)
It is also necessary to add the following: BARN(0) and RED(0). Additionally, we need to add a propositional axiom ( ∧ ) → to the constant specification. So, it is justified by justification A.
∀:INIT E(A, ( ∧ ) → , ) (30) The successor state axioms for BARN and RED need to be added, but they are simple since there are no actions that change these fluents. The successor state axioms for the sensing action are of the form given in the previous section.
Now the axiomatization entails
Knows(MKJUST(DO(SENSE , S0)),
BARN, DO(SENSE , S0)) (31) and
Knows((A · MKJUST(DO(SENSE∧, S0))),
BARN, DO(THINK, DO(SENSE∧, S0)))) (32) By the meta-information given in the problem description only the second is true knowledge. The formalism allows the two justifications for the knowledge of barn to be distinguished, while the modal logic based approach of [9] does not allow them to be distinguished.
This paper has presented preliminary results on integrating the justification logic model of knowledge into the situation calculus with knowledge and knowledge producing actions. The positive results of this work is that (as compared to the situation calculus with a modal view of knowledge) one is able to make a more fine-grained representation of the different ways an agent may have knowledge. Additionally, the agent is not logically omniscient.
Some of the properties [9] for the situation calculus with knowledge carry over to the case of justified knowledge. Space does not permit a full exposition. But all of these properties show that actions only affect knowledge in the appropriate way. Note that the property (from [9]) that agents know the consequences of acquired knowledge does not hold as knowledge of the consequences depends on having the justification that incorporates the reasoning involved.
Current work involves the development of regression to facilitate reasoning with the logic. The notion of thinking and amount of effort needs to be compared to similar notions in the literature [38, 39]. Additionally, the work can be extended to handle knowledge of sentences in full ifrst-order logic (with quantifiers) as has been done within the literature of justification logic [20].
Although the practical applications are limited, the steps taken set the basis for further work. One augmentation of significance will be the incorporation and elimination of justifications. Then the framework can model evidential reasoning. This can draw on justification awareness models [20] where the agent can have knowledge of the degree of reliability of various kinds of justifications. An additional topic for exploration is the use of justification terms for generating explanations of the beliefs of the agent.