Vol-3197/paper10
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | scientific paper published in CEUR-WS Volume 3197 |
| id | Vol-3197/paper10 |
| wikidataid | Q117341818βQ117341818 |
| title | A Situation-Calculus Model of Knowledge and Belief Based on Thinking About Justifications |
| pdfUrl | https://ceur-ws.org/Vol-3197/paper10.pdf |
| dblpUrl | https://dblp.org/rec/conf/nmr/Scherl22 |
| volume | Vol-3197βVol-3197 |
| session | β |
A Situation-Calculus Model of Knowledge and Belief Based on Thinking About Justifications
A situation-calculus model of knowledge and belief based
on thinking about justifications
Richard B. Scherl1
1
Monmouth University, West Long Branch, NJ, 07764, USA
Abstract
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.
Keywords
Situation Calculus, Knowledge, Justification Logic
1. Introduction The possible-world analysis of knowledge only handles
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 justi-
ception, and action of an agent [1, 2]. Axioms are used to fication 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 papier-
tified 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 [10]. An agent, S agent βknowingβ that a barn is red. One way is accidental.
knows that p iff (1) p is true; (2) S believes that p; (3) S is Henry may have a barn perception, and then believe that
justified in believing that p. There has been much philo- the object is a barn, but this is only accidentally true
sophical discussion of counterexamples to the sufficiency and therefore we donβt want to say that Henry knows the
of this tripartite analysis [11, 12, 13, 14, 15, 16]. object is a barn. If Henry perceives that the object is a red
barn, he is then justified in knowing that the object is a
NMR 2022: 20th International Workshop on Non-Monotonic Reason-
ing, August 7β9, 2022, Haifa, Israel
red barn and can then infer correctly that the object is a
$ rscherl@monmouth.edu (R. B. Scherl) barn. Modal logic does not distinguish between these two
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License ways of knowing/believing.
Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
104
οΏ½ 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 justifi-
cation of a proposition. In one case, there is a justification P OSS(DROP(π₯), π ) β‘ H OLDING(π₯, π ) (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 fluent πΉ , 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 con-
this 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- B ROKEN.
namic epistemic logic [24, 25, 26].
[(π = DROP(π¦) β§ F RAGILE(π¦))
β¨
2. The Situation Calculus and the (5)
(βπ π = EXPLODE(π) β§ N EXTO(π, π¦, π ))]
Frame Problem β B ROKEN(π¦, DO(π, π ))
The situation calculus (following the presentation in [4]) is Sentence 6 is a negative effect axiom for B ROKEN.
a first-order language for representing dynamically chang-
π = REPAIR(π¦) β Β¬B ROKEN(π¦, 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, B ROKEN (π₯, π ) 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. There-
functional 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 ax-
action πΌ(π₯ β ), 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 complete-
ness assumption.
β ), π ) β‘ ππΌ (π₯
P OSS(πΌ(π₯ β , π ) (1) Successor State Axiom
1
By convention, variables are indicated by lower-case letters in italic + β
font. When quantifiers are not indicated, the variables are implicitly F(DO(π, π )) β‘ πΎF (π, π ) β¨ (F(π ) β§ Β¬πΎF (π, π ))
universally quantified. (7)
105
οΏ½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
fluent 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 B ROKEN is obtained. Given a Fitting model β³ = β¨π’, β, β°, π±β©, the truth of
a formula π at a possible world Ξ, i.e., β³, Ξ |= π is
B ROKEN(π¦, DO(π, π )) β‘ given as follows:
(π = DROP(π¦) β§ F RAGILE(π¦))β¨
(8)
(βπ π = EXPLODE(π) β§ N EXTO(π, π¦, π )) β¨ 1. β³, Ξ |= π iff Ξ β π (π ) for π a propositional
(B ROKEN(π¦, π ) β§ π ΜΈ= REPAIR(π¦)) letter;
2. It is not the case that β³, Ξ |=β₯;
Now note for example that if Β¬B ROKEN(O BJ1 , S0 ) holds, 3. β³, Ξ |= π β π iff it is not the case that
then it also follows (given the unique name axioms) that β³, Ξ |= π or β³, Ξ |= π ;
Β¬B ROKEN(O BJ1 , DO(DROP(O BJ2 ), S0 )) holds as well. 4. β³, Ξ |= (π‘:π) iff Ξ β β°(π‘, π) and for every
β β π’, with Ξββ, β³, β |= π .
3. Justification Logic The last condition is the crucial one. It requires that for
something to be known, it both needs to be believed in the
Justification logic adds to the machinery of proposi- sense that it is true in every accessible world and that π‘ is
tional logic (or quantifier free first-order logic) justifi- relevant evidence for π₯ at that world. So, π‘:π holds iff π
cation terms that are built with justification variables is believable and π‘ is relevant evidence for π.
π₯, π¦, π§, . . . and justification constants π, π, π, . . . (using The following conditions need to be placed on the Evi-
indices π = 1, 2, 3, . . . whenever needed) using the opera- dence function:
tions βΒ·β and β+.β
The logic of justifications includes (in addition to the β’ β°(π , π β π ) β© β°(π‘, π) β β°(π Β· π‘, π )
classical propositional axioms and the rule of Modus Po- β’ β°(π , π) βͺ β°(π‘, π) β β°(π + π‘, π)
nens), the following axioms
These ensure that the application and sum axioms hold.
Application Axiom π : (πΉ β πΊ) β (π‘ : πΉ β [π Β· π‘] : 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
Sum Axioms π : πΉ β [π + π‘] : πΉ , π : πΉ β [π‘ + π ] : πΉ awareness can be distinguished through the constant spec-
As needed, the following axioms are added. ification. The constant specification (CS) is a set of jus-
tified formulas (axioms of propositional logic). A model
Factivity π‘ : πΉ β πΉ β³ meets the constant specification πΆπ as long as the
following condition is met:
Positive Introspection π‘ : πΉ β!π‘ : (π‘ : πΉ )
if π : π β πΆπ then β°(π, π) = π’
Negative Introspection Β¬π‘ : πΉ β?π‘ : (Β¬π‘ : πΉ )
This ensures that the axiom is justified in all possible
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 justifi-
els. 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.
106
οΏ½4. Representing Justified For clarity, a number of sorts4 are gradually introduced.
The sort S IT is used to distinguish between situations
Knowledge in the Situation and other objects. It is assumed that we have axioms
Calculus asserting that the initial situation S0 is of type S IT and
that everything of the form DO(π, π ) is of type S IT. The
The approach we take to formalizing knowledge2 is to letter π , possibly with subscripts, is used to as indication
adapt the semantics of justification logic described in that the variable is of type S IT, without explicit use of the
the previous section to the situation calculus. Following sort predicate.
[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 π β² .
To handle the accessibility relation between situations
Knowledge and Action
(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 B ROKEN(π¦, π ).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
fications and formulas to a set of situations. Since each of first-order logic with variables and quantifiers is a topic
fluent already contains a situation argument, a relational for future work.
fluent 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 non-
def knowledge-producing actions. Finally, we add knowledge-
Knows(π‘, B ROKEN(π¦), π ) = E(π‘, B ROKEN(π¦), π )β§ producing actions.
βπ β² K(π β² , π ) β B ROKEN(π¦, π β² ).
Note that this notation supplies the appropriate situation 5.1. The Initial Picture: Without Actions
argument to the fluent on expansion. It is implicitly requir-
For illustration, consider a model for an axiomatization
ing the existence of a justification term for the expression
of the initial situation (without any actions) We can
that is a candidate for knowledge.
imagine that the term S0 denotes the situation S1 (an
Turning now to knowledge-producing actions imagine
object in a model). Three situations (S1, S2 and S3)
a SENSE P action for a fluent P, such that after doing a
are accessible via the K relation from S1. Proposition
SENSE P , the truth value of P is known. We introduce the
Β¬B ROKEN is true in all of these situations5 , while
notation Kwhether(P, π ) as an abbreviation for a formula
proposition Q is true in S1 and S3, but is false in S2. We
indicating that the truth value of a fluent P is known.
also, have in S0 that π‘1 is evidence for Β¬B ROKEN(OBJ1 ).
def Hence, E(π‘1 , Β¬B ROKEN(OBJ1 ), S0 ) holds. There-
Kwhether(π‘, P, π ) =
fore6 the agent in S0 knows Β¬B ROKEN(obj1 ),
Knows(π‘, P, π ) β¨ Knows(π‘, Β¬P, π )
but does not know Q. In other words, we have
It will follow from our specification in the next section
that
4
βπ‘ Kwhether(π‘, P, DO(SENSE P , π )) holds. Here sorts or types are simply one place predicates. But commonly
βπ :S IT π is used an abbreviation for βπ S IT(π ) β π
2 5
The situation calculus is a first-order formalism. But the knowledge For expository purposes we speak informally of a proposition being
that we are modeling is a knowledge of propositional or quantifier- true in a situation rather than saying that the situation is in the
free first-order formulas. relation denoted by the predicate symbol P.
3 6
Note that using this convention means that the arguments to K are Note that the the justification is needed for the agent to know a
reversed from their normal modal logic use. proposition. In [9], anything true in all accessible worlds is known.
107
οΏ½a model of Knows(π‘1 , Β¬B ROKEN(obj1 ), S0 ) and used to indicate that the variable ranges over justifications,
βπ‘Β¬Knows(π‘, Q, S0 ). at times without explicit indication of the sort. Both of
these will be explained shortly. We also need a sort F ORM
5.1.1. Setting up the Initial Picture to range over formulas of propositional logic. Variables
π and π are used to range over formulas without explicit
Restrictions need to be placed on the K relation so that it use of the sort predicate.
correctly models the accessibility relation of a particular Additionally, for every π‘ : π β πΆπ, we need to have:
justification logic. The problem is to do this in a way
that does not interfere with the successor state axioms βπ :I NIT E(π‘, π, π ) (9)
for K, which must completely specify the K relation for
non-initial situations. The solution is to axiomatize the This specifies that the constant specification holds in the
restrictions for the initial situation and then verify that the set of initial situations.
restrictions are then obeyed at all situations.
The sort I NIT is used to restrict variables to range only 5.2. Adding Ordinary Actions
over S0 and those situations accessible from S0 . It is
necessary to stipulate that: Now the language includes more terms describing situ-
ations. In addition to S0 , there is the DO function along
I NIT(S0 ) with the presence of actions in the language. More sit-
βπ , π 1 I NIT(π 1 ) β (K(π , π 1 ) β I NIT(π )) uations are added to the model described earlier. The
βπ , π 1 Β¬I NIT(π 1 ) β (K(π , π 1 ) β Β¬I NIT(π )) function denoted by DO maps the initial set of situations
I NIT(π ) β Β¬βπ β² (π = DO(π, π β² )) to these other situations. (These in turn are mapped to
yet other situations, and so on). These situations intu-
We want to require that the situation S0 is a member itively represent the occurrence of actions. The situations
of the sort I NIT, everything K-accessible from an I NIT S1, S2, and S3 are mapped by DO and the action terms
situation is also I NIT, and that everything K-accessible MOVE, PICKUP, or DROP to various other situations. The
from a situation that is not I NIT is also not I NIT. 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 I NIT. We also need on the K relation in the models. We first cover the sim-
to specify that everything of type I NIT 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 rep-
resentations of the conditions on the accessibility relations K(π β²β² , DO(DROP(π₯), π )) β‘
for the standard modal logics of knowledge discussed in βπ β² (P OSS(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 P OSS(DROP(π₯), π β² ) hold. So the
Reflexive βπ 1 :I NIT K(π 1 , π 1 ) only change in knowledge (given only 10) that occurs in
Euclidean βπ 1 :I NIT, π 2 :I NIT, π 3 :I NIT 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 :I NIT, π 2 :I NIT K(π 2 , π 1 ) β K(π 1 , π 2 ) of situations and the fluents Β¬ B ROKEN(OBJ1 ) and Q,
we imagine that an action named DROP(OBJ1 ) makes
Transitive βπ 1 :I NIT, π 2 :I NIT, π 3 :I NIT B ROKEN(OBJ1 ) true, but does not change the truth value
K(π 2 , π 1 ) β§ K(π 3 , π 2 ) β K(π 3 , π 1 ) of Q.
For clarity a sort J UST 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 B ROKEN.
Now 11 is a positive effect axiom for the fluent B ROKEN.
7
As in [9] it can be shown that these properties persist through all
successor situations. [(π = DROP(π¦) β B ROKEN(π¦, DO(π, π )) (11)
108
οΏ½Sentence 12 is a negative effect axiom for B ROKEN. justification involving the fluent that was there before.
π = REPAIR(π¦) β Β¬B ROKEN(π¦, DO(π, π )) (12) βπ‘:JUST E(π, π, DO(π, π )) β‘
[E(π‘, π, π ) β§ π‘ = π β§ π = π β§
Now the simplified successor state axiom is: +
(((Β¬πΎP (π, π ) β¨ (π ΜΈ= P1 )) β§
1
β
B ROKEN(π¦, DO(π, π )) β‘ (Β¬πΎP (π, π ) β¨ (π ΜΈ= Β¬P1 )))
1
(π = DROP(π¦)β¨ (13) β§
(B ROKEN(π¦, π ) β§ π ΜΈ= REPAIR(π¦)) ..
.
For Q, we have β§
+
((Β¬πΎP (π, π ) β¨ (π ΜΈ= Pπ )) β§
π
Q(DO(π, π )) β‘ Q(π ) (14) (Β¬πΎPβ
(π, π ) β¨ (π ΜΈ= Β¬Pπ )))
π
β§
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 ((Β¬πΎP +
(π, π ) β¨ (π ΜΈ= Pπ )) β§
have the situation do(drop(obj1,S0), denoted by π
β
(Β¬πΎP (π, π ) β¨ (π ΜΈ= Β¬Pπ )))]
DO ( DROP ( OBJ 1 , S 0 ), which represents the result of per- π
forming a drop action in the situation denoted by S0 . β§
+
Our axiomatization requires that this situation be K [((π = MKJUST(DO(π, π )) β§ π = P1 β πΎP (π, π ))
1
related only to the situations do(drop(obj1),S1), β§
+
do(drop(obj1),S2) and do(drop(obj1),S3). (π = MKJUST(DO(π, π )) β§ π = Β¬P1 β πΎP (π, π )))
1
The DROP(OBJ1 ) action does not affect the truth of β§
Q, but makes B ROKEN(OBJ1 ) true. So, we see that ..
proposition B ROKEN 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 ((π = MKJUST(DO(π, π )) β§ π = Pπ β πΎP (π, π ))
π
false in do(drop,S2). Therefore in do(drop,S1) β§
the fluent B ROKEN(OBJ1 ) holds in all K accessible situa- +
(π = MKJUST(DO(π, π )) β§ π = Β¬Pπ β πΎP (π, π )))
π
tions, 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 +
((π = MKJUST(DO(π, π )) β§ π = Pπ β πΎP (π, π ))
π
of the action that occurred as well as the justifications for β§
formulae in the prior situation. Most justifications will (π = MKJUST(DO(π, π )) β§ π = Β¬Pπ β
be passed onto the resulting situation resulting from the +
πΎP (π, π )))]
action occurring. Some will not when they are replaced π
(15)
by new justifications. The successor-state axiom for E
The first part of equation 15 ensures that if none of the
is given in equation 15. Here MKJUST is a gensym like
conditions for creating a new justification for a fluent are
function that creates a justification out of the action that
met then the justification for a formula that is present at π
has occurred. The intuition is that the occurrence of the
is also present at DO(π, π ). So, this means for every fluent
action is the justification for the knowledge of the changes
for which it is not the case that the positive effect axiom
that are caused by the action.
is true at π and the formula π is the fluent and it is not
In general, we assume that there are π fluents (P1
the case that the negative effect axiom is true at π and the
through Pπ ), each of which has a positive and negative
formula π is not the negation of the fluent. Otherwise,
effect axiom and a compiled successor-state axiom. The
one of the positive or negative effect formulae must be
successor-state axiom for E needs to allow justifications
true and the formula instantiating π must be either the
that are present at π available at DO(π, π ), unless it is the
positive fluent or negation of the fluent. Under this second
case that the action π alters the truth value of a fluent in
case, a new justification is created for DO(π, π ).
which case there is a new justification that overrides any
109
οΏ½ To return to our running example, we have have as the successor state axiom for πΈ:
βπ‘:JUST, π:JUST E(π‘, π, DO(π, π )) β‘ βπ‘:JUST, π:JUST E(π‘, π, DO(π, π )) β‘
[(E(π‘, π, π ) β§ π‘ = π β§ π = π β§ [(E(π‘, π, π ) β§ π‘ = π β§ π = π β§
((Β¬(π = DROP(π¦)) β¨ (π ΜΈ= B ROKEN(π¦)))
((Β¬(π = DROP(π¦)) β¨ (π ΜΈ= B ROKEN(π¦))) β§
β§ (Β¬(π = REPAIR(π¦)) β¨ (π ΜΈ= Β¬B ROKEN(π¦))))]
(Β¬(π = REPAIR(π¦)) β¨ (π ΜΈ= Β¬B ROKEN(π¦))))] β§
β§ [(π‘ = MKJUST(DO(D ROP(π₯), π ))β§
[(π‘ = MKJUST(DO(D ROP(π₯), π ))β§ π = B ROKEN(π₯) β π = DROP(π₯))
π = B ROKEN(π₯) β π = DROP(π₯)) β§
β§ (π‘ = MKJUST(DO(REPAIR(π₯), π ))β§
(π‘ = MKJUST(DO(REPAIR(π₯), π ))β§ π = Β¬B ROKEN(π₯) β π = REPAIR(π¦))]
π = Β¬B ROKEN(π₯) β π = REPAIR(π¦))] β§
(16) [((π‘ = π1 Β· π2 β§ E(π1 , π β π, π ) β§ E(π2 , π, π ) β§
as the successor-state axiom. This ensures that if the Β¬πΈ(π1 Β· π2 , π, π )) β (π = THINK1 ))
justification is for anything other than Β¬B ROKEN, then it β§
persists in the E relation into the situation resulting from (π‘ = π1 + π2 β§ E(π1 , π, π ) β§
the action π₯. But if the action is a DROP(π₯) action then a Β¬πΈ(π1 + π2 , π, π )) β π = THINK2π )
new justification is created for B ROKEN(π₯). β§
The following two sentences hold in this model: ((π‘ = π2 + π1 β§ E(π1 , π, π ) β§
Β¬πΈ(π2 + π1 , π, π )) β π = THINK2π )]
Knows(MKJUST(DO(DROP(OBJ1 ), S0 )), (20)
Β¬B ROKEN(OBJ1 )DO(DROP(OBJ1 ), S0 )) Note that thinking actions for positive and negative intro-
and spection may also be added. In this case the expansion of
the formula for Knows will also need to be augmented so
βπ‘ Β¬Knows(π‘, Q, DO(DROP, S0 )) that knowledge of knowledge and knowledge of the lack
The agentβs knowledge of Q has remained the same, of knowledge can be expressed.
and the knowledge of B ROKEN(OBJ1 ) is a result of the
knowledge of the effect of the action DROP, and the justi-
5.4. Adding Knowledge-Producing
fication provided by the successor-state axiom for E.
Actions
5.3. Adding Thinking Actions Now consider the simple case of a knowledge-producing
action SENSEπ that determines whether or not the fluent
We need the following to handle the application axiom Q is true (following Moore [33, 8]). There may also be
and the sum axiom. ordinary actions, which are not knowledge-producing.
βπ‘:J UST βπ:J UST βπ :S IT E(π, π β π, π ) We imagine that the action has an associated sensing re-
β§ E(π‘, π, π ) (17) sult function. This result is βYESβ if βQβ is true and βNOβ
β E(π Β· π‘, π, DO(THINK1 , π )) otherwise. The symbols are given in quotes to indicate
that they are not fluents. We axiomatize the sensing result
For the sum axiom we need as follows:
βπ‘:J UST π:J UST βπ :S IT E(π, π, π ) β‘ (π = βYESβ β§ Q(π ))
SR ( SENSE π , π ) = π
(18) (21)
β E(π + π‘, π, DO(THINK2π , π ) β¨ (π = βNOβ β§ Β¬Q(π ))
and The question that we need to consider is what situations
are K accessible from DO(SENSEπ , π 0 ).
βπ‘:J UST, π:J UST βπ :S IT E(π, π, π )
(19)
β E(π‘ + π, π, DO(THINK2π, , π ) K(π β²β² , DO(SENSE Q , π )) β‘
βπ β² (P OSS(SENSE Q , π β² ) β§ K(π β² , π ) β§
Note that one act of thinking THINK1 , does each possible (22)
π β²β² = DO(SENSEπ , π β² ) β§
execution of the rule of modus ponens. Both THINK2π β²
SR ( SENSE Q , π ) = SR ( SENSE π , π ))
and THINK2π are needed for each possible application of
the sum rule. To return to our running axiomatization, we 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
110
οΏ½any of the worlds DO(SENSEπ , π β² ) such that K(π β² , π ) and action.
P OSS(SENSEπ , π β² ) hold by (22), and also Q(π ) β‘ Q(π β² )
by the combination of (21) and (22) holds. The idea here βπ‘:JUST, π:JUST E(π‘, π, DO(π, π )) β‘
is that in moving from π to DO(SENSEπ , π ), the agent not [(E(π‘, π, π ) β§ π‘ = π β§ π = π β§
only knows that the action SENSEπ has been performed ((Β¬(π = DROP(π¦)) β¨ (π ΜΈ= B ROKEN(π¦)))
(since every accessible situation results from the DO func- β§
tion and the SENSEπ action), but also the truth value of the (Β¬(π = REPAIR(π¦)) β¨ (π ΜΈ= Β¬B ROKEN(π¦))))]
predicate Q. Observe that the successor state axiom for Q β§
(sentence 14) guarantees that Q is true at DO(SENSEπ , π ) [(π‘ = MKJUST ( DO (D ROP(π₯), π ))β§
if and only if Q is true at π , and similarly for π β² and π = B ROKEN(π₯) β π = DROP(π₯))
β²
DO ( SENSE π , π ). Therefore, Q has the same truth value
β§
β²β² β²β²
in all worlds π such that K(π , DO(SENSEπ , π )), and so (π‘ = MKJUST ( DO ( REPAIR (π₯), π ))β§
Kwhether(Q, DO(SENSEπ , π )) is true. π = Β¬B ROKEN(π₯) β π = REPAIR(π¦))]
To return to our running example, which is the il- β§
lustration of the result of a SENSEπ action, note that [((π‘ = π 1 Β· π 2 β§ E(π1 , π β π, π ) β§ E(π2 , π, π ) β§
the only situations accessible via the K relation from Β¬πΈ(π 1 Β· π2 , π, π )) β (π = THINK1 ))
do(sense,S1) (denoted by DO( SENSEπ , π 0 )) are β§
do(sense, S1) and do(sense,S3). The situ- (π‘ = π1 + π2 β§ E(π1 , π, π ) β§
ation do(sense,S2) is not K accessible. There- Β¬πΈ(π1 + π2 , π, π )) β π = THINK2π )
fore Knows(π‘, P, DO(SENSEπ , S0 )) is true as it was β§
before the action was executed, but also now ((π‘ = π 2 + π 1 β§ E(π1 , π, π ) β§
β² β²
Knows(π‘ , Q, DO(SENSEπ , S0 )) is true where π‘ is a new Β¬πΈ(π 2 + π1 , π, π )) β π = THINK2π )]
justification as introduced in the successor state axiom β§
for E given below. The knowledge of the agent being [(π‘ = MKJUST(DO(SENSEπ , π ))β§
modeled has increased. (π = π β¨ π = Β¬π)) β (π = SENSEπ )]
In general, there may be many knowledge-producing (26)
actions, as well as many ordinary actions. To characterize For every sensing-result axiom of the form (23) we
all of these, we have a function SR (for sensing result), need a clause in the axiom of the form (26). Note that
and for each action πΌ, a sensing-result axiom of the form: now the general form of the successor-state axiom for E
as given in equation 15 needs to be augmented (in the
SR (πΌ(π₯β ), π ) = π β‘ ππΌ (π₯ β , π, π ) (23) same manner as was done for the running example) with
the thinking actions that the axiomatizer decides to use
For ordinary actions, the result is always the same, with and also the available sensing actions.
the specific result not being significant. For example, we
could have:
6. Example
SR ( PICKUP(π₯), π ) = π β‘ π = βOKβ (24)
Consider the red barn example mentioned earlier8 . We
The successor state axiom for K is as follows: have two sensing actions; SENSEπ΅β§π
and SENSEπ΅ . The
Successor State Axiom for K first represents the action of sensing whether there is a
red barn and the second is the sensing of whether there
πΎ(π β²β² , DO(π, π )) β‘ is a barn. Note that by the problem description only the
(β π β² π β²β² = DO(π, π β² ) first is a causal justification for knowledge. This is meta-
(25)
β§ πΎ(π β² , π ) β§ P OSS(π, π β² ) information, not available to the agent.
β§ SR(π, π ) = SR(π, π β² )) The sensing result axioms are as follows:
The relation K at a particular situation DO(π, π ) is com- SR ( SENSE π΅β§π
, π ) = π β‘
pletely determined by the relation at π and the action π. (π = βY ESβ β§ (R ED(π ) β§ BARN(π ))
We need a successor state axiom for E and the sensing β¨ (π = βN Oβ β§ Β¬(R ED(π ) β§ BARN(π ))
(27)
SR ( SENSE π΅ , π ) = π β‘
(π = βY ESβ β§ BARN(π )) (28)
β¨ (π = βN Oβ β§ Β¬BARN(π ))
8
Here the example follows [17, 19].
111
οΏ½ We axiomatize E following the approach in the previous Some of the properties [9] for the situation calculus
sections. Note that there are no successor state axioms inwith knowledge carry over to the case of justified knowl-
this example. edge. Space does not permit a full exposition. But all of
these properties show that actions only affect knowledge
βπ‘:JUSTπ1 :JUSTπ2 :JUST E(π‘, π, DO(π, π )) β‘ in the appropriate way. Note that the property (from [9])
[((π‘ = π1 Β· π2 β§ E(π1 , π β π, π )β§ that agents know the consequences of acquired knowledge
E(π2 , π, π ) β§ Β¬πΈ(π1 Β· π2 , π, π )) does not hold as knowledge of the consequences depends
β π = THINK1 ] on having the justification that incorporates the reasoning
β§ involved.
[(π‘ = MKJUST(DO(SENSEπ΅ , π )) β§ Current work involves the development of regression to
(π = BARN β¨ π = Β¬BARN)) facilitate reasoning with the logic. The notion of thinking
β π = SENSEπ΅ and amount of effort needs to be compared to similar
β§ notions in the literature [38, 39]. Additionally, the work
(π‘ = MKJUST(DO(SENSEπ΅β§π
(π ))) β§ can be extended to handle knowledge of sentences in full
(π = BARN β§ R ED β¨ π = Β¬BARN β§ R ED)) first-order logic (with quantifiers) as has been done within
β π = SENSEπ΅β§π
] the literature of justification logic [20].
(29) Although the practical applications are limited, the
It is also necessary to add the following: BARN(π0 ) steps taken set the basis for further work. One augmen-
and R ED(π0 ). Additionally, we need to add a proposi- tation of significance will be the incorporation and elim-
tional axiom (π΅ β§ π
) β π΅ to the constant specification. ination of justifications. Then the framework can model
So, it is justified by justification A. evidential reasoning. This can draw on justification aware-
ness models [20] where the agent can have knowledge of
βπ :I NIT E(A, (π΅ β§ π
) β π΅, π ) (30) the degree of reliability of various kinds of justifications.
An additional topic for exploration is the use of justifica-
The successor state axioms for BARN and R ED need to
tion terms for generating explanations of the beliefs of the
be added, but they are simple since there are no actions
agent.
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 )),
(31)
BARN, DO(SENSEπ΅ , S0 ))
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.
7. Summary
This paper has presented preliminary results on integrat-
ing the justification logic model of knowledge into the
situation calculus with knowledge and knowledge pro-
ducing 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 omni-
scient.
112
οΏ½References of Philosophy 64 (1967) 357β372.
[16] F. Dretske, Is knowledge closed under known entail-
[1] H. Levesque, G. Lakemeyer, Cognitive robotics, ment? the case against closure, in: Contemporary
in: F. van Harmelen, V. Lifschitz, B. Porter (Eds.), Debates in Epistemology, Blackwell, 2005, pp. 13β
Handbook of Knowledge Representation, Elsevier, 26.
2007. To appear. [17] S. N. Artemov, The logic of justification, The Re-
[2] R. Reiter, Knowledge in Action: Logical Foun- view of Symbolic Logic 1 (2008) 477β513. doi:10.
dations for Specifying and Implementing Dynam- 1017/S1755020308090060.
ical Systems, The MIT Press, Cambridge, Mas- [18] S. Artemov, Explicit provability and constructive
sachusetts, 2001. semantics, Bulletin of Symbolic Logic 7 (2001)
[3] J. McCarthy, Programs with common sense, in: 1β36.
M. Minsky (Ed.), Semantic Information Processing, [19] S. N. Artemov, M. Fitting, Justification logic,
The MIT Press, 1968, pp. 403β418. in: E. N. Zalta (Ed.), The Stanford Ency-
[4] R. Reiter, The frame problem in the situation calcu- clopedia of Philosophy, fall 2012 ed., 2012.
lus: A simple solution (sometimes) and a complete- URL: http://plato.stanford.edu/archives/fall2012/
ness result for goal regression, in: V. Lifschitz (Ed.), entries/logic-justification/.
Artificial Intelligence and Mathematical Theory of [20] S. Artemov, M. Fitting, Justification Logic: Rea-
Computation: Papers in Honor of John McCarthy, soning with Reasons, Cambridge University Press,
Academic Press, San Diego, CA, 1991, pp. 359β Cambridge, UK, 2019.
380. [21] R. Kuznets, T. Studer, Logics of Proofs and Justifi-
[5] J. McCarthy, P. Hayes, Some philosophical prob- catins, College Publications, 2019.
lems from the standpoint of artificial intelligence, [22] S. Kripke, Philosophical Troubles: Collected Papers,
in: B. Meltzer, D. Michie (Eds.), Machine Intel- Volume 1, Oxford University Press, New York, NY,
ligence 4, Edinburgh University Press, Edinburgh, 2011.
UK, 1969, pp. 463β502. [23] R. Scherl, A situation-calculus based theory of jus-
[6] H. Levesque, R. Reiter, Y. LespΓ©rance, F. Lin, R. B. tified knowledge and action, in: Logical Formaliza-
Scherl, Golog: A logic programming language for tions of Commonsense Reasoning: Papers from the
dynamic domains, Journal of Logic Programming 2015 AAAI Spring Symposium Technical Report
(1997). SS-15-04, AAAI Press, Palo Alto, California, 2015,
[7] G. De Giacomo, Y. LespΓ©rance, H. J. Levesque, Con- pp. 134β140.
Golog, a concurrent programming language based [24] A. Baltag, B. Renne, S. Smets, The logic of
on the situation calculus, Artificial Intelligence justified belief change, soft evidence and defea-
(2000) 109β169. sible knowledge, in: L. Ong, R. de Queiroz
[8] R. Moore, A formal theory of knowledge and action, (Eds.), Proceedings of the 19th Workshop on Logic,
in: J. Hobbs, R. Moore (Eds.), Formal Theories Language, Information, and Computation (WoL-
of the Commonsense World, Ablex, Norwood, NJ, LIC 2012), volume 7456 of Lecture Notes in
1985, pp. 319β358. Computer Science, Springer-Verlag Berlin Heidel-
[9] R. Scherl, H. J. Levesque, Knowledge, action, and berg, Buenos Aires, Argentina, 2012, pp. 168β190.
the frame problem, Artificial Intelligence 144 (2003) doi:10.1007/978-3-642-32621-9_13.
1β39. URL: aij03frame.pdf. [25] B. Renne, Dynamic Epistemic Logic with Jus-
[10] J. J. Ichikawa, M. Steup, The analysis of knowledge, tification, Ph.D. thesis, City University of New
in: E. N. Zalta (Ed.), The Stanford Encyclopedia of York, 2008. URL: http://gradworks.umi.com/33/10/
Philosophy, spring 2014 ed., 2014. 3310607.html.
[11] S. Luper, The epistemic closure principle, in: E. N. [26] T. Qualiano, A multi-agent justification logic with
Zalta (Ed.), The Stanford Encyclopedia of Philoso- common knowledge and public announcements,
phy, fall 2012 ed., 2012. 2021. Monmmouth University M.S. Thesis.
[12] K. Lehrer, Theory of Knowledge, Routledge, Lon- [27] E. Pednault, ADL: exploring the middle ground
don, UK, 1990. between STRIPS and the sit uation calculus, in:
[13] V. Hendricks, Mainstream and Formal Epistemol- R. Brachman, H. Levesque, R. Reiter (Eds.), Pro-
ogy, Cambridge University Press, New York, NY, ceedings of the First International Conference on
2007. Princi ples of Knowledge Representation and Rea-
[14] R. Nozick, Philosophical Explanations, The Belk- soning, Morgan Kaufmann Publishers, Inc., San
nap Press of Harvard University Press, Cambridge, Mateo, California, 1989, pp. 324β332.
Massachusetts, 1981. [28] L. Schubert, Monotonic solution of the frame prob-
[15] A. I. Goldman, A causal theory of knowing, Journal lem in the situation calcul us: an efficient method for
113
οΏ½ worlds with fully specified actions, in: H. E. Kyberg,
R. Loui, G. Carlson (Eds.), Knowledge Representa-
tion and Defeasible Reasoning, Kluwer Academic
Press, Boston, Mass., 1990, pp. 23β67.
[29] N. M. Rubtsova, On realization of S5-modality by
evidence terms, Journal of Logic and Computa-
tion 16 (2006) 671β684. doi:10.1093/logcom/
exl030.
[30] M. Fitting, The logic of proofs, semantically, Annals
of Pure and Applied Logic 132 (2005) 1β25. doi:10.
1016/j.apal.2004.04.009.
[31] A. Mkrtychev, Models for the logic of proofs,
in: S. Adian, A. Nerode (Eds.), Logical Founda-
tions of Computer Science, 4th International Sym-
posium, LFCSβ97, Yaroslavl, Russia, July 6β12,
1997, Proceedings, volume 1234 of Lecture Notes
in Computer Science, Springer, 1997, pp. 266β275.
doi:10.1007/3-540-63045-7_27.
[32] S. N. Artemov, R. Kuznets, Logical omniscience
via proof complexity, in: Z. Γsik (Ed.), Com-
puter Science Logic, 20th International Workshop,
CSL 2006, 15th Annual Conference of the EACSL,
Szeged, Hungary, September 25β29, 2006, Proceed-
ings, volume 4207 of Lecture Notes in Computer Sci-
ence, Springer, 2006, pp. 135β149. doi:10.1007/
11874683_9.
[33] R. Moore, Reasoning About Knowledge and Action,
Technical Note 191, SRI International, 1980.
[34] G. Hughes, M. Cresswell, An Introduction to Modal
Logic, Methuen and Co., London, 1968.
[35] S. Kripke, Semantical considerations on modal
logic, Acta Philosophica Fennica 16 (1963) 83β94.
[36] B. F. Chellas, Modal Logic: An Introduction, Cam-
bridge University Press, Cambridge, 1980.
[37] R. Bull, K. Segerberg, Basic modal logic, in:
D. Gabbay, F. Guenther (Eds.), Handbook of Philo-
sophical Logic, Vol. II, D. Reidel Publishing Com-
pany, Dordrecht, 1984, pp. 1β88.
[38] Y. Liu, G. Lakemeyer, H. J. Levesque, A logic of
limited belief for reasoning with disjunctive infor-
mation, in: Proc. KR-04, Whistler, Canada, 2004,
pp. 587β597. URL: lll-kr2004.pdf.
[39] G. Lakemeyer, H. J. Levesque, A tractable, expres-
sive, and eventually complete first-order logic of
limited belief, in: Proceedings of the Twenty-Eighth
International Joint Conference on Artificial Intelli-
gence, IJCAI-19, International Joint Conferences on
Artificial Intelligence Organization, 2019, pp. 1764β
1771. URL: https://doi.org/10.24963/ijcai.2019/244.
doi:10.24963/ijcai.2019/244.
114
οΏ½