Shuffling syntax

Randall Holmes (
Thu, 27 Oct 1994 09:31:21 -0600

It is important for those who design, maintain, and theorize about
theorem provers to be aware that they are ultimately shuffling syntax
(or even bit strings at the lowest level).

It should be the aim for the consumer to be entirely unaware of this
fact most of the time. The consumer should perceive that he is proving
theorems about mathematical objects, not that he is shuffling bit

The opinions expressed | --Sincerely,
above are not the "official" | M. Randall Holmes
opinions of any person | Math. Dept., Boise State Univ.
or institution. |