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; Wed, 19 May 1993 15:38:41 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28556; Wed, 19 May 93 07:29:16 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA28551; Wed, 19 May 93 07:29:07 -0700 Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <57677>; Wed, 19 May 1993 16:29:00 +0200 Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <57683>; Wed, 19 May 1993 16:24:20 +0200 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57709>; Wed, 19 May 1993 16:22:36 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8087>; Wed, 19 May 1993 16:22:29 +0200 From: Konrad Slind To: info-hol@ted.cs.uidaho.edu In-Reply-To: schneide's message of Wed, 19 May 1993 15:38:48 +0200 <9305191239.AA28435@ted.cs.uidaho.edu> Subject: First-Order Reasoning and HOL Message-Id: <93May19.162229met_dst.8087@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 19 May 1993 16:22:18 +0200 Klaus Schneider's last posting raises the question of how important pure first order reasoning is in HOL applications. I suspect that arithmetical and propositional reasoning are more important in verification. Is there a large body of existing proofs that can be shortened/automated with a first order predicate logic reasoner? Going further, it would be nice to know when a theory was especially suited for automated reasoning of some sort or other. Are there means of "matching" reasoners to higher-order logic theories? Konrad.