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; Wed, 25 May 1994 04:12:23 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10046; Tue, 24 May 1994 21:03:35 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA10030; Tue, 24 May 1994 21:02:54 -0600 Received: from itd0.dsto.gov.au by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA03055; Tue, 24 May 1994 20:02:49 -0700 Received: from tcs22.dsto.gov.au by itd0.dsto.gov.au with SMTP (5.64+1.3.1+0.50/DSTO-1.0) id AA20275; Wed, 25 May 1994 12:32:01 +0930 Date: Wed, 25 May 1994 12:32:01 +0930 From: Jim Grundy Message-Id: <9405250302.AA20275@itd0.dsto.gov.au> To: info-hol@cs.uidaho.edu Subject: Re: Class of automatic verifiable formulas In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Tue, 24 May 1994 16:37:57 +0200 (METDST) > Is it true that the decideability of higher order formulas has not > been shown? If this is true, I suppose it means that no one has come > up with a program that can verify the truth of any arbitrary higher > order formula, right? And if above is wrong, then any HOL formula > should be automatically verifiable. am I right? I am pretty sure that this is the case; that is, that the decidability of HOL formulas has not been shown. In fact I would rather suspect that they have been shown to be undecidable. This of course means that nobody has a program that can verify arbitrary HOL formulae. But this does not mean that someone could not write a program that would do the job most of the time. Perhaps something with lots of AI. For example, I think higher-order unification is undecidable, but there are impementations out there that do a pretty good job of doing it most of the time. So, in some cases, there is no solution in theory, but in practice there is (almost) a solution. Likewise even if it were decidable, which I don't think it is, it might prove impossible to write a program with a reasonable time compexity. So, you can also have problems which while theoretically possible turn out to be intractable in practice. Jim Well thats my quite possibly very ignorant thoughts on the matter. I welcome correction (taken out of contect this sentence make me sound a more colourfull character than I am.)