Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!princeton!caip!seismo!mcvax!enea!sicsten!lhe
From: lhe@sicsten.UUCP (Lars-Henrik Eriksson)
Newsgroups: net.lang.prolog
Subject: Re: Standard behavior?
Message-ID: <1162@sicsten.UUCP>
Date: Thu, 29-May-86 01:58:38 EDT
Article-I.D.: sicsten.1162
Posted: Thu May 29 01:58:38 1986
Date-Received: Sat, 31-May-86 06:40:12 EDT
References: <980@watdragon.UUCP>
Reply-To: lhe@sicsten.UUCP (Lars-Henrik Eriksson)
Organization: SICS, Sweden
Lines: 15

In article <980@watdragon.UUCP> rggoebel@watdragon.UUCP writes:
>...  The formulae assert that the
>individual constant named `[]' and everthing else (i.e., `_') is in the 
>class named by the predicate `a'.  If you believe that the anonymous variable
>is a universially quantified variable, then there are two resolution proofs
>of the query a([]).

There are indeed two resolution proofs of a([]), but as the two proofs produce
indentical bindings (in this case, none), it is not obvious that you'd want
two matches rather than one.

The problem gets worse if you give the query a(X). Again you have two
resolution proofs, but with different bindings. As one of the proofs subsumes
the other, you could argue for a single match in this case as well (with the
most general binding). I would prefer the single match in both cases.