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