Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from cs.uidaho.edu (actually ted.cs.uidaho.edu !OR! info-hol-request@cs.uidaho.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Fri, 16 Jul 1993 20:12:57 +0100
Received: by cs.uidaho.edu (16.6/2.0) id AA18565; Fri, 16 Jul 93 12:02:53 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by cs.uidaho.edu (16.6/2.0) id AA18560;
          Fri, 16 Jul 93 12:02:38 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 16 Jul 1993 20:02:37 +0100
To: Phil Windley <windley@dbms1.cs.byu.edu>
Cc: markaa@ultrastar.ee.cornell.edu, info-hol@cs.uidaho.edu, 
    Tom.Melham@cl.cam.ac.uk
Subject: Re: kgs of proofs??
In-Reply-To: Your message of "Wed, 14 Jul 93 09:44:29 MDT." <9307141544.AA24202@dbms1.cs.byu.edu>
Date: Fri, 16 Jul 93 20:02:32 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:026620:930716190242"@cl.cam.ac.uk>


windley@dbms1.cs.byu.edu says:

> I was thinking it would be fun if HOL kept a running tally of the number of
> primitive inference made (in a file somewhere) that could be consulted to
> see how many inferences had been made by a particular executable.
> 
> I was going to get a scoreboard for the lab and have contests.

Actually, the hard (and worthwhile) part is to *minimize* the number 
of inferences necessary to generate any particular theorem.  The old,
slow, version of rewriting, for example, used to do far too many 
useless inferences (rebuilding unchanged subtrees).  Perhaps a contest
to prove a fixed set of theorems with the fewest inferences...?

Tom