From owner-qed Thu Oct 27 10:33:18 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA25292 for qed-out; Thu, 27 Oct 1994 10:30:44 -0500 Received: from catseye.idbsu.edu (catseye.idbsu.edu [132.178.200.125]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA25287 for ; Thu, 27 Oct 1994 10:30:37 -0500 Message-Id: <199410271530.KAA25287@antares.mcs.anl.gov> Received: by catseye.idbsu.edu (1.38.193.4/16.2) id AA08703; Thu, 27 Oct 1994 09:31:21 -0600 Date: Thu, 27 Oct 1994 09:31:21 -0600 From: Randall Holmes To: qed@mcs.anl.gov Subject: Shuffling syntax Sender: owner-qed@mcs.anl.gov Precedence: bulk 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 strings. The opinions expressed | --Sincerely, above are not the "official" | M. Randall Holmes opinions of any person | Math. Dept., Boise State Univ. or institution. | holmes@math.idbsu.edu