[net.lang.prolog] lemmas

dave@lsuc.UUCP (David Sherman) (08/13/86)

In article <292@mit-amt.MIT.EDU> mob@mit-amt.MIT.EDU (Mario O. Bourgoin) writes:
>
>		If Prolog refused to solve for goals already encountered,
>this problem would not exist. A hash table of  calls  would  provide  an
>efficient  solution  to  the  problem  of  whether  a state has been met
>already given a consistent  encoding  of  variable  names.  Can  someone
>provide me with a reason other than efficiency for why this is not done?

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 suppose it might be possible to program this into Prolog without
modifying Prolog itself - i.e., with predicates. Has anyone done this?
(It's of interest to me for the income tax analysis system I'm working on.)

One obvious problem that I can see is what to do with assert and
retract. For the lemma-system to be correct, it would have to be
able to figure out the implications of calls to assert and retract,
*including* how these affect predicates several calls away. For example:

	tired(today) :- toomuch(netnews, yesterday).
	toomuch(netnews, Day) :-
		read(netnews, Minutes, Day),
		Minutes > 120.
	read(netnews, 180, yesterday).

	?- tired(today).
	yes.

	retract(read(netnews, 180, yesterday)).

	?- tired(today).

If the implementation of retract has to search the entire database
and start making changes to what's been put into the lemma hash table,
the whole point of the system (improving efficiency) could be defeated.

Comments?

David Sherman
The Law Society of Upper Canada
Toronto
-- 
{ ihnp4!utzoo  seismo!mnetor  utzoo  hcr  decvax!utcsri  } !lsuc!dave

mob@mit-amt.MIT.EDU (Mario O. Bourgoin) (08/17/86)

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

raan@techunix.BITNET (Ran Ever-Hadani) (08/18/86)

Newsgroups: net.lang.prolog
Subject: Re: lemmas
References: <292@mit-amt.MIT.EDU> <1311@lsuc.UUCP>
Reply-To: raan@techunix.BITNET (Ran Ever-Hadani)
Organization: Technion CS Dept., Haifa, Israel

In article <1311@lsuc.UUCP> dave@lsuc.UUCP (David Sherman) writes:
>In article <292@mit-amt.MIT.EDU> mob@mit-amt.MIT.EDU (Mario O. Bourgoin) writes
:
>>
>>efficient  solution  to  the  problem  of  whether  a state has been met
>>already given a consistent  encoding  of  variable  names.  Can  someone
>>provide me with a reason other than efficiency for why this is not done?
>
>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.

It has been done - at least partialy.  Theory + experiments for Prolog
with assert and retract, esp. for very large databases of facts.  The
reference is:

Oded Shmueli, Hana Zfira, Ran Ever-Hadani
"Dynamic Rule Support In Prolog"
Fifth Generation Computer Architectures, J.V. Woods (ed.)
Elsevier Science Publishers B.V.(North-Holland)
IFIP, 1986

-- Ran Ever-Hadani,  raan@techunix.BITNET

raan@techunix.BITNET (Ran Ever-Hadani) (08/18/86)

Sorry, one name was omitted by mistake from the reference I posted -
That of Shalom Tsur of MCC.  Here is the right reference:

Oded Shmueli, Hana Zfira, Shalom Tzur, Ran Ever-Hadani
"Dynamic Rule Support in Prolog"
Fifth Generation Computer Architectures, J.V. Woods (ed.)
Elsevier Science Publishers B.V. (North-Holland)
IFIC, 1986

-- Ran Ever-Hadani
raan@techunix