%%%% 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.