Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 14 Jul 1994 21:17:02 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14280; Thu, 14 Jul 1994 14:11:18 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from ptolemy-fddi1.arc.nasa.gov by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA14276; Thu, 14 Jul 1994 14:11:17 -0600 Received: by ptolemy.arc.nasa.gov (4.1/) id for info-hol@leopard.cs.byu.edu; Thu, 14 Jul 94 13:05:19 PDT From: Jim Alves-Foss Message-Id: <9407142005.AA15058@ptolemy.arc.nasa.gov> Subject: Re: FM etiquette and accuracy To: vac@air16.larc.nasa.gov (Victor A. Carreno) Date: Thu, 14 Jul 1994 13:05:18 -0700 (PDT) Cc: info-hol@leopard.cs.byu.edu In-Reply-To: <9407141954.AA14524@air52.larc.nasa.gov> from "Victor A. Carreno" at Jul 14, 94 03:54:42 pm X-Mailer: ELM [version 2.4 PL23] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 796 > > Some people get rather annoyed, and with good reason, when you tell them you > are going to formalize their proof. Maybe mechanically check it is more > accurate. > > Victor. > > Unfortunately I have seen some "formal" proofs with statements such as: "From lemma n it is obvious/apparent/insert-your-favorite-word-here that x has P". In my mind this is NOT a formal statement and will NOT work in HOL. So if they get annoyed, let us hope it is with good reason. =============================================================================== -Jim Alves-Foss, Assistant Professor Computer Science Department voice: (208) 885-7232 University of Idaho fax : (208) 885-6645 Moscow, ID 83844-1010 email: jimaf@cs.uidaho.edu