Re: Grounding puzzle

I'll answer my own question....

   We also need to strengthen the process description to make it clear
   that the Ashcroft service didn't change the person's phone number and
   then send you the new number.

All we need is the pseudo-connective (when p e), used by the
AI-planning community to mean "If p is true before the action, effect
e is imposed after."  I'll make up a nice infix notation: p |-> e.

Then we revise the ':effect' filed as shown here:

   (define_process call_ashcrofts_friendly_db
                   :inputs (ssn: US_Social_Security_number)
		   :outputs (pn: US_phone_number)
      :definition
         (send dest <= ashcrofts_pn_port
	       message <= ssn
	       response => pn)
      :effect (forall (p: Person pn: US_phone_number)
                    person_has_SSN(p, ssn(v @))
		     & person_has_phone(p, pn)
		    |->
		    pn = pn(^ @)
		     & i_know(person_has_phone(p, pn(^ @)))))

Is that elegant or what?  

   -- 
						-- Drew McDermott
						   Yale Computer Science Department