===============================
May 1, 2012: formalization of Pat's conversation about blocksworld
The latest pass was written bty rww per discussions with Will and Jeremy
For clarity earlier comments by Will and Rww
  have been replaced by our current understanding.
Neither WIll nor Jermey have studied this latest version

We have two people me and bob (bob is describing to me what he did)
we abbreviate 'short term memory' with stm
we abbreviate 'long-term memory' with ltm
we abbreviate 'timestamp' with ts
we abbreviate 'problen solving context' with psc
the IN statement
 (in psc e) means psc contains a fact with expression e
   so
 if (in blocksworld (on A B)) in practice means
   if we look in the stm of the blocksworld we will find the triple (on A B)

====================================================================

  in stm of me

    ; general beliefs
    (isA bob agent) 
    (listening-to bob C1)
    (isA C1 conversation)

====================================================================
This utterance is not in Pat's dialog but agreed on by W and R
It sets the stage for the content of the conversation.
It orients 'me' wrt the meaning of 'On' 'A' and 'B' 
  which are mentioned later by 'bob'.

[U1] Let's discuss blocksworld

(hear me (say bob (that
  (lets-discuss blocksworld) 
)))

    =================================================
    ; speech art understanding
    (1st C1 U1)
    (isA U1 utterance) 
    (said-to U1 me) 
    (said-by U1 bob)
    (speech-act-type U1 suggest-discussion)
    (content-of U1 D1)
      ; in dialog/general knowledge
      ;  (subtype suggestion declarative-sentence)
      ;  (subtype declarative-sentencr otterance)
    (isA D1 suggestion)
    (object D1 discussion)
    (subject D1 blocksworld)
    -------------------------------------------------

new symbols introduced by bob 
     C1 - the ongoing conversation (isA C1 conversation)
     U1 - the first thing said (isA U1 utterance) 
     T1 - the 'time' U1 was said (isA T1 timestamp)) 
     D1 - content of the stuff uttered (isA W1 suggestion) 

    ; new beliefs of 'me' after hearing U1
    (talking-with bob C1)
    (talking-about C1 blocksworld)  
    (has-pcs bob blocksworld)

    in stm of bob
      (isA blocksworld psc)            
      in stm of blocksworld in bob
        nothing


====================================================================
[U2] I had a goal to get A on B.

(hear me (say bob (that
  (goal bob (in blocksworlds (on A B)))
)))

    =================================================
    ; speech art understanding

    (2nd C1 U2)
    (isA U2 utterance) 
    (said-to U2 me) 
    (said-by U2 bob)
    (speech-act-type U2 inform)
    (content-of U2 G2)
    (ts U2 T2)
    (before T0 T1) 

    (isA G1 goal-expression)
    (goal-agent G1 bob)
    (goal-desire G1 R1)
      (isA R1 relation)
      (relsym R1 in)
      (psc R1 blocksworld)
      (wff-of R1 F1)
      (isA F1 formula)   
      (relsyn F1 On)
      (arg1 F1 A)
      (arg2 F1 B)
    (ts G1 T2-1)  

    ; question[1]
    ;   is T2-1  when 'me' checks if (in blocksworld (on A B)) is true
    ;   or the time (in blocksworld (on A B) becomes true 
    ; this effects the partial order on the 'time's
    ;
    ; note[1]
    ; asserting (before T2-1 T2)
    ;     implicitly this says that I had the goal because
    ; since (not (in blocksworld (on A B)) at time T0
    ;   the answer to question[1] matters
    ;
    ;question[1]
    ; what is rhe relation between T1 and T2-1
    -------------------------------------------------
   
new symbols introduced by bob 
 U2 - the second thing said (isA U2 utterance) 
 T2 - the 'time' U2 was said (isA T2 time) 
 G1 - the goal statement made in U2 (isA G1 goal) 
 T2-1 - the 'time' when bob 'had' the goal

(in ?W ?e) means "?e can be found in the stm of ?w" (isA R1 ground-wff[me])
  this relation is part of general knowledge as soon as we reify agents/worlds
 R1 - (in blocksworld F1) 
 F1 - (on A B) (isA F1 awff) in the language of the blocksworld of bob

   in stm of bob
     (goal bob G1)
     (ts G1 T0)
     in stm of blocksworld in bob
       (isA A block)
       (isA B block) 
             
====================================================================
[U3] I expected that stacking A on B from the table
   would produce a state in which A was on B.

-------------------------------------------------
note [2]
Will's interpretation with of timestamps was

(hear me (say bob (that
"intention (stack A B) at time T1" and "expected [(on A B)
at time T2] at time T0" where T0 < T1 < T2

Rww has reworked the triples because it seemed to him that
the scope of the expectation included the the effect.
-------------------------------------------------

(hear me (say bob (that
  (expected bob
    (subtype do-action-get-effect)
    (action A1)
    (effect B1)
    (ts T3)
    (constraint C1)  
    (constraint C2) ) 
)))

    =================================================
    ; speech art understanding

    (3rd C1 U3)
    (isA U3 utterance) 
    (ts U3 T3)
    (said-by U3 bob)
    (said-to U3 me) 
    (speech-act-typetype U3 inform)
    (content-of U3 E1)

    (isA E1 expectation)
    (agent E1 bob)
    (type E1 do-action-get-effect)
    (action E1 A1)
    (effect E1 B1)

      (isA A1 action)
      (agent A1 bob)
      (psc A1 blocksworld)
      (lhs A1 L1)
        (isA lhs L1)
        (name L1 Stack)    
        (arg1 L1 A) 
        (arg2 L1 B)
      (isA T3-1 timestamp)
      (ts A1 T3-1)
        (isA T3-1 timestamp)

      (isA B1 belief) 
      (believer bob)
      (expr B1 W1)`
        (isA W1 awff)
        (relsym W1 in)
        (psc W1 blocksworld)
        (expr W2)
          (ISA W2 awff)
          (relsym W2 on)
          (arg1 W2 A)
          (arg2 W2 B) 
      (ts B1 T3-2)
        (isA T3-2 timestamp)

    (ts E1 T3-0)
      (isA T3-0 timestamp)
    (constraint E1 C1)
      (isA C1 constraint)
      (relsym C1 before)
      (arg1 C1 T3-0)
      (arg2 C1 T3-1) 
    (constraint E1 C2)
      (isA C2 constraint)
      (relsym C2 before)
      (arg1 C1 T3-1)
      (arg2 C1 T3-2) 
    -------------------------------------------------

    in stm of me

    ; new beliefs
    none       
      ; added to stm bob
        (expectation bob E1)
        ; in stm blocksworld
          nothing

-------------------------------------------------
note [2]
Rww: why isn't moving objects across stm's an action
     Bob is talking about changes in his mental state
       NOT changes in the world.

====================================================================

But one of the conditions of stacking A on B, that B
be clear, was not satisfied.

(hear me (say bob (that (and
   (in blocksworld (precondition A1 (clear B))
   (belief bob W5) ) )))

  in stm of me
   
   ; speech act info for U4
   ; a more interesting one
   ; 'me' gets a new belief
   ;   1. we 'resolved the action to the previously mentioned A1
   ;   2. we DO NOT have a name for the awff (clear B) so we
   ;      (reify me (awff W3 (
   ;        (relsym clear)
   ;        (arg1 B) ))) 
   ;      (reify me (beilef B2 (
   ;        (believer bob)
   ;        (expr W4) )))
   ;      (reify me (not-wff A4 (
   ;        (expr W5) ))) 
   ;      and 'resolving' W3 in W5!!!!! 
   ;      (reify me (awff W5 ( 
   ;        (relsym W5 in) 
   ;        (arg1 W5 blocksworld)
   ;        (expr W3) )))
   (precondition A1 W3)
     (isA W3 awff) 
     (relsym W3 clear)
     (arg1 W3 B)
   (belief bob B2)
     (isA B2 belief) 
     (believer B2 bob)
     (expr B2 W4)`
       (isA W4 not-wff)
       (expr W5)
         (isA W5 awff)
         (relsym W5 in)
         (psc W5 blocksworld)
         (expr W3)
     (ts B1 T4-0)
       (isA T4-0 timestamp)

This begs the question of the persistence of blocksworld
We accept the 'persistence' of bob BUT
timestamps seem to proliferats 'blocksworld's
are we diong belief addition or belief revision
ie do we forget eg ;contradictions 
are we saved by justifications 

====================================================================

Carrying out this action achieved
the associated goal.

(hear me (say bob (that (and
  (did A1)
  (achieved ) 

====================================================================

The action also produced a state in
  which, as expected, B was clear.

(hear me (say bob (that (and
  (did A1)
  (in blocksworld W?)

====================================================================

Thus, this state satisfied the goal
  of having B clear.

(hear me (say bob (that
  (satisfied (goal bob (in blocksworld (clear B))) )))

====================================================================

I expected that stacking A on B from the table would
produce a state in which A was on B.

  (hear me (say bob (that
    (expected me (in (do me W1 (stack A B)) (on A B)))
)))
         here we have the problem of what is an 'action'
         (stack A B) is unlikely to be an 'action/rule' for us
         as it does not articulate ALL the parameter.  Perhapss
         (expected me (in (do (stack me W1 A B)) (on A B))) )))
         here (in ?W ?E) means that
           ?E can be found in the belief structure of ?W
         note that 'do' is imagined to be descrictive SO
           (do (stack bob W1 A B)) (if doable) would
         result in changing
           the belief structure of W1 to contain the
           effects of stacking 
         and it would 'replace' the belief
           structure W1 in bob
           SO in the next utterance bob would still
           refer to this as W1
           in this sense we (temporarily) beg the
           issue of time.

============================

Thus, I created a goal to stack A on B from the table.

  (hear me (say bob (that
    (done (add-to me me (goal me (do (stack me W1 A B)))))
  )))

         This ugly collections of me is because 'add-to' is an action
         which requires both an agent and a world as a parameter

============================

But one of the conditions of stacking A on B, that B be
clear, was not satisfied.

  (hear me (say bob (that (and
     (precondition (do me W1 (stack A B)) (in W1 (clear B)))
     (not (in W1 (clear B))) ))))

          note (in W1 (clear B)) means that
            the expression (clear B) can be found
            in the belief structure of W1
            confusing logical 'satisfaction' with this seems wrong
              so I use 'in' instead of 'satisfy' for relations
            abduction could be used here
              to fill in bob's knowledge about actions in W1

============================

So I created a goal to have B clear.

  (hear me (say bob (that
    (done (add-to me me (goal me (do (clear me W1 B)))))
  )))

============================

I expected that unstacking C from B to the table would
produce a state in which B was clear.

  (hear me (say bob (that
    (expected me (in (do me W1 (unstack C B)) (clear B)))
  )))

============================

Thus, I created a goal to unstack C from B to the table.
  (hear me (say bob (that
    (done (add-to me me (goal me (in W1 (unstack C B))))
  )))

============================

The conditions for unstacking C from B were satisfied, so
I carried out this action.

  (hear me (say bob (that (and
     (all-in W1 (preconditions (unstack me W1 C B)))
     (done (unstack me W1 C B)) )
  )))

============================

Carrying out this action achieved the associated goal.

  (hear me (say bob (that
    (achieved 
       (doing (do (unstack me W1 C B))) 
       (goal me (in W1 (clear B))) )
  )))

============================

The action also produced a state in which, as expected, B
was clear.

  (hear me (say bob (that (and
    (satisfied (expected me (in (do (unstack me W1 C B)) (clear B))))
    (in W1 (clear B)) )
  )))

============================

Thus, this state satisfied the goal of having B clear.

  (hear me (say bob (that
    (satisfied (goal me (in W1 (clear B)))
  )))

The conditions was stacking A on B were satisfied, so I

============================

carried out this action.

  (hear me (say bob (that (and
     (all-satisfied W1 (preconditions (stack A B)))
      (done (stack me W1 A B)) )
  )))

==================

Carrying out this action achieved the associated goal.

  (hear me (say bob (that
    (satisfied (goal me (in W1 (on A B)))) )))

==================

The action also produced a state in which, as expected, A
was on B.

  (hear me (say bob (that
    (satisfied (expectation me (in W1 (on A B))))
    (in W1 (on A B)) )))


==================

Thus, this state satisfied the goal of having A on B,
which solved the original problem.

  (hear me (say bob (that (and
    (satisfied (goal me (in W1 (on A B))))
    (solved problem) ))))
       by abduction
       (do (solve-problem me me (on W1 A B)))


==================

This contains a litany
   Have expectation
   create goal
   try to satisfy goal
     this could be turned into a 'higher level' activity/action