## 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