Specifying Theories in Situation Calculus

IndiGolog's high-level programs contain primitive actions and tests of predicates that are domain-dependent, and an interpreter for such programs must reason about these. We specify the required domain theories in the situation calculus, a language of predicate logic for representing dynamically changing worlds. In this language, a possible world history, which is simply a sequence of actions, is represented by a first order term called a situation. The constant So is used to denote the initial situation and the term do(a,s) denotes the situation resulting from action a being performed in situation s.

Relations that vary from situation to situation, called predicate fluents, are represented by predicate symbols that take a situation term as last argument; for example, Holding(o,s) might mean that the robot is holding object o in situation s. Similarly, functions whose value varies with the situation, functional fluents, are represented by function symbols that take a situation argument. The special predicate Poss(a,s) is used to represent the fact that primitive action a is executable in situation s. A domain of application will be specified by theory that includes the following types of axioms:

• Axioms describing the initial situation, So
• Action precondition axioms, one for each primitive action a, which characterizes Poss(a, s).
• Successor state axioms, one for each fluent F, which characterize the conditions under which F(x,do(a,s)) holds in terms of what holds in situation s; these axioms may be compiled from effects axioms, but provide a solution to the frame problem.
• Sensed fluent axioms, which relate the value returned by a sensing action to the fluent condition it senses in the environment.
• Unique names axioms for the primitive actions.
• Some foundational, domain independent axioms.

Domain Theories in IndiGolog


Here is how a domain theory can be specified in IndiGolog:

1. Declare predicate fluents:
   
   prim_fluent(<name of your fluent>).
   
   
2. Specify the initial situation (the values of some of your fluents):
   
   initially(<name of your fluent>,<initial value>).
   
   
3. Declare primitive actions:
   
   prim_action(<name of your action>).
   
   
4. Specify precondition axioms for your actions:
   
   poss(<name of your action>,<precondition>).
   
   Here the precondition can be quite complex and can include boolean operators neg, and, or and previously declared primitive fluents. If it is always possible to execute certain action, then the precondition is 'true'.
   
   
5. Define your actions:
   
   execute(<name of your action>,_) :- <some code>.
   
   Note that the code is just pure Prolog code.
   
   
6. Write successor state axioms that specify what fluents change after your primitive actions are executed, and how they change:
   
   causes_val(<action>,<fluent>,<new value>,<condition>).
   
   The above could be read as "the value of fluent <fluent> changes to the value <new value> after action <action> is executed and provided that the condition <condition> holds".
   
   If several fluents change their values after certain action is executed, you have to write several 'causes_val' statements. As always, if there is no condition, just write 'true'.