[m-dev.] Re: Assocative predicates
fjh at cs.mu.OZ.AU
Sat Apr 18 03:38:46 AEST 1998
On 17-Apr-1998, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
> >On 16-Apr-1998, Peter Schachte <pets at cs.mu.OZ.AU> wrote:
> >How about just `pragma assert(Goal)'?
> > :- pragma assert(all [A,B,C] (A+B)+C=A+(B+C)).
> > :- pragma assert(all [A,B,C,D,E,F,G,H] (
> > foo(A, B, C, D, E), foo(D, E, F, G, H) <=>
> > foo(A, B, F, D, E), foo(D, E, C, G, H))).
> I think there is some confusion here.
Yes, you're right.
> You want to express something
> some [ABs] (append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
> some [BCs] (append(As, BCs, ABCs), append(Bs, Cs, BCs))
> The existential quantification of the linking variable is very important
One question we need to answer is what should the default
quantification be for goals inside `pragma assert'?
Should variables be implicitly existentially quantified
or should they be implicitly universally quantified?
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 184.108.40.206 | -- the last words of T. S. Garp.
More information about the developers