Return-Path: 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 23:40:33 +0100 Received: by cs.uidaho.edu (16.6/2.0) id AA19188; Fri, 16 Jul 93 15:33:07 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from ptolemy-ethernet.arc.nasa.gov by cs.uidaho.edu (16.6/2.0) id AA19183; Fri, 16 Jul 93 15:33:00 -0700 Received: from scoobydoo.arc.nasa.gov by ptolemy.arc.nasa.gov (4.1/) id ; Fri, 16 Jul 93 15:36:27 PDT Date: Fri, 16 Jul 93 15:36:27 PDT From: Jim Alves-Foss-Summer 93 Message-Id: <9307162236.AA07141@ptolemy.arc.nasa.gov> Received: by scoobydoo.arc.nasa.gov (4.1/SMI-4.1) id AA02303; Fri, 16 Jul 93 15:32:36 PDT To: Tom.Melham@cl.cam.ac.uk Cc: windley@dbms1.cs.byu.edu, info-hol@cs.uidaho.edu, markaa@ultrastar.ee.cornell.edu In-Reply-To: Tom Melham's message of Fri, 16 Jul 93 20:02:32 +0100 <"swan.cl.cam.:026620:930716190242"@cl.cam.ac.uk> Subject: kgs of proofs?? > 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 I assume you've heard of the annual internet programming contest, where each team starts with a set of problems and e-mails in solutions which are judged and awarde points for correctness and speed. How about the first "International Internet Theorem Proving Contest", where the problems are proposed theorems, and the solutions are the HOL tactics. -Jim Alves-Foss, Assistant Professor Computer Science Department voice: (208) 885-7232 University of Idaho fax : (208) 885-6645 Moscow, ID 83844-1010 email: jimaf@cs.uidaho.edu