gistfile1.txt

an expression with no metavars we'll call closed, and an expression w/
metavars is open

a substitution S is a for a set of metavars G is a total map from G (or any
superset of G) to closed expressions

given an open expression M with metavars in G (where G might have more than
just the ones in M), and a substitution S for G, [S]M is a closed expression

provability is a concept that applies to closed expressions, ie a closed
expression M is provable iff there is a proof tree for it

a goal is some structure composed of expressions. we extend open/closed to
goals in the obvious way.

a goal queue is a set of goals. we extend open/closed to goal queues in the
obvious way.

given an open goal M with metavars G, a substitution S for G satisfies M (ie
Sat(S,M)) just in case [S]M is provable

given an open goal queue Q with metavars G, a substitution S for G satisfies Q
(ie SatQueue(S,Q)) just in case Sat(S,M) for each M in Q

lemma:   if M in Q and SatQueue(S,Q) then Sat(S,M)

lemma:   if M in Q then { S | SatQueue(S,Q) } is a subset of { S | Sat(S,M) }

lemma:   { S | SatQueue(S, {M0,...,Mn}) }
         
         =
         
         { S | Sat(S,M0) }   ∩   ...   ∩   { S | Sat(S,Mn) }

  in english: the satisfiers of a queue of goals is the satisfiers that the
              goals have in common

lemma:   { S | SatQueue(S, {M0,...,Mn}) }
         
         =
         
         { S | Sat(S,Mi) }   ∩   {S | SatQueue(S, {M0,...,Mn} - {Mi}) }
  
  in english: the satisfiers of a queue are the satisfiers of any one goal in
              the queue, intersected with the satisfiers for the rest of the
              queue
  
  corollary: if we want to find the satisfiers of a queue, we can first find
             the satisfiers of an arbitrary goal in the queue, find the
             satisfiers of the remainder of the queue, then intersect them.