Difference between revisions of "Vol-3197/paper10"
Jump to navigation
Jump to search
(edited by wikiedit) |
(edited by wikiedit) |
||
| Line 9: | Line 9: | ||
|dblpUrl=https://dblp.org/rec/conf/nmr/Scherl22 | |dblpUrl=https://dblp.org/rec/conf/nmr/Scherl22 | ||
|wikidataid=Q117341818 | |wikidataid=Q117341818 | ||
| + | |description=scientific paper published in CEUR-WS Volume 3197 | ||
}} | }} | ||
==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== | ||
Latest revision as of 16:54, 30 March 2023
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
�