Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site lsuc.UUCP
Path: utzoo!lsuc!dave
From: dave@lsuc.UUCP (David Sherman)
Newsgroups: net.lang.prolog
Subject: lemmas
Message-ID: <1311@lsuc.UUCP>
Date: Wed, 13-Aug-86 08:45:36 EDT
Article-I.D.: lsuc.1311
Posted: Wed Aug 13 08:45:36 1986
Date-Received: Wed, 13-Aug-86 18:28:42 EDT
References: <292@mit-amt.MIT.EDU>
Reply-To: dave@lsuc.UUCP (David Sherman)
Organization: Law Society of Upper Canada, Toronto
Lines: 46

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