Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 18 May 1993 10:34:26 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26777;
          Tue, 18 May 93 02:19:42 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA26772;
          Tue, 18 May 93 02:19:29 -0700
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <57683>;
          Tue, 18 May 1993 11:19:16 +0200
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57677>;
          Tue, 18 May 1993 11:09:16 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8081>;
          Tue, 18 May 1993 11:08:51 +0200
From: Tobias.Nipkow@Informatik.TU-Muenchen.De
To: info-hol@ted.cs.uidaho.edu
Cc: Larry.Paulson@cl.cam.ac.uk
Subject: Higher-Order Reasoning
Message-Id: <93May18.110851met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 18 May 1993 11:08:38 +0200

P.S. I forgot to test Larry's implementation of a model-elimination proof
procedure due to Stickel (I think). I performs very well:

by (safe_meson_tac 1);

Level 1
lives(agatha) &
lives(butler) &
lives(charles) &
(killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &
(! x y. killed(x,y) --> hates(x,y) & ~ richer(x,y)) &
(! x. hates(agatha,x) --> ~ hates(charles,x)) &
(hates(agatha,agatha) & hates(agatha,charles)) &
(! x. lives(x) & ~ richer(x,agatha) --> hates(butler,x)) &
(! x. hates(agatha,x) --> hates(butler,x)) &
(! x. ~ hates(x,agatha) | ~ hates(x,butler) | ~ hates(x,charles)) -->
killed(agatha,agatha)
No subgoals!
val it = () : unit   
Timing  compile-0.1s (0.0s+0.0s+0.0s+0.0s+0.1s) run-3.1s

Tobias