Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site sbcs.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!mit-eddie!genrad!panda!talcott!harvard!seismo!cmcl2!philabs!sbcs!debray
From: debray@sbcs.UUCP (Saumya Debray)
Newsgroups: net.lang.prolog
Subject: Re: Prolog: first order??
Message-ID: <377@sbcs.UUCP>
Date: Mon, 22-Jul-85 09:58:23 EDT
Article-I.D.: sbcs.377
Posted: Mon Jul 22 09:58:23 1985
Date-Received: Thu, 25-Jul-85 21:59:45 EDT
References: <174@bcsaic.UUCP> <697@water.UUCP> <315@cstvax.UUCP>
Organization: Computer Science Dept, SUNY@Stony Brook
Lines: 25

> There are people in our department who maintain that PROLOG is not first
> order *logic* since it relies on features like the ordering of clauses,
> and the ordering of goals within a clause.
> -- 
> 	Dave Berry. CS postgrad, Univ. of Edinburgh		

"Pure" Prolog has a well-defined semantics in terms of first order
logic (e.g. see [van Emden & Kowalski, JACM v.23 #4 1976], [Apt & van
Emden, JACM v.29 #3 1982]).  Relying on a specific clause order for
resolution, as Prolog does, loses completeness but not soundness,
i.e. at worst, Prolog may loop on a query although a refutation exists.
It turns out (as Apt & van Emden show in their proof of completeness
of SLD-resolution) that the order in which literals are selected
for resolution is irrelevant for completeness _as_long_as_ the clauses
to be resolved against can be chosen nondeterministically.

It is possible, however, to lose the logical semantics once "not" is
thrown in, unless you're careful about variables inside negations.
-- 
Saumya Debray
SUNY at Stony Brook

	uucp: {allegra, hocsd, philabs, ogcvax} !sbcs!debray
	arpa: debray%suny-sb.csnet@csnet-relay.arpa
	CSNet: debray@sbcs.csnet