A fully automatic problem solver with human-style output
  This paper describes a program that solves elementary mathematical problems,
mostly in metric space theory, and presents solutions that are hard to
distinguish from solutions that might be written by human mathematicians. The
program is part of a more general project, which we also discuss.
