----- Unsent message follows -----
Received: by antares.mcs.anl.gov id AA02837
(5.65c/IDA-1.4.4 for qed-outgoing); Sun, 19 Dec 1993 15:35:32 -0600
Received: from uqcspe.cs.uq.oz.au by antares.mcs.anl.gov with SMTP id AA02830
(5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>); Sun, 19 Dec 1993 15:35:29 -0600
Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au
id <AA02446@uqcspe.cs.uq.oz.au>; Mon, 20 Dec 93 07:35:10 +1000
Date: Mon, 20 Dec 93 07:35:09 EST
From: pjr@cs.uq.oz.au
Message-Id: <9312192135.AA06183@client>
To: qed@mcs.anl.gov
Subject: Qu-Prolog 3.2 and Ergo 4.0
Sender: qed-owner
Qu-Prolog 3.2 and the interactive theorem prover Ergo 4.0
are now available by ftp from ftp.cs.uq.oz.au
These systems are research prototypes only and will
not be supported.
Qu-Prolog is a high-level language designed primarily
for rapid prototyping of interactive theorem provers
and, more generally, for symbolic computation on formal languages.
Its object level includes quantified terms and object variables.
See SVRC Tech. Report 93-18, available from the same ftp site, for details.
As an example Ergo 4.0 is implemented in Qu-Prolog 3.2.
The compactness and high level of Ergo 4.0 source code demonstrate the
advantages of Qu-Prolog for such applications.
We are currently implementing the next version of Qu-Prolog.
The new version will be a more efficient implementation
with more expressive power.
Extensions in the next version to the object language supported
by Qu-Prolog 3.2 include
* functions with arbitrary terms in the functor position
(e.g. higher-order notation)
* functions with an unspecified number of arguments
* quantified terms with arbitrary terms in the quantifier position
* parallel quantification with notations that can
be used to type the bound variables
The portability of the makefiles
and the source files have been tested only on sun4.
Ergo 4.0 is an interactive theorem prover, designed and implemented
at the Software Verification Research Centre (SVRC) at The University of
Queensland. It has the following features:
* A 'window inference' method that is specifically designed
to support hierarchical goal-directed proofs and allow easy
access to the context of a subterm.
* Support for defining a variety of logics.
* Support for proving schematic theorems and answer extraction.
* The use of a high level logic programming language, Qu-Prolog,
for implementation and for writing tactics and interfaces.
* An automatic mechanism for recording proofs. This records
the high level tactics used in proofs as well as the low
level transformations that are generated by those tactics.
* Support for storing, browsing and replaying proofs.
* A directed acyclic graph of theories.
* A powerful query language for searching a set of theories.
* A heuristic environment for automating common proof steps.
Ergo has been and is being used to support the development of
verified software (eg. SVRC Technical Report 92-10. "Real Time
Behaviour of a RISC processor: Specification and Computer-Aided
Verification"). Further versions of Ergo are planned. Improvements
are expected to include:
* more theories (esp. Z library theories), tactics and heuristics.
* generic/parameterised theories.
* the integration of window and natural deduction inference styles.
* more sophisticated ways of reusing recorded proofs, such as
the ability to rerun proofs at various levels of abstraction
and utilities for extracting tactics from proofs.
RELEVANT FILES
pub/SVRC/software/qp.tar.Z : A compressed tar file containing
Qu-Prolog 3.2.
pub/SVRC/software/ergo.tar.Z : A compressed tar file containing Ergo 4.0.
pub/SVRC/techreports/tr93-18.ps.Z : Technical Report 93-18.
HOW TO GET THESE FILES
Sample FTP Session
$ ftp ftp.cs.uq.oz.au
Name: anonymous
Password: <your e-mail address>
ftp> cd <appropriate directory>
ftp> bin
ftp> get <file>
ftp> quit
$ uncompress <file>
To build Qu-Prolog 3.2
$ tar -xf qp.tar
$ cd qp3.2
$ more INSTALL
$ make compile
To build Ergo 4.0
$ tar -xf ergo.tar
$ cd ergo
$ more INSTALL
Send any comments to pjr@cs.uq.oz.au