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; Sat, 17 Jul 1993 00:00:43 +0100 Received: by cs.uidaho.edu (16.6/2.0) id AA19196; Fri, 16 Jul 93 15:49:27 -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 AA19191; Fri, 16 Jul 93 15:49:23 -0700 Received: from scoobydoo.arc.nasa.gov by ptolemy.arc.nasa.gov (4.1/) id ; Fri, 16 Jul 93 15:53:12 PDT Date: Fri, 16 Jul 93 15:53:12 PDT From: Jim Alves-Foss-Summer 93 Message-Id: <9307162253.AA07765@ptolemy.arc.nasa.gov> Received: by scoobydoo.arc.nasa.gov (4.1/SMI-4.1) id AA02345; Fri, 16 Jul 93 15:49:25 PDT To: hall@itd.nrl.navy.mil Cc: info-hol@cs.uidaho.edu In-Reply-To: hall@itd.nrl.navy.mil's message of Fri, 16 Jul 93 18:38:52 EDT <9307162238.AA12075@qed> Subject: kgs of proofs?? > Why limit it to just HOL? Maybe having different divisions for different > provers would produce interesting results? A separate division for HOL, PVS, > Eves, maybe even Boyer-Moore? > > -- > Kelly Hall == hall@itd.nrl.navy.mil > no disclaimers, no cute quotes Don't forget the PAP prover (Paper-and-Pencil) ;-) -jimaf