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:00:26 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28491; Wed, 19 May 93 06:50:00 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28486; Wed, 19 May 93 06:49:54 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 19 May 1993 14:49:52 +0100 To: Tom Melham Cc: info-hol@ted.cs.uidaho.edu Subject: Re: First-Order Reasoning and HOL In-Reply-To: Your message of Wed, 19 May 93 14:08:08 +0100. <"swan.cl.cam.:115350:930519130826"@cl.cam.ac.uk> Date: Wed, 19 May 93 14:49:48 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:125300:930519134957"@cl.cam.ac.uk> > Well, for a start someone could program up Isabelle's fast_tac (and > related tactics) in HOL. fast_tac uses logical variables and unification to "guess" quantifier instantiations. A HOL tactic would have to make such instantiations explicitly. This becomes difficult in the presence of function symbols; the Agatha problem is unusual in having none. Larry Paulson