Knowledge Representation: Homework 2 --- Sample Axioms
Axiomatizing Domains in Reiter-style Situation Calculus
Questions to leora@watson.ibm.com
The situation calculus was first introduced by John McCarthy
in the early 1960s, and popularized by McCarthy and Hayes
in their 1969 paper "Some Philosophical Problems from the
Standpoint of Artificial Intelligence." The essence of the
situation calculus has remained unchanged since then, although
its syntax has gone through a number of changes. More
importantly, researchers have recognized that formalizing
temporal domains entails formalizing different sorts of
facts. For example, any formalization must include some
causal rules, specifying how the world changes as actions
are performed; frame axioms, specifying the parts of the world
that don't change when actions are performed; and
feasibility axioms, specifying the preconditions that must
be satisfied in order for an action to be performed.
Although many researchers have contributed to this understanding,
the formalism introduced by Ray Reiter, of the
Cognitive Robotics
group at the University of Toronto, has become very popular
and widely used. This version of the situation calculus
is therefore used in the partial axiomatization below.
The basics of the syntax:
There are two distinguished predicates in
Reiter-style situation calculus:
--- Holds(s,fluent), understood to mean that
fluent is true in situation s
--- Poss(s,action), understood to mean that
action is feasible or possible in situation s
and one distinguished function:
--- result(s,action) which maps action and a
situation s into another situation, intuitively, the situation
which results from doing the action in the initial situation
s.
The trick in formalizing a temporal domain is to try to
fit any fact you want to write down into one of the following
categories. In each of the categories, I will give
as an example at least one of the axioms that are needed in Homework 2.
In all axioms,
all variables are assumed to be universally quantified unless
otherwise specified.
Categories of temporal axioms:
-
Background Information
(sometimes called boundary conditions or problem-specific facts):
These are the facts that are specific to the particular problem
at hand. General facts are not included here.
In Homework 2, the boundary conditions include the fact
that one socket has a burnt out bulb. This could be
represented as:
B 1:
Holds(S0,burnt-out(Bulb1))
B 2:
Holds(S0,in(Bulb1,Socket2))
-
Domain Constraints
(sometimes called state coherence axioms):
These facts specify how fluents relate at a particular
situation. For example, it is always the case that
a switch is on if and only if it is not off. Also,
there can never be more than one bulb in a socket at any
point. These facts can be represented as:
DC 1:
Holds(s, on(switch)) <==> ~Holds(s, off(switch))
DC 2:
Holds(s, in(bulb1,socket)) & ~(bulb1=bulb2) ==>
~Holds(s, in(bulb2,socket))
-
Feasibility Axioms:
These axioms specify the conditions under which it is possible
to do actions. For example, in order to turn on a switch,
it must be in the off position. This can be represented as:
FEAS 1:
Poss(s, turn-on(switch)) <==> Holds(s, off(switch))
-
Causal Axioms:
These axioms specify how the world changes after an action
is performed. For example, after one turns on a switch,
the switch is on. This can be represented as:
CAUSE 1:
Poss(s,turn-on(switch)) ==> Holds(result(s,turn-on(switch)),on(switch))
In English, this says: if it is possible to turn on a switch,
the in the situation resulting from the action of turning on
the switch, the switch is on.
-
Frame Axioms
(in this form, also known as explanation closure axioms):
These axioms specify how the world doesn't change
after an action is performed. For example, we might want to reason
that after a bulb burns out, a switch that was on in still on.
In general, it turns out to be easier to axiomatize this knowledge
by axiomatizing negative facts. We want to say that the only
way a light switch can change position is by turning a switch
on or off. Then, if we know that a bulb has burned out, we
know that the switch has not changed position. (Note that
such an inference will depend crucially on knowing all
events that have happened.) Such axioms are known as
explanation closure axioms because they give all possible explanations
for a fluent to change its truth value.
The explanation closure axiom that we need above can be represented
as:
FRAME 1: ~(act=turn-on(switch)) & ~(act=turn-off(switch))=>
Holds(result(s,act),on(switch)) <==> Holds(s,on(switch))
-
Unique Names Assumptions:
These axioms specify that differently named terms in fact
denote different entities. For example, the action of
turning on a switch is not the same as the action of removing
a light bulb. Such axioms are needed in inference in temporal
domains, in particular, for using explanation closure axioms.
Specifying unique names assumptions is arduous and time consuming,
since it requires an axiom for each pair of entities.
All unique names assumptions for actions are given below.
(You will still need to specify the unique names assumptions
for objects.) I am using the abbreviation ~= to denote not equals.
UNA1:
(insert(b,socket) ~= remove(b,socket)) & (insert(b,socket) ~= turn-on(switch))
& (insert(b,socket) ~= turn-off(switch)) & (insert(b,socket) ~= burn-out(b))
& (remove(b,socket) ~= turn-on(switch)) & (remove(b,socket) ~= turn-off(switch))
& (remove(b,socket) ~= burn-out(bulb)) & (turn-on(switch) ~= turn-off(switch))
& (turn-on(switch) ~= burn-out(bulb)) & (turn-off(switch) ~= burn-out(bulb))
UNA2:
((b1 ~= b2) v (socket1 ~= socket2)) ==>
(insert(b1,socket1) ~= insert(b2,socket2)) &
(remove(b1,socket1) ~= remove(b2,socket2))
UNA3:
b1 ~= b2 ==> burn-out(b1) ~= burn-out(b2)
UNA4:
sw1 ~= sw2 ==> (turn-on(sw1) ~= turn-on(sw2)) & (turn-off(sw1) ~= turn-off(sw2))
-
Domain Closure Assumptions:
These axioms specify that the objects mentioned are the
only ones there are. This can be useful when you must
infer that all objects of a certain sort do or do not
have a certain property. In this problem, we will want
to specify that there are no more than two bulbs,
two sockets, two switches. For example, to specify
that there are only two bulbs, we may write:
DCA 1:
(b = B1) v (b = B2)
(Recall that we are assuming universal quantification over
the variable b, which ranges over bulbs.)
Back to web page
for Homework 2
web page for KR course