From MAILER-DAEMON Thu Dec 23 16:21:32 1993 Received: by antares.mcs.anl.gov id AA16884 (5.65c/IDA-1.4.4); Thu, 23 Dec 1993 16:19:37 -0600 Date: Thu, 23 Dec 1993 16:19:37 -0600 From: Mail Delivery Subsystem Message-Id: <199312232219.AA16884@antares.mcs.anl.gov> To: qed-owner Cc: Postmaster Subject: Returned mail: Cannot send message for 4 days ----- Transcript of session follows ----- 421 hubinf.informatik.hu-berlin.de (TCP)... Deferred: Connection timed out during user open with hubinf.informatik.hu-berlin.de ----- 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 ); Sun, 19 Dec 1993 15:35:29 -0600 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; 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: ftp> cd ftp> bin ftp> get ftp> quit $ uncompress 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