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, 19 Oct 1993 10:37:22 +0100 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA23074; Tue, 19 Oct 93 03:28:44 -0600 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.4/16.2) id AA23070; Tue, 19 Oct 93 03:28:41 -0600 Received: from sirius.brunel.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25531; Tue, 19 Oct 93 02:27:00 -0700 Received: from elektra.brunel.ac.uk by sirius.brunel.ac.uk with SMTP (PP) id <09893-0@sirius.brunel.ac.uk>; Tue, 19 Oct 1993 10:24:32 +0100 From: Simon Finn Received: from Delta.ahl.co.uk by Pinky.ahl.co.uk; Tue, 19 Oct 93 10:24:31 BST Date: Tue, 19 Oct 93 10:24:28 BST Message-Id: <191.9310190924@Delta.ahl.co.uk> To: info-hol@cs.uidaho.edu Subject: Re: how to get FAUST? > > (2) How fast FAUST can prove the following: > > > > "(?!x. x=f(g x)) = (?!y. y=g(f y))" > > It can't prove that as > i) that looks like a HOL88 term ... I think FAUST is only in hol90 > ii) in any case I don't think that FAUST will solve that goal. As an > experiment I tried it on it and after hol90 had increased heap > to 100Mb I interrupted it As I understand it, there's a more fundamental limitation. FAUST works with pure first-order logic, but for this proof you need first-order logic *with equality*. You can axiomatise equality inside first-order logic, so you could ask FAUST to prove something like --`(!v:'a. (v = v)) /\ (!v:'b. (v = v)) /\ (!(h:'a->'b) (v:'a) (w:'a). (v = w) ==> (h v = h w)) /\ (!(h:'b->'a) (v:'b) (w:'b). (v = w) ==> (h v = h w)) ==> (?x:'a. (x = f (g x)) /\ (!z:'a. (z = f (g z)) ==> (z = x))) = (?y:'b. (y = g (f y)) /\ (!z:'b. (z = g (f z)) ==> (z = y)))`-- but that is guaranteed to be horrendously inefficent. Simon Finn (Abstract Hardware Limited)