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; Thu, 17 Jun 1993 22:53:33 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16748; Thu, 17 Jun 93 14:44:53 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from qusunt.eng.McMaster.CA by ted.cs.uidaho.edu (16.6/1.34) id AA16743; Thu, 17 Jun 93 14:44:45 -0700 Received: by qusunt.eng.McMaster.CA id AA24996 (5.65c/IDA-1.4.4 for @qusunt.eng.McMaster.CA:info-hol@ted.cs.uidaho.edu); Thu, 17 Jun 1993 17:44:15 -0400 Date: Thu, 17 Jun 1993 17:44:15 -0400 From: David Parnas Message-Id: <199306172144.AA24996@qusunt.eng.McMaster.CA> To: info-hol@ted.cs.uidaho.edu, guttman@linus.mitre.org Subject: Re: Parnas: "some theorems we should prove" Cc: parnas@triose.eng.mcmaster.ca I would be curious to know what you mean by "formalizing" these theorems. The formula in the paper looked formal to me. Do you mean something more than changeing notation? We are of course looking for automatic proofs, not manually assisted proofs. How far are you from that? 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