[Termtools] Termination Competition: LP-Prolog and the Occurs Check

[Thomas Ströder]

Dear all,

termination of some of the examples in the LP-Prolog category depends on 
whether unification is performed with or without the occurs check. The 
ISO standard for Prolog leaves the behavior of Prolog implementations 
undefined in case of unifications where there is a different result if 
one is using the occurs check or not. Following the treatment of 
overflows in the Java categories, I have inserted a little section on
http://termination-portal.org/wiki/Logic_Programming
where it is said that in such cases both YES and NO answers (with 
consistent proofs) are valid.
If someone disagrees with this solution, please propose a different one 
and discuss it on this mailing list.

Best regards,
Thomas


-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241