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 09:21:57 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24814; Thu, 9 Sep 93 01:09:56 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from arbi.Informatik.Uni-Oldenburg.DE by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA24810; Thu, 9 Sep 93 01:09:51 -0700 Received: by arbi.informatik.uni-oldenburg.de (smail3.1.18 + xalias); Thu, 9 Sep 93 10:08 CES Received: by aragorn.Informatik.Uni-Oldenburg.DE (Smail3.1.22.1) id ; Thu, 9 Sep 93 10:02 CES Received: from murphy.theorie by theoretica (4.1/SMI-4.1) id AA16457; Thu, 9 Sep 93 10:02:12 +0200 From: Juergen Bohn Message-Id: <9309090802.AA16457@theoretica> Subject: Re: a little proof challenge To: borm@cs.ubc.ca Date: Thu, 9 Sep 1993 10:02:08 +0200 (MET DST) Cc: info-hol@cs.uidaho.edu X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 2641 Perhaps you are interested in results from other theorem provers. In LAMBDA (classical higher order logic) I have proved your goal in ten or twelve minutes without any idea who it works at the beginning. In LAMBDA it is not necessary to quantify over P,Q,R and x, but quantification would be equivalent. The script and output of the system are appended. I am really interested in a HOL prove of this goal to compare it with the effort in LAMBDA. Juergen -- Juergen Bohn | Phone : ++49-441-798-3122 FB10 theoretische Informatik | FAX : ++49-441-798-2155 Universitaet Oldenburg | EMail : Juergen.Bohn@ Postfach 2503 | Informatik.Uni-Oldenburg.DE D-26111 Oldenburg | or : uniol!Juergen.Bohn -- val rew = rewriteTac; fun instAllLTac str = chooseAllLTac (topPenv()) [str]; fun instExRTac str = chooseExRTac (topPenv()) [str]; pushGoal libPenv "G // H |- exists v,w,y,z. (P x /\\ Q y) ->> ((P v \\/ R w) /\\ (R z ->> Q v))"; ******* LEVEL 1 ******* 1: G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) ---------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) > at (rew allScopeRules); ******* LEVEL 2 ******* 1: G // H |- P x /\ (forall x. Q x) ->> exists x1. (P x1 \/ (exists x. R x)) /\ ((forall x. R x) ->> Q x1) ------------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) > apprl impR; ******* LEVEL 3 ******* 1: G // P x /\ forall x. Q x $ H |- exists x1. (P x1 \/ (exists x. R x)) /\ ((forall x. R x) ->> Q x1) ---------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) > at ( (instExRTac "x") thenT (rew []) ); ******* LEVEL 4 ******* 1: G // P x /\ forall x. Q x $ H |- (forall x. R x) ->> Q x ---------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) > apprl and2L; ******* LEVEL 5 ******* 1: G // forall x. Q x $ H |- (forall x. R x) ->> Q x ---------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v) > at ( (instAllLTac "x") thenT (rew []) ); ******* LEVEL 6 ******* ---------------------------------------------------------------------- G // H |- exists v,w,y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)