[FOM] Skolem functions

[Steve Stevenson]

When I took a course in automatic theorem proving many years ago, the 
instructor railed against Skolem functions for reason I have never 
understood. Now, while doing some work with intuitionistic tableaux, 
I find comments that Skolem functions are not allowable. Would 
someone explain this to me. Is this because they're magic functions 
of some sort?
-- 
best,
steve

Dr. D. E. Stevenson
Director, Institute for Modeling and Simulation Applications
Clemson University
Clemson,SC 29634-0974