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 14:53:23 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14389; Thu, 2 Dec 1993 07:43:46 -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 AA14385; Thu, 2 Dec 1993 07:43:35 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA09823; Thu, 2 Dec 93 06:40:45 -0800 Received: from gate.fzi.de by iraun1.ira.uka.de id <12688-0@iraun1.ira.uka.de>; Thu, 2 Dec 1993 15:40:17 +0100 Received: from frodo.fzi.de by gate.fzi.de with SMTP (PP) id <13775-0@gate.fzi.de>; Thu, 2 Dec 1993 15:40:08 +0100 Received: from fzi.de by acid0s4.fzi.de id <11375-0@acid0s4.fzi.de>; Thu, 2 Dec 1993 15:39:57 +0100 To: info-hol@cs.uidaho.edu Subject: Re: can FAUST prove this? In-Reply-To: Mail from 'Wishnu Prasetya ' dated: Thu, 2 Dec 1993 14:47:33 +0100 (MET) Date: Thu, 2 Dec 1993 15:39:57 +0100 From: Dirk Eisenbiegler Message-Id: <"acid0s4.fz.070:02.11.93.14.40.01"@fzi.de> Hello, Faust does find the prove for your theorem. Just enter: set_goal ([], --` (!s:'a. q s ==> r s) /\ ~r s /\ (!s. ~r s /\ ~q s ==> p t \/ q t) ==> p t \/ r t `--); expand Faust.FAUST_TAC; Dirk -- ----------------------------------------------------------------- Dirk Eisenbiegler Tel.: +49 (721) 9654-420 Forschungszentrum Informatik (FZI) Fax: +49 (721) 9654-459 Haid-und-Neu-Str. 10-14 Email: eisen@fzi.de 76131 Karlsruhe -----------------------------------------------------------------