%%%% CP's comment:
%%%% This is a trial to make the evaluation process of scientific
%%%% papers more bidirectional. 
%%%% If you think that this is against some etiquette, inappropriate,
%%%% or against good manners, please let me know and I will stop it!!!

%%%% What follows is a 
%%%% complete Summary of an anonymous review
%%%% of a short version for TABLEAU 2002.
%%%% The Comments for the author of this
%%%% referee were very well justified and used
%%%% to improve the paper significantly.

Hilbert's Epsilon calculus `ought' to have relevance 
to automated theorem proving.  
An epsilon term is rather like a function 
producing an appropriate Skolem term,
but made an essential part of the language.  
The problem is, Hilbert thought proof-theoretically 
(at least he talked as if he did, in this area), 
and so a range of semantics is possible for epsilon terms.  
The author proposes making an epsilon term behave indefinitely 
--- as if it were ``an x such that...'' --- 
rather than functionally 
--- ``the x such that...''.  
This makes considerable sense, is explained well, 
and is related to the subject matter of this conference.