Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Wed, 7 Dec 1994 21:52:34 +0000
Received: from localhost (listserv@localhost) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) id PAA25480 for qed-out;
          Wed, 7 Dec 1994 15:41:34 -0600
Received: from cli.com (cli.com [192.31.85.1]) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id PAA25475 
          for <qed@mcs.anl.gov>; Wed, 7 Dec 1994 15:41:29 -0600
Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1) id AA06589;
          Wed, 7 Dec 94 14:39:13 CST
From: boyer@CLI.COM (Robert S. Boyer)
Received: by rita (4.1) id AA03169; Wed, 7 Dec 94 14:39:09 CST
Date: Wed, 7 Dec 94 14:39:09 CST
Message-Id: <9412072039.AA03169@rita>
To: nqthm-users@CLI.COM, qed@mcs.anl.gov, theorem-provers@mc.lcs.mit.edu
Subject: Otter Web Page on Results
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


  http://www.mcs.anl.gov/home/mccune/ar/new_results/index.html

contains a summary of many of the cases in which Bill McCune's
automated reasoning system Otter, and other Argonne provers, have been
used to help settle open mathematical questions.  Quite remarkable.

I hope that those who make disparaging remarks about the prospects for
the automation of mathematical reasoning get pointed to that summary.

Bob