THE FRAME PROBLEM

Formalization of: Looking up someone's phone #, dialing it, and having a conversation:

Premises:

1. has(p, Phonebook, s0)

2. listed(q, Phonebook, s0)

3. (forall s,p,q)[has(p, Phonebook, s) ^ listed(q, Phonebook, s)
                       ->
                       phone#(q) = idea-of-phone#(p, q, result(p, lookup(q, Phonebook), s))]

4. (forall s,p,q,x)[at(q, home(q), s) ^ has(p,x,s) ^ telephone(x)
                        ->
                        in-conversation(p, q, result(p, dial(phone#(q)), s))]

5. at(q, home(q), s0)

6. telephone(Telephone)

7. has(p, Telephone, s0)

Desired conclusion:

in-conversation(p, q, result(p, begin
                                                  lookup(q, Phonebook);
                                                  dial(idea-of-phone#(p,q))
                                              end,
                                              s0)))

But:

at(q, home(q))

has(p, Telephone)

So, need to revise (3) to: