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; Tue, 24 May 1994 15:59:52 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03480; Tue, 24 May 1994 08:39:24 -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 AA03472; Tue, 24 May 1994 08:38:01 -0600 Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA01441; Tue, 24 May 1994 07:38:05 -0700 Received: by relay.cs.ruu.nl id AA10067 (5.67a/IDA-1.5 for info-hol@ted.cs.uidaho.edu); Tue, 24 May 1994 16:37:57 +0200 From: Wishnu Prasetya Message-Id: <199405241437.AA10067@relay.cs.ruu.nl> Subject: Class of automatic verifiable formulas To: info-hol@cs.uidaho.edu (hol mailing list) Date: Tue, 24 May 1994 16:37:57 +0200 (METDST) X-Mailer: ELM [version 2.4 PL23] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 400 Hi, I have a short, and probably dumb question: 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? Thanks for your help. Wishnu