Re: PROLOG AND INFINITE TREES (Was: --- OLCOTT BANNED ---)

Hi,
Here you see SWI-Prolog deal with cyclic terms:
/* SWI-Prolog 9.3.2 */
?- X = [f,f|X], Y = [f|Y], X = Y.
X = Y, Y = [f|Y].
Clocksin & Mellish refer to the formal
definition of Unification in Resolution Theorem
proving, and not in Prolog. They write:
 > According to the formal definition of Unification,
 > this kind of "infinite term" should never come to exist.
 > Thus Prolog systems that allow a term to match an
 > uninstantiated subterm of itself do not act correctly
 > as Resolution theorem provers.
Thats from page 254 of this Clocksin and Mellish:
Programming in Prolog - Using the ISO Standard
Fifth Edition - See PDF page 268
Clocksin & Mellish - 2003
https://athena.ecs.csus.edu/~mei/logicp/Programming_in_Prolog.pdf
Bye
Mild Shock schrieb:

Hi,
 Pete Olcott is full of bullshit. He writes
nonsense like for example:
 "According to the formal definition of Unification, this
kind of “infinite term” should never come to exist"
https://philarchive.org/archive/OLCPDPv4
 Thats not true. There are different formal definitions
of Unification. There is Unification with and without
occurs check.
 There are algorithms that can make Unification without
occurs check terminate, and such an algorithm is
for example implemented in SWI-Prolog.
 They were pioneered by Alain Colmerauer himself, the
co-inventor of Prolog, who even wrote a paper about
the subject:
 PROLOG AND INFINITE TREES
Alain Colmerauer - 1982
Universite Aix-Marseille
https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf  Bye
 Mild Shock schrieb:

>
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.