If we are to make QED a public resource, let's keep in mind recent
advances in distributed database technology (such as WWW and mosaic).
It would be really interesting to find WWW resources besides the
weather and the latest Dr. Fun Cartoon. (You can also find tangos, by
the way and some really beautiful, albeit risque' pictures of tango
dancers).
Javier
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id JAA19506 for qed-out; Wed, 14 Jun 1995 09:32:21 -0500
Received: from mcs.anl.gov (donner.mcs.anl.gov [140.221.5.134]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id JAA19499 for <qed>; Wed, 14 Jun 1995 09:32:12 -0500
Message-Id: <199506141432.JAA19499@antares.mcs.anl.gov>
To: qed
Subject: URI Support Program
Date: Wed, 14 Jun 1995 09:32:10 -0500
From: Rusty Lusk <lusk@mcs.anl.gov>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
I have been asked to post this to the list on behalf of ONR. Readers
may find it of interest.
- Rusty Lusk
------- Forwarded Message
-------------------------------------------------------------
The FY 95/96 URI Support Program (URISP), a Congressionally mandated
program for "have-not" institutions of higher education, has been
announced This will provide $2M grants over five years ($500K, $500K,
$500K, $300K, $200K) for work on any topic covered by our BAA. Each
eligible school can submit only one white paper (due 29 June) and one
proposal (due 29 September). It is anticipated that ONR will make
several $2M awards as a result of this announcement.
The announcement is available on internet via FEDIX, http://web.fie.com/.
-------------------------------------------------------------
MAY 1995
AFOSR BAA 95-4
I. INTRODUCTION
The Department of Defense (DoD) announces the University Research
Initiative Support Program (URISP). This program will be administered through
the Army Research Office (ARO), the Office of Naval Research (ONR), the Air
Force Office of Scientific Research (AFOSR), the Advanced Research Projects
Agency (ARPA) and the Ballistic Missile Defense Office (BMDO). URISP is
designed to help build the research infrastructure in the fields of science,
engineering, and mathematics that are important to DoD, at eligible
institutions through the use of competitive, multi-year grants. Eligible
institutions are those that have received a total of less than $2 million in
grant and contract awards from DoD over the previous two fiscal years. Non
eligible institutions are listed in Appendix E.
-------------------------------------------------------------
------- End of Forwarded Message
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id LAA09183 for qed-out; Mon, 19 Jun 1995 11:13:53 -0500
Received: from relay3.UU.NET (relay3.UU.NET [192.48.96.8]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id LAA09173 for <qed@mcs.anl.gov>; Mon, 19 Jun 1995 11:13:46 -0500
From: kerber@cs.uni-sb.de
Received: from uni-sb.de by relay3.UU.NET with SMTP
id QQyuuy14714; Mon, 19 Jun 1995 12:13:30 -0400
Organization: Universitaet des Saarlandes
D-66041 Saarbruecken, Germany
Received: from sbsvax with SMTP
by uni-sb.de (5.65++/UniSB-2.2/9502015)
id AA23275; Mon, 19 Jun 95 18:13:19 +0200
Received: from js-sfbsun.cs.uni-sb.de with SMTP
by cs.uni-sb.de (5.65/UniSB-2.3/950601)
id AA19139; Mon, 19 Jun 95 18:13:17 +0200
Received: from js-ss20.cs.uni-sb.de with SMTP
by js-sfbsun.cs.uni-sb.de (5.65b/UniSB-2.2/DFKI-1.0/061991)
id AA02658; Mon, 19 Jun 95 18:13:15 +0200
Message-Id: <9506191613.AA26851@js-ss20.cs.uni-sb.de>
Received: from js-ss20.cs.uni-sb.de with SMTP
by js-ss20.cs.uni-sb.de (5.65b/UniSB-1.0/DFKI-1.0/061991)
id AA26851; Mon, 19 Jun 95 18:13:15 +0200
To: qed@mcs.anl.gov
Cc: kerber@cs.uni-sb.de
Subject: QED-WS Integration of existing code
Date: Mon, 19 Jun 95 18:13:15 +0200
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
I would like to discuss two different points at the QED-Workshop II in Warsaw.
First, how is it possible to integrate existing verified code into the QED
approach? In order to answer this question it is necessary to discuss the status
of proofs in QED. My position is that the correctness of QED should guaranteed
by the *communication* of checkable proofs and that only such systems should be
integrated that deliver information which can be extended to full proofs. In
order to integrate the proofs from one system into the QED language, I propose
to employ a constructive meta-logic, in which provably correct transitions from
one formal system into another formal system can be encoded. By this it is
possible to show abstractly that theorems in an existing system can be used in
QED on the one hand, on the other hand the proofs can be constructed concretely
within QED.
Second, I'd like to discuss the question, why QED is needed in mathematics. One
point is that there have been false theorems in mathematics (compare Lakatos'
description of the development of Euler's polyhedron theorem). Another important
point is the striving for correctness at a level as high as possible in
mathematics, a system like QED is the answer of our time to that striving. (Many
good points to this discussion have already been made in this mailing list last
winter.)
Manfred Kerber
+------------------------------------------------------------+
| Manfred Kerber Tel.: (+49)-681-302-4628 |
| Fachbereich Informatik Fax.: (+49)-681-302-4421 |
| B. 36.1, R. 414 e-mail: kerber@cs.uni-sb.de |
| Universitaet des Saarlandes |
| D-66041 Saarbruecken |
| Germany |
| WWW: http://js-sfbsun.cs.uni-sb.de/pub/www/ |
+------------------------------------------------------------+
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id OAA27120 for qed-out; Thu, 10 Aug 1995 14:01:31 -0500
Received: from mcs.anl.gov (donner.mcs.anl.gov [140.221.5.134]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id OAA27094 for <qed>; Thu, 10 Aug 1995 14:01:16 -0500
Message-Id: <199508101901.OAA27094@antares.mcs.anl.gov>
To: qed
Subject: [Richard Waldinger: Re: about the proof of the CheckerBoard Problem]
Date: Thu, 10 Aug 1995 14:01:15 -0500
From: Rusty Lusk <lusk@mcs.anl.gov>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
mark stickel used a prpositional logic representation to prove the theorem
for 8x8 and some larger boards without using the color representation, just
using exhaustive search (a fast implementation of davis-putnam). the work is
reported in the recent paper of stickel and uribe. of course this bypasses
the point of mccarthy's challenge and doesnt establish the general case.
there is a recent paper by a student of boyer using the boyer moore theorem
prover to get the general result. the proof is interactive and uses the
coloring argument. it is the subject of a paper that has been submitted to a
recent journal, perhaps journal of symbolic systems (?).
maybe these were mentioned at QED2, i wasn't there---richard
(Actually from Richard, only posted by me - Rusty)
Received: from coral.cs.jcu.edu.au (geoff@coral.cs.jcu.edu.au [137.219.53.16]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id XAA06354 for <lusk@mcs.anl.gov>; Thu, 10 Aug 1995 23:33:31 -0500
Received: (from geoff@localhost) by coral.cs.jcu.edu.au (8.6.10/8.6.10) id OAA00457; Fri, 11 Aug 1995 14:33:25 +1000
From: Geoff Sutcliffe <geoff@cs.jcu.edu.au>
Message-Id: <199508110433.OAA00457@coral.cs.jcu.edu.au>
Subject: Re: about the proof of the CheckerBoard Problem
To: lusk@mcs.anl.gov (Rusty Lusk)
Date: Fri, 11 Aug 1995 14:33:23 +1000 (+1000)
Cc: qed@antares.mcs.anl.gov
In-Reply-To: <199508101901.OAA27094@antares.mcs.anl.gov> from "Rusty Lusk" at Aug 10, 95 02:01:15 pm
X-Mailer: ELM [version 2.4 PL23]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Hi,
> mark stickel used a prpositional logic representation to prove the theorem
> for 8x8 and some larger boards without using the color representation, just
> using exhaustive search (a fast implementation of davis-putnam). the work is
> reported in the recent paper of stickel and uribe.
If anyone would like to see and use Stickel's representation, it appears
as problems PUZ015-2 and PUZ016-2 of the forthcoming release of the
TPTP problem library. The release will be v1.2.0, and will be out soon.
The TPTP problem library can be accessed through the URLs:
http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
Cheers,
Geoff
Geoff Sutcliffe
Department of Computer Science Email : geoff@cs.jcu.edu.au
James Cook University Phone : +61 77 815085/814622
Townsville, Australia, 4811. FAX : +61 77 814029
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id XAA06530 for qed-out; Thu, 10 Aug 1995 23:54:52 -0500
Received: from coral.cs.jcu.edu.au (geoff@coral.cs.jcu.edu.au [137.219.53.16]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id XAA06525 for <qed@antares.mcs.anl.gov>; Thu, 10 Aug 1995 23:54:32 -0500
Received: (from geoff@localhost) by coral.cs.jcu.edu.au (8.6.10/8.6.10) id OAA00879 for qed@antares.mcs.anl.gov; Fri, 11 Aug 1995 14:54:27 +1000
From: Geoff Sutcliffe <geoff@cs.jcu.edu.au>
Message-Id: <199508110454.OAA00879@coral.cs.jcu.edu.au>
Subject: Re: about the proof of the CheckerBoard Problem (fwd)
To: qed@antares.mcs.anl.gov
Date: Fri, 11 Aug 1995 14:54:26 +1000 (+1000)
X-Mailer: ELM [version 2.4 PL23]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
Hi,
WRT ...
> The TPTP problem library can be accessed through the URLs:
> http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
> http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
Gustav Meglicki suggests ...
> What about an ftp location of the whole package?
1. Obtaining the TPTP by FTP
prompt> cd <the directory where you want the TPTP to reside>
prompt> ftp -i coral.cs.jcu.edu.au # or: ftp -i 137.219.17.4
# or use
ftp -i flop.informatik.tu-muenchen.de # or: ftp -i 131.159.8.35
Name (coral.cs.jcu.edu.au:<your login-name>): ftp
331 Guest login ok, send your complete e-mail address as password.
Password:<your full login-name>
ftp> cd pub/research/tptp-library # on coral.cs.jcu.edu.au
cd pub/tptp-library # on flop.informatik.tu-muenchen.de
ftp> binary
ftp> mget *.gz
ftp> quit
Or use the World Wide Web (WWW) with either of the following URLs :
http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
2. Installing the TPTP
prompt> gunzip -c TPTP-v1.2.0.tar.gz | tar xvf -
prompt> TPTP-v1.2.0/TPTP2X/tptp2X_install
<... the script will then ask for required information>
If you don't have any Prolog installed, you need to get one first. BinProlog
is freely available by anonymous ftp from clement.info.umoncton.ca:BinProlog
3. Converting all the TPTP problems to the syntax of other ATP systems
prompt> TPTP-v1.2.0/TPTP2X/tptp2X -f<Syntax>
where <Syntax> is one of kif, leantap, tap, meteor, mgtp, otter, pttp,
setheo, sprfn, or tptp.
The tptp option simply expands include directives, producing files in the
TPTP Prolog-style syntax. tptp2X offers MUCH more than this. See the TPTP
technical report for a detailed description of the utility, including
information on how to produce output in your own syntax.
Cheers,
Geoff
Geoff Sutcliffe
Department of Computer Science Email : geoff@cs.jcu.edu.au
James Cook University Phone : +61 77 815085/814622
Townsville, Australia, 4811. FAX : +61 77 814029
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id CAA05446 for qed-out; Tue, 15 Aug 1995 02:22:12 -0500
Received: from compu735.mathematik.hu-berlin.de (compu.mathematik.hu-berlin.de [141.20.18.102]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id CAA05441 for <qed@mcs.anl.gov>; Tue, 15 Aug 1995 02:22:05 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA05729; Tue, 15 Aug 1995 09:21:56 +0200
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA01639; Tue, 15 Aug 95 09:21:14 +0200
Date: Tue, 15 Aug 95 09:21:14 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9508150721.AA01639@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Re: Hierarchy of theorem provers
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
I don't think that QED will develop in a linear fashion. E. g. many useful and QED-related things can be done with theorem provers for typed languages and I don't understand why these should be forced to include Heavy Duty Set Theory.
QED should urge systems to become more cooperative so that e. g. theories, formulas, proofs are reusable (which only in the most optimistic case means 'translatable'). When this has been achieved, we may examine the graph of connections that has emerged and classify its nodes.
Certainly, systems that get their proofs passed through the most tough basic proof checkers will be especially honored. This will - among others - strengthen the path from Typed Theorem Provers through Heavy Duty Theorem Provers to Basic Theorem Provers.
Ingo Dahn
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA13151 for qed-out; Wed, 23 Aug 1995 06:44:57 -0500
Received: from compu735.mathematik.hu-berlin.de (compu.mathematik.hu-berlin.de [141.20.18.102]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id GAA13146 for <qed@mcs.anl.gov>; Wed, 23 Aug 1995 06:44:43 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA21400; Wed, 23 Aug 1995 09:06:42 +0200
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA20979; Wed, 23 Aug 95 09:05:57 +0200
Date: Wed, 23 Aug 95 09:05:57 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9508230705.AA20979@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: QED Framework
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
While the first QED workshop had put emphasis on the discussion of the
basic understandings of the QED project, the second also gave a survey on
existing expertise that can be used to bring QED into life. Moreover, there
seemed to be sufficient consensus among the participants of the Warsaw
workshop on goals that would be desirable to achieve in order to proceed.
Logically, the next step is to aim to concrete projects that push QED
forward. These will be based on the state of the art that has become
apparent in the 2nd QED workshop. It is widely agreed that QED is not a
monolithic system but gives room to a variety of cooperating approaches.
Therefore, I propose, that the QED community should actually use its
scientific authority in order to support projects that promise progress
towards the aims of QED. It is not important, that authors of such projects
believe in the feasilbilty of QED. It is not even necessary, that their
projects have computer aided mathematics as a principal goal. The only
point to make is, that these projects yield results that are useful for
QED.
To be more concrete, I propose to set up a description of topics and
problems where research is especially encouraged. The intended readers of
such a description are
- researchers looking for fields of application for their current work,
- researchers planning their future work or preparing proposals for
projects,
- staff of institutions that consider funding of related projects,
- referees of of related proposals and papers.
I would prefer, if this QED framework is not anonymous, but signed by many
competent contributors where at least some of them offer to the readers
further advice on request.
In order to launch a discussion I attach a list of topics that may be of
importance for QED. Most of them have been touched at the 2nd QED Workshop.
I am looking forward to comments to extend or modify this list. I expect to
mail a revised version in October.
Ingo Dahn
***************************************
* Bernd, Ingo Dahn *
* *
* Humboldt-University *
* Institute of Pure Mathematics *
* Ziegelstr. 13a *
* D-10099 Berlin *
* *
* Phone: (+49)30-2843-1829 *
* Fax : (+49)30-2843-1846 *
* Mail : dahn@mathematik.hu-berlin.de *
* *
***************************************
---------------------------------------------------------------------------
QED Framework V. 1.1 (8/23/95)
=============
Projects in (at least) the following topics are valuable for the QED
project and should be supported:
Proof Production
----------------
+ Automated theorem provers with special abilities.
The production of formal proofs can benefit considerably from the support
by automated theorem provers. While there are very refined universal
theorem provers, little is known about the technology of provers which take
advantage from domain specific properties, except for associativity and
commutativity. Other relevant fields could be set inclusions, finite sets,
finite and infinite sequences and number systems.
It is important, that the provers should be easy to combine with each other
and with automated and interactive general purpose provers. This requires a
welldefined input/output format, the possibility to accept limited
resources and support for the selection of well-suited problems.
+ Tools that support the generation of formalized proofs based on standard
mathematical texts.
A major problem for QED is the presentation of a large body of already
existing proofs in a format that can be verified. Actual mathematical texts
are mostly far from such a format. The tools should support the extraction
of the verifiable part of standard proof texts. Moreover, they should
supply their users with all available information that can be useful to
complete the extracted proof skeleton
+ Tools that support the generation and formalization of examples.
Examples play an important role in mathematics. Though most of them are not
used in proofs, they are very useful for mathematicians in order to
understand mathematical concepts. If the QED library is to be used by
mathematicians, it is desirable that it also contains a selection of
examples. Also the mathematical techniques to build new examples and to
derive their properties should be supported. Methods to represent
(infinite) models and to use them in automated and interactive proof search
need further investigations.
+ Tools that facilitate the tuning of automated theorem provers.
The fruitful application of most current automated theorem provers requires
solid knowledge of their specific logical calculi and methods of proof
search. This knowledge cannot be expected from a working mathematician.
Therefore, provers should tune themselve to adapt to the problems they are
supposed to solve. According to standard mathematical practice it can be
assumed that a prover will be faced with a large sequence of problems from
a specific domain. Alternatively, there may be mechanisms to detect a
change of domain and a necessity of re-tuning.
+ Projects that aim to formalize or verify specific parts of mathematics.
Such projects yield the basis to test QED tools. Thus they will give
valuable hints for further improvements. Moreover they give the basis to
present the achievements to potential users. In order to extend the QED
library as fast as possible, mathematical topics that have applications in
many other fields of mathematics should be preferred. To support reuse of
the results, the formalization should be in a precisely defined format
which is easy to parse.
Proof Checking
--------------
+ Proof checkers for specific systems
These check the correctness of proofs in a specific calculus. The
underlying calculus must be sound and should be complete with respect to a
mathematically defined semantics. The format of the proofs to be checked
must be precisely documented. If a proof is found to be incorrect or
incomplete appropriate informations should be returned in a standardized
format. The proof checking algorithm as well as its implementation have to
be available to the public in an extensively documented format. Their
correctness and completeness should be proved at least by standard
mathematical tools.
+ Generic proof checkers
These provide a language to specify proof concepts. Thus they can be used
to check the correctness of proofs in several calculi.The general remarks
made for proof checkers for specifiic systems also apply.
+ Proof translation between logical calculi
The aim is, to translate proofs in calculi without a proof checker into
proofs in a calculus where a proof checker is available. Since the success
of proof checking in the target calculus will guarantee the existence of a
correct proof, the demands to formal verification of the transformation
need not be as strict as for the proof checkers themselves.
Proof Administration and Exchange
---------------------------------
+ Tools for administring QED libraries
QED libraries will be large collections of formulas, definitions, theories
examples and proofs. They can be distributed worldwide. The contents of
these libraries has to be structured in an appropriate way. Besides the
usual technology known from bibliographical databases specific retrieval
tools will be helpful. These
should tolerate slight logical or linguistic variants of formulas or
theories. Search for incompletely specified formulas should be supprted. It
must be possible to generate entries into the library automatically. The
methods by which a theorem in the library has been verified will be
documented. The answers to search requests should be available in a format
that can be easily parsed as well as in a human readable format.
+ Tools for the transformation of proofs and theories
It will be necessary to bring together proofs and theories from different
sources and in different formats to make them available to different
systems. Moreover, human users with differing interests and knowledge will
use the QED libraries. Therefore, there is a need to adapt the material in
the libraries to special purposes (calculi, systems, readers).
Proof Presentation
------------------
+ Input/Output-Tools for mathematicians
It should be possible for mathematicians with little extra knowledge to use
and extend QED libraries. The interface language should be as close to the
usual language of mathematicians as possible. There will be support for
entering incomplete or partially verified proofs. The extent to which these
are verified will be documented automatically and there will be support for
the use of proof checkers.
+ Tools that integrate QED libraries into the existing world of
mathematical
education and research.
QED libraries should be made available to the mathematician at his desktop
and in libraries. There should be methods to refer in mathematical
publications to entries in QED libraries and vice versa.
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id JAA28046 for qed-out; Fri, 15 Sep 1995 09:36:10 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id JAA28041 for <qed@mcs.anl.gov>; Fri, 15 Sep 1995 09:36:02 -0500
Received: from dilbert.cli.com by cli.com (4.1/SMI-4.1)
id AA20543; Fri, 15 Sep 95 09:35:29 CDT
From: boyer@CLI.COM (Robert S. Boyer)
Received: by dilbert.cli.com (4.1) id AA13871; Fri, 15 Sep 95 09:35:29 CDT
Date: Fri, 15 Sep 95 09:35:29 CDT
Message-Id: <9509151435.AA13871@dilbert.cli.com>
To: qed@mcs.anl.gov
Subject: Announcing the Availability of More Nqthm-Checked Theorems
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
Below we describe how to obtain, install, and mechanically proof-check some
files containing Nqthm-checked theorems over and above those in the `examples'
directory distributed with Nqthm-1992.
These additional files include:
* Much of the `Clinc Stack'
a. The FM9001 microprocessor
(Brock & Hunt, with contributions from Kaufmann)
[fm9001-piton/fm9001-replay.events]
b. The Piton assembler (Moore)
[fm9001-piton/piton.events]
c. The `big-add' Piton example (Moore)
[fm9001-piton/big-add.events]
d. A Piton program that wins at Nim (Wilding)
[fm9001-piton/nim-piton.events]
* A Paris-Harrington Ramsey theorem (Kunen)
[kunen/paris-harrington.events]
* An illustration of the surprising power of EVAL$ (Kunen)
[kunen/induct.events] (surprising to Boyer and Moore anyway)
* The arithmetic-geometric mean theorem
(Kaufmann & Pecchiari)
[numbers/arithmetic-geometric-mean.events]
* The mutilated checkerboard theorem in the general NxN case
(Subramanian)
[subramanian/mutilated-checkerboard.events]
* A simple real-time system, the classic train example (Young)
[young/train.events]
* A theorem about coin tossing probabilities (Kaufmann)
[numbers/tossing.events]
* A proof of correctness of a real-time scheduling algorithm
(Wilding)
[numbers/scheduler.events]
Some documentation for some of the above proof efforts may be found as follows:
* FM9001 microprocessor http://www.cli.com/hardware/fm9001.html
* Piton assembler http://www.cli.com/reports/files/022.ps
* Nim playing program in Piton http://www.cli.com/reports/files/078.ps
* Paris-Harrington Ramsey http://www.cs.wisc.edu/~kunen/ramsey.ps
* EVAL$ http://www.cs.wisc.edu/~kunen/nqthm.ps
* Arithmetic-geometric mean http://www.cli.com/reports/files/100.ps
* Real time train http://www.cli.com/reports/files/093.ps
* Mutilated checker board
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/subramanian/mutilated-checkerboard.ps
* Real-time scheduling ftp://ftp.cli.com/home/wilding/scheduler-proof.ps
The source files for these theorems, named within square brackets above, may be
obtained individually from the directory
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/ or altogether in the single
file ftp://ftp.cli.com/pub/nqthm/nqthm-1992/1995-examples.tar.Z.
Also included on the tar file are new `driver' files for doing a replay of all
the examples under Nqthm-1992, both these new examples and those previously
distributed with Nqthm-1992. A Gnu Emacs TAGS file for all the event commands
in all the examples is also provided.
Supposing that one has obtained the file
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/1995-examples.tar.Z, and assuming that
Nqthm-1992 has been installed, and resides in the directory `nqthm-1992',
proceed as follows:
1. Move the file `1995-examples.tar.Z' to the `nqthm-1992' directory.
2. % cd nqthm-1992
3. % uncompress 1995-examples.tar.Z
4. % tar xvf 1995-examples.tar
5. % rm 1995-examples.tar (optional, to save space)
Assuming that Nqthm-1992 has been installed correctly, it should now be
possible to execute the following command, when connected to the `nqthm-1992'
directory, to have all the new event files proof-checked by Nqthm-1992. This
checking process will take many hours on a contemporary work station.
6. % make giant-test
On operating systems not Unix related, instead of the previous command one may
load the files `examples/driver.lisp' and `examples/driver-sk.lisp' to recheck
the theorems. See the file examples/README for further details.
Bob Boyer and J Moore
September 1995
P. S. This message may also be found as the file
examples/README-for-1995-examples on the tar file mentioned above.
P. P. S. For information on obtaining the Nqthm prover itself, please see
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/nqthm-1992.announcement
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id PAA10526 for qed-out; Mon, 25 Sep 1995 15:56:57 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id PAA10521 for <qed@mcs.anl.gov>; Mon, 25 Sep 1995 15:56:46 -0500
Received: from rana.cli.com by cli.com (4.1/SMI-4.1)
id AA12226; Mon, 25 Sep 95 15:56:15 CDT
From: moore@CLI.COM (J Strother Moore)
Received: by rana.cli.com (4.1) id AA03565; Mon, 25 Sep 95 15:56:12 CDT
Date: Mon, 25 Sep 95 15:56:12 CDT
Message-Id: <9509252056.AA03565@rana.cli.com>
To: qed@mcs.anl.gov
Subject: ACL2
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
ACL2 is a new theorem proving system produced at Computational Logic, Inc. The
acronym ``ACL2'' stands for ``A Computational Logic for Applicative Common
Lisp.'' ACL2 is similar to the Boyer-Moore theorem prover, Nqthm, and
Kaufmann's interactive extension, Pc-Nqthm. However, instead of supporting the
``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common Lisp.
Furthermore, ACL2 is programmed almost entirely within that language.
To obtain ACL2 by ftp, first connect to ftp.cli.com by anonymous login. Then
`cd' to ~acl2/v1-8, `get' the file `README' and follow the directions therein.
To obtain ACL2 by magnetic tape (for which service a fee shall be charged)
write to Software-Request, Computational Logic Inc., 1717 West Sixth, Suite
290, Austin, TX 78703-4776, USA; email: Software-Request@cli.com. FAX: +1
512 322 0656.
If you would like to join the unmoderated ACL2 mailing list, acl2@cli.com, send
to acl2-request@cli.com a message containing as its body (NOT its Subject) the
the single word `subscribe'. To get general information about the mailing
list, send the word `info' (this will not subscribe you to the mailing list).
To send a message to all who receive ACL2 mail, send the message to
acl2@cli.com. Finally, please report bugs in ACL2 to acl2-bugs@cli.com.
The ACL2 logic is a first-order logic of recursive functions providing
mathematical induction on the ordinals up to epsilon-0 and two extension
principles: one for recursive definition and one for constrained introduction
of new function symbols. First-order quantification is supported in a weak
sense using a ``choice'' operator.
The syntax of ACL2 is that of Common Lisp. Constants and macros may be defined
and used to extend the syntax.
The following primitive data types are axiomatized: rational numbers
(including, of course, integers and naturals), complex rationals, characters,
character strings, symbols (including packages), and conses. All primitive
Common Lisp functions on the above data types are (meant to be) defined in
ACL2. By ``Common Lisp function'' we mean any function described in ``Common
Lisp The Language,'' by Guy Steele (Digital Press, 30 North Avenue, Burlington,
MA 01803, 1984 and 1990), that is applicative, is not dependent on state,
implicit parameters or data types other than those listed above, and is
completely and unambiguously specified in a host-independent manner.
Approximately 170 such symbols are axiomatized.
To applicative Common Lisp ACL2 adds a single-threaded notion of ``state''
allowing the efficient provision of one and two dimensional arrays, property
lists, and file directed input and output within the applicative setting. In
addition, ACL2 adds notions of multi-valued function call and return and a
number of other useful primitives.
The ACL2 system allows the definition of new function symbols and the proofs of
theorems about those symbols. Like Nqthm, the behavior of the theorem proving
engine is determined by rules derived from previously introduced functions and
theorems. ACL2 provides many ``rule classes'' by which the user can specify
how a theorem is to affect the behavior of the theorem prover. ACL2 also
provides
* an interactive capability like that of Pc-Nqthm;
* more user control of proofs than Nqthm, via hints and scoping mechanisms;
* improved handling of propositional logic (including use of BDDs);
* a specification capability (``guards'') akin to types, but more flexible;
* proof techniques in addition to those of Nqthm, including forward chaining,
congruence-based rewriting, forced case-splits, and built-in clauses for
termination proofs;
* extensive hyper-linked on-line documentation available via ACL2 documentation
commands, HTML browsers and Emacs Info; and
* a ``proof-tree'' facility that makes it easy to explore failed proof
attempts.
ACL2 has seen heavy in-house use at Computational Logic, Inc., for
approximately 2 years. Several major projects have been carried out with it.
However, it has not received the extensive scrutiny that Nqthm has and bugs --
possibly even soundness bugs -- may crop up. Please report them to
acl2-bugs@cli.com, so that we can fix them and notify other users.
ACL2, including the source code, is available electronically without fee.
However, use of ACL2 signifies the user's agreement to abide by the terms of a
license agreement distributed as part of the system.
ACL2 currently works on the Unix (and some variants, including Linux) and
Macintosh operating systems. It is built on top of any of the following Common
Lisps: Allegro, GCL (Gnu Common Lisp) [or, AKCL], Lispworks, Lucid, and MCL
(Macintosh Common Lisp). We recommend running ACL2 with at least 16MB of
memory.
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id QAA03678 for qed-out; Wed, 27 Sep 1995 16:36:25 -0500
Received: from cerberus.ibmoto.com (cerberus.ibmoto.com [129.38.12.13]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id QAA03594 for <qed@mcs.anl.gov>; Wed, 27 Sep 1995 16:32:58 -0500
Received: from hangdog.ibmoto.com (raina@hangdog.ibmoto.com [129.38.10.13]) by cerberus.ibmoto.com (8.6.12/8.6.9) with ESMTP id QAA25806; Wed, 27 Sep 1995 16:20:39 -0500
Received: (raina@localhost) by hangdog.ibmoto.com (8.6.10/8.6.9) id QAA18374; Wed, 27 Sep 1995 16:20:37 -0500
Message-Id: <199509272120.QAA18374@hangdog.ibmoto.com>
X-Mailer: exmh version 1.5 11/22/94
To: info-hol@leopard.cs.byu.edu, larch-interest@pa.dec.com,
nqthm-users@CLI.COM, theorem-provers@ai.mit.edu, qed@mcs.anl.gov
cc: raina@ibmoto.com
Subject: DAC 1996 - Special Topics Session on Functional Design Verification
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Wed, 27 Sep 95 16:20:36 -0600
From: Raj Raina <raina@ibmoto.com>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
*****************************************************************************
33rd DESIGN AUTOMATION CONFERENCE
LAS VEGAS CONVENTION CENTER
JUNE 3 - 7, 1996
ANNOUNCEMENT
============
The organizing committee for DAC '96 is planning a Special Topic Session
focusing on Functional Design Verification of Microprocessors. Papers are
being solicited from Microprocessor Design groups in the area of functional
design verification. Topics can include (but are not limited to) the
following subjects:
o Functional design verification methodology & experience on a chip.
o Functional verification coverage analysis techniques.
- toggle coverage
- state-machine coverage
- event coverage
o Design Modeling for functional verification - choices & tradeoffs.
o Design verification test generation - focused, random.
o Simulation/Emulation techniques for functional verification.
o When are we done with functional verification? Practical & Formal
methods for establishing "doneness" criteria.
o Techniques for stressing a design.
REQUIREMENTS FOR SUBMISSION OF PAPERS
Authors should submit their papers to the Program Chair postmarked no
later than October 6, 1995. Previously published papers, including
workshop proceedings, will not be considered. Each submission should
include one cover page and ten (10) stapled copies of the complete
manuscript.
The one cover page should include:
-Name, affiliation, and complete address for each author
-A designated contact person including his/her telephone number,
fax number, and email address
-A designated presenter, should the paper be accepted
-A list of topic numbers, ordered by relevancy, most clearly
matching the content of the paper
The following signed statement: "All appropriate organizational
approvals for the publication of this paper have been obtained. If
accepted, the author(s) will prepare the final manuscript in time for
inclusion in the Conference proceedings and will present the paper at
the Conference."
To permit a blind review, do not include name(s) or affiliation(s) of
the author(s) on the manuscript. Include:
-Title of paper
-60 word abstract indicating significance of contribution. The
abstracts of accepted papers will appear on the World Wide Web
before the Conference.
-The complete text of the paper in English, including all
illustrations and references, not exceeding 5000 words. The papers
will be reviewed as finished papers. Preliminary submissions will
be at a disadvantage.
Notice of acceptance will be mailed to the contact person by Feb 16,
1996. Authors of accepted papers must sign a copyright release form.
PROGRAM CHAIR
MP Associates, Inc.
ATTN: Program Chair, 33rd DAC
5305 Spine Rd., Suite A
Boulder, Colorado 80301
For information call: (303) 530-4333
Watch the WWW for updates! (http://www.dac.com/dac.html)
--
For more information on this Special Topics Session, please contact:
******************************************************************************
Raj Raina * e-mail: raina@ibmoto.com * (512) 795-7211
Address: Motorola at Somerset; MD: OE513; 9737 GH Trail, Austin, TX 78759
******************************************************************************