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; Mon, 14 Jun 1993 01:05:18 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08556; Sun, 13 Jun 93 16:54:03 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA08551; Sun, 13 Jun 93 16:53:58 -0700 Received: by grolsch.cs.ubc.ca id AA11968 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Sun, 13 Jun 1993 16:54:20 -0700 Date: 13 Jun 93 16:54 -0700 From: hug93 To: info-hol Message-Id: <110*hug93@cs.ubc.ca> Subject: RE: ` Parnas: "some theorems we should prove" John Rushby and Mandayam Srivas of SRI have investigated the use of PVS on the theorem-proving problems proposed by David Parnas (as mentioned in a previous posting to this mailing list). The results of their investigation are available in a write-up which can be obtained by anonymous ftp from ftp.csl.sri.com in /pub/reports/proofs-done.ps (postscript file). These theorems and the PVS investigation are very likely to be discussed in some manner at the HUG'93 meeting. It would be useful to hear a.s.a.p. about any other efforts (even on-going efforts) to guide us in planning the fine-details of the HUG'93 program.