Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!linus!philabs!cmcl2!seismo!caip!princeton!allegra!ulysses!burl!clyde!watmath!watnot!watdragon!rggoebel
From: rggoebel@watdragon.UUCP (Randy Goebel LPAIG)
Newsgroups: net.lang.prolog
Subject: Re: Standard behavior?
Message-ID: <1053@watdragon.UUCP>
Date: Mon, 2-Jun-86 11:55:41 EDT
Article-I.D.: watdrago.1053
Posted: Mon Jun  2 11:55:41 1986
Date-Received: Wed, 4-Jun-86 07:16:23 EDT
References: <980@watdragon.UUCP> <253@ubc-cs.UUCP> <1021@watdragon.UUCP> <1163@sicsten.UUCP>
Organization: U of Waterloo, Ontario
Lines: 17

> The reason why cut, var and nonvar cannot be "described logically" is that
> they are non-logical (or meta-logical, if you wish) primitives, that is
> primitives used to control the search for proofs.
> 
> The meaning of these primitives are dependent of the particular way an
> implementation looks for proofs. With a different implementation you
> could be forced to give a different meaning to cut, var and nonvar, or
> even find that they couldn't be given any meaning at all.
---------------
The standard implementation of Prolog provides a standard meaning for the
primitives described as non-logical.  These primitives have an interpretation
in a semantic domain that includes Prolog proofs (and partial proofs) as 
objects.  Such a formalization, if produced, would provide a standard 
specification for ``non-logical'' primitives of ordinary Prolog implementations.

I don't believe that anyone really believes that any Prolog primitive is
inherently unformalizable?