Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Roger Bishop Jones <rbj@win.icl.co.uk>
Date: Wed, 24 Nov 93 12:00:36 GMT
Message-Id: <9311241200.18843.0@norman.win.icl.co.uk>
To: info-hol@cs.uidaho.edu
Subject: little problem, solved by Otter

I don't have a record of the original posting but someone asked whether
the conjecture:

	(?!x. x = f ( g ( x))) <=> (?!x. x = g ( f( x)))
	
was automatically provable in HOL.
The only solution offered was a fairly complicated script from
David Shepherd and some doubt was expressed about whether FAUST would
be able to cope.

I have recently visited Argonne Labs, and while I was there I put the
problem to Bill McCune, and he got Otter to prove it.
(though I set the problem with the equations the other way round and
only just now remembered that the original wasn't that way)

Though the implication can be used to prove the equivalence easily
in HOL, the equivalence is much harder to prove (from scratch) than the
implication in Otter.
The implication took 66 seconds, to prove, the equivalence
took 4005 seconds (on a SPARK2 I think).

So it can be done automatically, if you are prepared to wait a while.

Roger Jones
International Computers Limited