Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 15:35:58 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24956;
          Thu, 9 Sep 93 07:25:42 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from alpha.ora.on.ca by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA24952; Thu, 9 Sep 93 07:25:35 -0700
Received: by alpha.ora.on.ca (4.1/SMI-4.1) id AA24883;
          Thu, 9 Sep 93 10:18:13 EDT
Date: Thu, 9 Sep 93 10:18:13 EDT
From: mark@ora.on.ca (Mark Saaltink)
Message-Id: <9309091418.AA24883@alpha.ora.on.ca>
To: info-hol@cs.uidaho.edu
Cc: borm@cs.ubcca
Subject: Re: a little proof challenge


I transcribed the challenge into first-order untyped set theory and
proved it using EVES.  (Thus the predicates P Q and R are translated
into sets).  The proof was not completely automatic, but it took only
four prover commands.  The total elapsed time was under two minutes.

In the transcript below, my input consisted of the S-expressions
following the ">" prompts.

> (try (all (P Q R x)
         (some (v w)
	   (all (y z)
	     (implies (and (in x P) (in y Q))
		      (and (or (in v P) (in w R))
			   (implies (in z R) (in v Q))))))))


Beginning proof of ...
(ALL (P Q R X)
     (SOME (V W)
           (ALL (Y Z)
                (IMPLIES (AND (IN X P)
                              (IN Y Q))
                         (AND (OR (IN V P)
                                  (IN W R))
                              (IMPLIES (IN Z R)
                                       (IN V Q)))))))
> (open)


Opening the formula results in ...
(SOME (V W)
      (ALL (Y Z)
           (IMPLIES (AND (IN X P)
                         (IN Y Q))
                    (AND (OR (IN V P)
                             (IN W R))
                         (IMPLIES (IN Z R)
                                  (IN V Q))))))
> (reduce)


Which simplifies
forward chaining using ELEM-TYPE-P.TYPE-P
with the assumptions ELEM-TYPE-P.CHAR, ELEM-TYPE-P.INT, TYPE-P.BOOL
with the instantiation (= Z W) to ...
(IMPLIES (AND (IN X P)
              (SOME (Y) (IN Y Q)))
         (SOME (V)
               (IF (IN V P)
                   (IMPLIES (SOME (Z) (IN Z R))
                            (IN V Q))
                   (AND (SOME (W) (IN W R))
                        (IN V Q)))))
> (instantiate (v x))


Instantiating (= V X)

gives ...
(IMPLIES (AND (IN X P)
              (SOME (Y) (IN Y Q))
              (NOT (IF (IN X P)
                       (IMPLIES (SOME (Z) (IN Z R))
                                (IN X Q))
                       (AND (SOME (W) (IN W R))
                            (IN X Q)))))
         (SOME (V)
               (IF (IN V P)
                   (IMPLIES (SOME (Z$0) (IN Z$0 R))
                            (IN V Q))
                   (AND (SOME (W$0) (IN W$0 R))
                        (IN V Q)))))
> (simplify)


Which simplifies
forward chaining using ELEM-TYPE-P.TYPE-P
with the assumptions ELEM-TYPE-P.CHAR, ELEM-TYPE-P.INT, TYPE-P.BOOL to ...
(TRUE)


Mark Saaltink, ORA Canada. (mark@ora.on.ca)