Re: Shuffling syntax

Victor Yodaiken (
Thu, 27 Oct 1994 11:49:38 -0600

On Oct 27, 9:31am, Randall Holmes wrote:
Subject: Shuffling syntax
>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