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; Thu, 2 Dec 1993 15:05:43 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14438; Thu, 2 Dec 1993 07:58:49 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.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 AA14434; Thu, 2 Dec 1993 07:58:46 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA09834; Thu, 2 Dec 93 06:55:53 -0800 Received: from ira.uka.de by iraun1.ira.uka.de id <13596-0@iraun1.ira.uka.de>; Thu, 2 Dec 1993 15:55:38 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <29599-0@i80fs2.ira.uka.de>; Thu, 2 Dec 1993 15:54:39 +0100 To: info-hol@cs.uidaho.edu Date: Thu, 2 Dec 1993 15:54:38 +0100 From: schneide Message-Id: <"i80fs2.ira.601:02.11.93.14.54.46"@ira.uka.de> Wishnu Prasetya asked: ||> Can FAUST solve the the following: ||> ||> "(!s:*. q s ==> r s) /\ ~r s /\ (!s. ~r s /\ ~q s ==> p t \/ q t) ||> ==> ||> p t \/ r t" Here is what I gave to HOL90: - set_goal ([],--`(!s:'a. q s ==> r s) /\ ~r s /\ (!s. ~r s /\ ~q s ==> p t \/ q t) = ==> p t \/ r t`--); (--`(!s. q s ==> r s) /\ ~(r s) /\ (!s. ~(r s) /\ ~(q s) ==> p t \/ q t) ==> p t \/ r t`--) ============================= val it = () : unit - e(FAUST_TAC); OK.. Goal proved. |- (!s. q s ==> r s) /\ ~(r s) /\ (!s. ~(r s) /\ ~(q s) ==> p t \/ q t) ==> p t \/ r t Top goal proved. val it = () : unit The runtime of the proof was 0.02 sec on a SPARC 10. ||> Does FAUST run for HOL 88? We had a version of FAUST also for HOL88, but as we decided to switch to HOL90, we removed the HOL88 version. -- Klaus