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 13:56:39 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28440; Wed, 19 May 93 05:39:50 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA28435; Wed, 19 May 93 05:39:25 -0700 Message-Id: <9305191239.AA28435@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <22275-0@iraun1.ira.uka.de>; Wed, 19 May 1993 14:37:32 +0200 Date: Wed, 19 May 93 14:38:48 MET DST From: schneide To: info-hol@ted.cs.uidaho.edu Subject: First-Order Reasoning and HOL ===================== First-Order Reasoning ===================== It is not the point that the problem of aunt Agatha can be automatically solved or not (indeed, FAUST can also find an automatic proof for it, though the proof time is about 30 seconds). First the tactics I mentioned construct a proof without using mk_thm and second they can be used for interactive first-order reasoning within HOL. This allows to do the proof completely manually or on the other hand to simplify the goal such that the automated theorem prover can do the rest (there are a lot of challenge problems, e.g. Schubert's Steamroller problem or SAM's lemma which cannot be solved automatically by a lot of first-order provers, e.g. FAUST). =========================== Making HOL more comfortable =========================== I was surprised, that so many procedures for first-order reasoning exists and again I found out, that many higher-order theorem provers are more comfortable than HOL. For example, ISABELLE seems to me much more comfortable due to higher-order matching and first-order reasoning; Nuprl and Veritas both have dependent types, but HOL has nothing of the mentioned tactics. Is there a chance, that HOL can be extended to compare with those systems?