Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Path: utzoo!linus!philabs!mcnc!unc!ulysses!ucbvax!SU-SCORE.ARPA!PROLOG-REQUEST From: PROLOG-REQUEST@SU-SCORE.ARPA (Chuck Restivo, The Moderator) Newsgroups: net.lang.prolog Subject: PROLOG Digest V4 #21 Message-ID: <8606130712.AA26221@ucbvax.Berkeley.EDU> Date: Thu, 12-Jun-86 12:09:00 EDT Article-I.D.: ucbvax.8606130712.AA26221 Posted: Thu Jun 12 12:09:00 1986 Date-Received: Sun, 15-Jun-86 04:22:15 EDT Sender: daemon@ucbvax.BERKELEY.EDU Reply-To: PROLOG@SU-SCORE.ARPA Organization: University of California at Berkeley Lines: 194 PROLOG Digest Friday, 13 Jun 1986 Volume 4 : Issue 21 Today's Topics: Implementation - Assert & Truth Maintenance & DFID, & Behavior & Arithmetic ---------------------------------------------------------------------- Date: wed, 11 jun 86 09:29:27 pdt From: Tom Dietterich Subject: Assert, Assume, and Truth Maintenance genesereth and his students at stanford have a version of their mrs system (which is a logic programming system embedded in lisp) that contains both an assumption mechanism (called residue) and an assumption-based tms. it also contains a caching mechanism. strictly speaking, caching does not require making assumptions. but caching can interact with negation-as-failure whenever changes are made to the database. at oregon state, we have developed a forward-chaining logic programming system that we call forlog. it is based on dekleer's assumption-based truth maintenance system and so, by default, caches all inferences. it also supports the making and retracting of assumptions (of course), as well as true negation, true equality, and built-in temporal reasoning mechanisms. -- Tom Dietterich Department of Computer Science Oregon State University ------------------------------ Date: 11 Jun 86 02:29:29 GMT From: Thomas Sj|land Subject: Depth First Iterative Deepening in parallel Prologs I agree with earlier statements that DFPD is rather useless as an approach for or-parallel logic programming systems. It has one interesting point though: It is hard to think of an or-parallel scheme which has a simpler implementation than this one. The needed communication is minimal and the variable representation is optimal ( = Warren's for instance). The price you pay is reexecution. In all other schemes I have seen (in our lab there is work going on considering a handful (sic!)) there are considerable measures taken as to either reach a highly flexible variable representation (Haridi/Ciepielweski /Hausman proposes hashing etc.) or trying to avoid copying through more or less smart heuristics or even specialized hardware (Khayri/Fahlen/Karlsson). All of these schemes involve a considerable amount of communication, at least compared to DFPD. An implementation of a DFPD Horn Clause prover ("pure Prolog") could show useful in the sense that any proposed "smart" scheme has to be at least as good as the DFPD scheme (for at least some subclass of programs and queries) to be taken seriously. It is also interesting to notice that DFPD is complete, whereas most of the "smarter" schemes are not. ------------------------------ Date: 9 Jun 86 13:39:34 GMT From: Gilbert Cockton Subject: Standard behavior? In all humility, and with a strong chance of getting it all wrong here I go: var(X) = All t in Term: can_unify(t,X) where can_unify is true if a most general unifier can be found for both its arguments. nonvar(X) = Exists t in Term: NOT(can_unify(t,X)) Dirty structures like lists with uninstantiated tails (as in the unit time queue trick) are nonvar under these definitions. I've had minimal training in Logic, so I don't know if the set of all Terms is an ok construct. Seems ok to me. This leaves cut, which is definitely meta-logical. ------------------------------ Date: Thu 12 Jun 86 11:51:38-EDT From: Vijay Subject: Arithmetic without infinitely many symbols. As another illustration of how variables may be used to good effect, here is a set of routines that implement Presburger arithmetic (=, <, addition) for the integers by using a] a representation of numbers as structures built up using a unary function symbol and b] the idea of a difference list. For those of you who are unfamiliar with CP[!,|], here is a brief description of the annotations that may help you to udnerstand the program: --This is an AND-parallel and OR-parallel language: all clauses for all goals in the currrent resolvent are tried in parallel. --If a term is decorated with a '!' in the head of a clause, then unification of the head of the clause with a goal term suspends until the corresponding argument in the goal becomes (top-level) instantiated. --The definition of the !/2 annotation is more complex. Basically it works like a top-level ==. In this context, == is adequate, as explained below. /* This is a module that shows how Presburger arithmetic may be done in O(1) unifications, using a unary representation of numbers. We represent a number by a structure that has two component terms. Let the term s(s(...m times..(X)...) be denoted by s^m(X). The term s^m(X)-X represents the positive number m; the term X-X represents 0 and the term X-s^m(X) represents -m. Let |A| stand for the integer represented by the term A. Then: sgn(X,S) holds iff |X| is positive and S=p; sgn(X,S) holds iff |X| is negative and S=n; sgn(X,S) holds iff |X| is 0 and S=0. neg(A,B) holds iff |A|=-|B|, eq(A,B) holds iff |A|=|B|, <(A,B) holds iff |A| < |B|, add(A,B,C) holds iff |A|+|B|=|C|, sub(A,B,C) holds iff |A|-|B|=|C|. All these operations can be done in 1 unification. (The definition of sub/3 and