Re: pure Prolog

I agree that the concepts are more important than the terms.
But this case (Horn Clauses vs. pure Prolog) and distinctions
seem interesting for two reasons:

1) Horn Clauses might (presumably by charter) form the basis of RIF Core.
On the other hand, pure Prolog might represent one concrete rule language
that we want RIF to cover.

2) This represents specific context where we may discuss issues of 
(non-)decidability, sound and complete inference procedures, ...

-Igor


Uschold, Michael F wrote:
> Michael Kifer has done a good job reflecting how the term 'Pure Prolog"
> is in use and suggested that because it is ambiguous, and that one of
> its definitions is snynnymous with Horn Clauses, that the latter term
> always be used when referring to Horn Clauses.
> 
> This is entirely sensible.
> 
> It is also useful to tease apart the technical issues that underly the
> different related notions.
> 
> Assuming there is no pressing need, per se, to define the term "Pure
> Prolog" and given it is ambiguous, perhaps it makes sense to just not
> use it in most technical discussions. The concepts are more important
> than the terms.
>
> Mike
> 
> -----Original Message-----
> From: Igor Mozetic [mailto:igor.mozetic@ijs.si] 
> Sent: Monday, April 10, 2006 4:19 AM
> To: Uli Sattler
> Cc: public-rif-wg@w3.org
> Subject: Re: pure Prolog
> 
> 
> Hi Uli (and the RIF list),
> 
> 
>>Am I right in assuming that SLD-resolution doesn't necessarily 
>>terminate (otherwise, Horn logic would be decidable, which it isn't?!)
> 
> 
> Yes, though I would attribute this to the language (Horn Clause, ie,
> definite programs), not to any specific procedure (it is true for all of
> them).
> 
> 
>>so, what kind is the "non-determinism" then? I am afraid "don't
> 
> know"? 
> 
>>Ie, depending on the order, it might or might not terminate  (yet, 
>>regardless of the order, it always gives the same answer, it it  gives
>>one):
> 
> 
> SLD is nondeterministic in the sense that it does not have to specify
> two choices:
> - goal selection or computation rule [LLoyd] - any fixed computation
> rule will do.
> - clause selection or search rule - it only has to be fair, so that each
> success branch is eventually found.
> 
> "Standard/pure" Prolog does specify the choices: it implements
> depth-first search rule (which is not fair) and can fall into an
> infinite branch.
> Then, there is a question of "occurs-check" in unification which might
> give rise (the lack of it) to unsoundness.
> 
> 
>>SLD-resolution is a sound and complete inference procedure which does 
>>not necessarily terminate. However, the resolution algorithm or 
>>SLD-refutation procedure is "don't know" non-deterministic and leaves 
>>open the order in which  atoms in the body are selected and the order 
>>in which clauses are tried.
> 
> 
> I would separate the issue of decidability (and halting problem) from
> the issues of Horn Clauses vs. pure Prolog.
> The first has to do with the choice of the language (Turing complete)
> while the second is the question of operational semantics and its actual
> execution model.
> 
> Regards,
> Igor
>

Received on Monday, 10 April 2006 16:38:41 UTC