Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!caip!think!mit-eddie!mit-amt!mob
From: mob@mit-amt.MIT.EDU (Mario O. Bourgoin)
Newsgroups: net.lang.prolog
Subject: Re: lemmas
Message-ID: <298@mit-amt.MIT.EDU>
Date: Sun, 17-Aug-86 13:30:38 EDT
Article-I.D.: mit-amt.298
Posted: Sun Aug 17 13:30:38 1986
Date-Received: Mon, 18-Aug-86 01:09:25 EDT
References: <292@mit-amt.MIT.EDU> <1311@lsuc.UUCP>
Organization: MIT Media Lab, Cambridge, MA
Lines: 50
Summary: I don't think we're talking abou the same thing

In article <1311@lsuc.UUCP>, dave@lsuc.UUCP writes:
> In article <292@mit-amt.MIT.EDU> mob@mit-amt.MIT.EDU writes:
> >
> >		If Prolog refused to solve for goals already encountered,
> >this problem would not exist. ...
> 
> I'd be interested in hearing the answer to this too. I believe this
> is what Kowalski describes as "lemmas" in Logic for Problem Solving -
> that is, whenever a goal is resolved (to either yes or no), that fact
> can be recorded.

I think that we aren't trying to solve the same problem. In  my  case,
if I solve for the goal  "goal(A)" which I  reduce to solving  for the
goal "goal(B)" then I  am no better  off, especially since Prolog will
then reduce the last goal to solving for "goal(C)".  I want Prolog  to
refuse to solve for "goal(B)" whether or not "goal(A)" has been solved
already.

What you  want appears to be  what  Suzanne Deitrich called "Extension
Tables" which is a form of dynamic programming. The problem of what is
current in the lemma hash table has been solved with what  is called a
Truth  Maintenance Systems  (TMS). In such  a system, an asserted fact
would  include both  it's  current   truth value (yes,   no) _and_   a
dependancy  record  of how  it  was deduced.  For  your  example,  the
deduction  that you are tired  today would be  removed from the  lemma
table when  the fact that  netnews was read for 180  minutes yesterday
would be removed.

A better solution is to have the asserted  lemmas keep track of _both_
a dependancy record of how it was deduced  _and_ the assumptions under
which it holds, in this case, yesterday's netnews reading time and the
rule used for goal  reduction. Prolog then keeps  track of which facts
are current as usual. These current facts form the context under which
deductions are made. When a goal is called, if it can  be found in the
lemma  table,  its  entry's   context is  checked  against the current
context and if it is  a subset of  the current context, the conclusion
reached earlier  can be used;   otherwise the goal   is resolved.  For
efficiency reasons, the context of deduction of  a fact is composed of
only those facts which the fact depends upon. This method is like what
Johann de Kleer proposed in Artificial  Intelligence, Vol.  28, No. 1.
1986.

Caveat: the above statements are a simplification of what would really
need to be done to make the algorythm work because they  doesn't  take
into account adding in  new rules or facts  under  which the deduction
could be made.

As is usual, we are trading off processing time for space.

--Mario O. Bourgoin