Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!caip!nike!ucbcad!ucbvax!techunix.BITNET!raan
From: raan@techunix.BITNET (Ran Ever-Hadani)
Newsgroups: net.lang.prolog
Subject: Re: lemmas
Message-ID: <8608171142.AA04834@techunix.bitnet>
Date: Sun, 17-Aug-86 19:10:59 EDT
Article-I.D.: techunix.8608171142.AA04834
Posted: Sun Aug 17 19:10:59 1986
Date-Received: Mon, 18-Aug-86 04:33:08 EDT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: University of California at Berkeley
Lines: 30

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