Assumptions for STRIPS operators

Here is a brief outline of the assumptions used when writing operators using the STRIPS language.
Initial State: 1. conjunction of function free ground literals.
The literals could be negated, but the closed world assumption is used, so whatever is not explicitely stated is assumed to be false.
Goal: 1. conjunction of positive ground literals
Preconditions of operators: 1. conjunction of positive literals.
2. existentially quantified variables are allowed
Effects of operators: 1. conjunction of positive and negative literals.
The interpretation is that positive literals describe what is added to the world as an effect of the action and negative literals describe what is deleted from the world.

Extensions to STRIPS

Here is a brief outline of the extensions we allow to the STRIPS language. The original STRIPS assumptions are numbered, the extensions are indicated with a + sign. A short description is given of what is needed to handle the extensions.
Initial State: 1. conjunction of function free ground literals.
Goal: 1. conjunction of positive ground literals

+ conjunction of negative literals
This requires unification to match "p" and "not not p", It also requires goals with negative literals to be matched against the initial state. "not p" is satified in the initial state unless "p" is in the initial state.

+ disjunction of positive or negative literals
Adding disjunction is simple, it requires a non deterministic choice when selecting a goal.

+ variables are (implicitely) considered existentially quantified.

+ universally quantified variables are allowed
Universally quantified variables require assuming the world to be finite, static, and typed, so the quantification is satisfied by enumeration. All objects must be in the initial state and must have a type.
Example: forall(p) passenger(p) implies served (p)
Example: forall(o) object(o) implies at(o,Home)

Preconditions of operators: 1. conjunction of positive literals.
+ disjunction of positive literals.
A disjunction such as "p or q" requires a non deterministic choice. The same effect could be achieved less efficiently by writing two separate operators, one with "p" and one with "q" as precondition.
Example: part-of(p,w) or single(p)

2. existentially quantified variables are allowed

+ universally quantified variables allowed
Universally quantified variables require assuming the world to be finite, static, and typed, so the quantification is satisfied by enumeration. All objects must be in the initial state and have a type.
Example: forall(x) block(x) implies not on(x,b)
Example: forall(r) resource(r) implies committed(r,p) + existentially quantified variables allowed

Effects of operators: 1. conjunction of positive and negative literals.
We do not allow disjunction since this would introduce non determinism.

+ universally quantified variables allowed
Universally quantified variables require assuming the world to be finite, static, and typed, so the quantification is satisfied by enumeration. All objects must be in the initial state and must have a type.

+ conditional effects, where both the antecedent (or condition) and the consequent (or effect) are conjunctions of literals.
The antecedent refers to the world before the action is executed, the consequent refers to the world afther the action is executed. This requires resolving threats in a different way, using confrontation, and changing how subgoals are selected.
Example: at(car,city2) and not at(car,city1) when connected(car,engine)
Example: forall(p) passenger(p) implies served(p) when destination(p,f)