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:

Back to web page for Homework 2 web page for KR course