CSCE 420 Lecture 25

« previous | Thursday, April 18, 2013 | next »

Situation Calculus

similar to event calculus in that it encodes something that changes in the world

Has to do with actions and their effects.

Knowledge-Based Agents: ${\text{state}}\wedge {\text{goals}}\wedge KB\models {\text{do}}(a_{i})\quad a_{i}\in {\text{Actions}}$

Suppose we have block-world problem:

[B][A]

[C]

Claw: empty

Next state:

[B]

[C]

Claw: [A]

Next state:

[B]

[C][A]

Claw:

Encoding in FOL:

Initial State:
    on(A,B)
    on(B,table)
    on(C,table)
    clear(A)
    clear(C)
    claw_empty

    Goal: holding(A)

Later State:
    Goal: on(A,C)

Using Situation Calculus

1. add situation argument to each predicate: on(A,B,S₀), on(B,table,S₀), etc.
2. Use result function to denote successor states with "anonymous name" (instead of arbitrary numbers): S₁ = result(pickup(A,B), S₀)

	pre-conditions	effects
pickup(X,Y)	claw_empty, on(X,Y), clear(X)	¬claw_empty, holding(X), clear(Y)
puton(X,Y)	holding(X), clear(Y)	on(X,Y), claw_empty, ¬clear(Y), clear(X)

Situation Calculus Axioms (add to KB above):

Template: ∀s,…  preconditions hold in s → effects hold in successor state

pickup(x,y): ∀s,x,y claw_empty(s) ∧ on(x,y,s) ∧ clear(x,s) →
    ¬claw_empty(result(pickup(x,y), s)) ∧
    holding(x,result(pickup(x,y), s)) ∧
    clear(y, result(pickup(x,y), s))

puton(x,y): ∀s,x,y holding(x,s) ∧ clear(y,s) →
    on(x,y, result(puton(x,y), s)) ∧
    claw_empty(result(puton(x,y),s)) ∧
    ¬clear(y, result(puton(x,y), s)) ∧
    clear(x, result(puton(x,y), s))

Now we can query the KB:

$KB\models {\text{holding}}(A,\Gamma )$, where $\Gamma$ is a variable representing some state.

To prove, we use back-chaining:

• holding(A, Γ) unifies with consequent of axiom for pickup: θ = { x/A, Γ/result(pickup(A,y), s) }
• pop goal and push antecedents with substituted/unified vars: clear(A,s), claw_empty(s), on(A, y, s) (s and y are still unbound variables)
• unify on(A,y,s) with fact on(A,B,S₀) and remove from goal stack: θ += { y/B, s/S₀ }
• Substitute new unified variables on goal stack: clear(A, S₀), claw_empty(S₀)
• All remaining goals are facts.

The binding for $\Gamma$ is now result(pickup(A,B), S₀)

We could to a similar proof to show that Γ/result(puton(A,C), result(pickup(A,B), S₀)) is unification for the third state in our blocks-world example above:

• goal stack initially on(A,C,Γ)
• pop-unify-push with puton axiom:
  • unification: θ = { x₁/A, y₁/C, Γ/result(puton(A,C), β }
  • goal stack: holding(A,β), clear(C,β)
• pop-unify-push with pickup axiom:
  • unification diff: θ += { x₂/A, β/result(pickup(A,y₂), γ) }
  • goal stack: claw_empty(γ), clear(A,γ), on(A,y₂,γ), clear(C,β)
• pop-unify-push with facts claw_empty(S₀), clear(A, S₀), and on(A, B, S₀)
  • unification diff: θ += { γ/S₀, y₂/B }
  • goal stack: clear(C,β) = clear(C, result(pickup(A,B), S₀))
• pop-unify-push with frame axiom
• empty goal stack ∴ Q.E.D

Frame Problem

How do we prove that C remains clear after we perform an action on the initial state?

Have to encode everything that doesn't change in every axiom:

pickup(x,y): ∀s,x,y claw_empty(s) ∧ on(x,y,s) ∧ clear(x,s) →
    ¬claw_empty(result(pickup(x,y), s)) ∧
    holding(x,result(pickup(x,y), s)) ∧
    clear(y, result(pickup(x,y), s)) ∧
    ∀z (z ≠ x ∧ clear(z,s) → clear(z, result(pickup(x,y), s)))

Alternatively, we could write possibility axioms, effects axioms, and frame axioms:

possibility

∀s,x,y clear(x,s) ∧ claw_empty(s) ∧ on(x,y,s) → possible(pickup(x,y), s)

effects

∀s,x,y possible(pickup(x,y), s) → holding(x,result(pickup(x,y), s))

frame

∀s,x,y,z possible(pickup(x,y), s) ∧ z ≠ x ∧ clear(z, s) → clear(z, result(pickup(x,y), s))

This requires Actions × Effects axioms!

The trick for representational frame problem is:

∀s,x,a clear(x, result(a,s)) ↔
    (∃y a = pickup(y,x,s)) ∨ (∃y a = puton(x,y,s)) ∨
    (clear(x,s) ∧ a ≠ pickup(y,x,s) ∧ a ≠ puton(x,y,s))

"for any other action, if $x$ was previously clear, it stays clear."

Fun in Prolog

Prolog Implementation of Situation Calculus named GOLOG.