Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Sat, 29 Aug 1992 02:22:46 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20029; Fri, 28 Aug 92 18:14:01 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from dewdrop.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) id AA20024; Fri, 28 Aug 92 18:13:55 -0700 Received: by dewdrop.cs.ucdavis.edu (5.57/UCD.CS.2.0) id AA01517; Fri, 28 Aug 92 18:12:34 -0700 Message-Id: <9208290112.AA01517@dewdrop.cs.ucdavis.edu> To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Isabelle In-Reply-To: Your message of Fri, 28 Aug 92 17:05:09 -0700 Date: Fri, 28 Aug 92 18:12:26 -0700 From: sara kalvala X-Mts: smtp > From: chou@cs.ucla.edu > > ... Anyway, I would be very interested in learning how (the > higher-order logic portion of) Isabelle compares with HOL. > Anyone has experience in both? Actually, this is the goal of a project starting this September at Cambridge. Here is a paragraph from the proposal: ----- HOL and Isabelle are based on many of the same principles. However, Isabelle also provides support for unification and embedded logics, and therefore could provide a better environment for large proofs than HOL. We propose to investigate whether this really is the case. We shall evaluate Isabelle on major hardware/system verifications. ----- Hopefully we can answer your question in detail later. I would like to know if anyone else has already attempted proofs in both and has any opinions at present. - Sara