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:44:10 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26785;
          Tue, 18 May 93 02:29:25 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26780;
          Tue, 18 May 93 02:29:17 -0700
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 18 May 1993 10:04:45 +0100
To: info-hol@ted.cs.uidaho.edu
Cc: Tobias.Nipkow@Informatik.TU-Muenchen.De
Subject: Higher-Order Reasoning (2)
Date: Tue, 18 May 93 10:04:33 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:119740:930518090501"@cl.cam.ac.uk>


Isabelle-HOL also implements the MESON proof procedure.  This only works for
the first-order fragment of HOL.  It proves the Aunt Agatha problem quickly:

goal HOL.thy "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)";

> 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!
Process time (incl GC): 6.8 secs

Again, runtime is for a SPARC ELC.  But safe_meson_tac does not work if the
original goal contains logical variables; it cannot tell us who killed agatha.

							Larry