Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 18 Jun 1993 01:57:23 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17121; Thu, 17 Jun 93 17:48:09 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from blackadder.CIS.McMaster.CA by ted.cs.uidaho.edu (16.6/1.34) id AA17116; Thu, 17 Jun 93 17:47:59 -0700 Received: from triose.eng.McMaster.CA by blackadder.cis.mcmaster.ca with SMTP id AA25716 (5.65c/IDA-1.4.4 for ); Thu, 17 Jun 1993 20:48:17 -0400 Received: by triose.eng.mcmaster.ca (4.0/SMI-4.0) id AA18915; Thu, 17 Jun 93 20:39:30 EDT Date: Thu, 17 Jun 93 20:39:30 EDT From: parnas@triose.eng.mcmaster.ca (David Parnas) Message-Id: <9306180039.AA18915@triose.eng.mcmaster.ca> To: John.Harrison@cl.cam.ac.uk, info-hol@ted.cs.uidaho.edu Subject: Re: Parnas: "some theorems we should prove" ONe of the reasons that I wrote the paper was to demonstrate that there is a need for automatic proof of pretty easy theorems. In my application, I need that much more than good support for "interesting" theorems. Prof. David Lorge Parnas Communications Research Laboratory Department of Electrical and Computer Engineering McMaster University, Hamilton, Ontario Canada L8S 4K1 Telephone: 416 525 9140 Ext. 7353 Telefax: 416 521 2922 Telephone at home: 416 648 5772 Telefax at home: 416 648 5943 email: parnas@triose.eng.mcmaster.ca