Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 01:30:10 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24416; Wed, 8 Sep 93 17:15:54 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from grolsch.cs.ubc.ca by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA24412; Wed, 8 Sep 93 17:15:46 -0700 Received: by grolsch.cs.ubc.ca id AA10236 (5.65c/IDA-1.3.5 for info-hol@cs.uidaho.edu); Wed, 8 Sep 1993 17:15:36 -0700 Date: 8 Sep 93 17:15 -0700 From: Jeffrey Joyce To: info-hol@cs.uidaho.edu Message-Id: <7637*joyce@cs.ubc.ca> Subject: a little proof challenge One of my students, Eric Borm, has come up with the following theorem which has been nasty to other theorem-provers. If anyone is interested in trying to prove this theorem in HOL, we would be interested in the result -- in addition to the proof script, we'd be interested in some account of the amount of effort required to prove it. The proof script is likely to be very short -- it's more a matter of the effort required to find the script. A version of this theorem has been proven (with effort) using at least two other theorem-provers. I've translated the original statement of the theorem into h.o.l. as shown below by quantifying the predicates P Q and R and adding type annotations ... hopefully the following is indeed a theorem. "!P Q R. !x:*. ?v. ?w. !y. !z:**. ((P x /\ Q y) ==> ((P v \/ R w) /\ (R z ==> Q v)))" - JJJ ps. if you respond to this challenge, I would appreciate if you would respond directly to borm@cs.ubc.ca (as well as info-hol).