CSE 676, Fall 2001

THE FRAME PROBLEM

Last Update: 1 November 2001

Note: NEW material is highlighted

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:

NEW

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

But:

Can't show that:

or

still apply to the situation = result(p, lookup(q, Phonebook), s0)

So, need to revise (3) to:

(forall s,p,q,x,y)[at(q,y,s) ^ has(p,x,s)
                        ^ has(p, Phonebook, s) ^ listed(q, Phonebook, s)
                        ->
                        (lambda r)[at(q,y,r) ^ has(p,x,r)
                                        ^ phone#(q) = idea-of-phone#(p,q,r)](result(p, lookup(q, Phonebook), s))]


Copyright © 2001 by William J. Rapaport (rapaport@cse.buffalo.edu)
file: 676/F01/frameprob.01nv01.html