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, 13 Jul 1995 08:54:49 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA153220649; Thu, 13 Jul 1995 01:30:49 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from david.zfe.siemens.de by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA153190642; Thu, 13 Jul 1995 01:30:42 -0600 Received: from ztivax.zfe.siemens.de by david.zfe.siemens.de with SMTP id AA13848 (5.67a/IDA-1.5 for ); Thu, 13 Jul 1995 09:31:41 +0200 Received: from borel.zfe.siemens.de (borel) by ztivax.zfe.siemens.de with SMTP id AA08583 (5.67a/IDA-1.5 for ); Thu, 13 Jul 1995 09:31:41 +0200 Received: from juist.zfe.siemens.de (juist) by borel.zfe.siemens.de with SMTP id AA12865 (5.67a/IDA-1.5 for ); Thu, 13 Jul 1995 09:31:21 +0200 Date: Thu, 13 Jul 1995 09:31:21 +0200 From: Holger Busch Message-Id: <199507130731.AA12865@borel.zfe.siemens.de> To: info-hol@leopard.cs.byu.edu Subject: Re: Conditionals Phil Windley said: > This points out a larger question for the HOL community. I suspect > that PVS would solve this straight up. It certainly solved the last little > exercise we went through a few days ago straight away. These sorts of > niggling little proofs are just too hard in HOL. ... > HOL {and LAMBDA} is just to hard for the non-expert to use and its time > we did something about it. That's what led me to develop Rispe (reduced instruction set proof environment) in LAMBDA. It is not only intended for the non-expert, but also for the lazy expert who does not want to waste time on such basic problems, which Rispe solves fully automatically. At the same time all libraries of tactics, rules and LAMBDA proof functions are still accessible. To me there does not appear to be a contradiction between offering powerful and easy-to-use "catch all tactics" and keeping the architecture of HOL or LAMBDA open. Regards, Holger