  Many interesting and useful symbolic computation algorithms manipulate
mathematical expressions in mathematically meaningful ways. Although these
algorithms are commonplace in computer algebra systems, they can be
surprisingly difficult to specify in a formal logic since they involve an
interplay of syntax and semantics. In this paper we discuss several examples of
syntax-based mathematical algorithms, and we show how to specify them in a
formal logic with undefinedness, quotation, and evaluation.
