[SCL] Re: implementing a nonstandard unifier

[Hans de Nivelle]

> 
> I would simply suggest to use a dummy predicate with a special meaning
> (e.g. holds) when you use non-constant relations. For example:
> 
>   transitive(u) <-> 
>   (!x)(!y)(!z)(holds(u,x,y) & holds(u,y,z) -> holds(u,z,x))
> 
> Of course in the logic holds will have a special semantics.
> 
> Any other syntax that comes to my mind would be quite confusing. Of
> course, it would be best to use a clearly visible name for this
> predicate, e.g. #holds.

Hello,

this is just the explicit application operator, as used in 
lambda-calculus, or higher order logic.

If you want to avoid using an explicit application operator, then
you would have to modify the datastructures. The application operator
would be still there, but hidden in the implementation.
(because you would have some kind of application record then).

Anyway, I agree with Andrei,

Hans.