🚀 go-pugleaf

>  In a more perspicuous description of Prolog-style Horn clause programming,
>I think it's a good idea to separate the constraint system from the
>resolution mechanism. Thus Prolog (in the simplified version here considered),
>whatever the constraint system used, delivers answers to a question A(x)
>of the form C(x,y), where C(x,y) is a conjunction of constraints, and
>it always holds that
>
>    (1)                     C(x,y) -> A(x)
>
>is a logical consequence of the program, read as a set of Horn clauses. Of
>course (1) does not imply that there is an x such that A(x); for this to
>follow, the constraint theory must be used.

This is a nice way of viewing things, but I don't know any Prolog that
gives you all of the constraints C.  Consider the following program:

	p(a) :- q(X,X).

	q(Y, f(Y)).

One the query p(X), Sicstus returns the following:

| ?- p(X).

X = a ? ;

no
| ?- q(X,X).

X = f(f(f(f(f(f(f(f(f(f(f(f(f(f ...
 
That is, sicstus only returns constraints related to variables appearing
the goal.  But the constraints that only have cyclic solutions may be
associated with other variables.

On a related issue, are there systems that permit user-specified
constraints, perhaps by means of some kind of escape system built
into the unifier?

Mark


Mark Johnson
Cognitive Science, Box 1978
Brown University