Duration Calculus Proof Checker Prototype Now Available by FTP
==============================================================

This is to announce the availability of the Beta Version of the Proof
Checker for Duration Calculus (PC/DC) [1].

PC/DC provides an environment for analyzing, modifying, and
documenting Duration Calculus (DC) specifications and proofs.
Formulas can be expressed in a specification language using a syntax
close to the DC notation.  Proofs are carried out in a Gentzen style
DC proof system.  

This is the first release of the system and is a prototype. The proof
checker has been created as a semantic embedding in PVS with special
parsing/pretty-printing features and provides most of the
functionality of PVS.

Instructions on how to obtain the system are provided below.

Please send questions and problem reports to: jus@id.dtu.dk.

Best regards,

Jens


[1] J.U. Skakkeb{\ae}k and N. Shankar: Towards a {D}uration {C}alculus
    Proof Assistant in PVS, in Proceedings of Symposium on Formal
    Techniques in Real-Time and Fault Tolerant Systems, Lecture Notes in
    Computer Science 863, pp. 660-679.

=============================================================================
Jens Ulrik Skakkebaek *  jus@id.dtu.dk  *   Department of Computer Science
Technical University of Denmark, Building 344      DK-2800 Lyngby, Denmark

New address: 
Jens Ulrik Skakkebaek * jus@spd.cri.dk * Computer Resources International A/S 
Space Division     *    Bregneroedvej 144    *     DK-3460 Birkeroed, Denmark
Tel: +45 45 82 21 00 * Direct: +45 45 82 22 66 / 2241  * Fax: +45 45 82 32 17
=============================================================================


Obtaining and Installing PC/DC
==============================

The system is obtained and installed in the following steps:

1. Create a file in your local PVS directory called ``dc'': mkdir dc
   and change to this directory: cd dc.

2. Get PC/DC by anonymous ftp from ftp.id.dtu.dk as the tar
   file: /pub/ProCoS/Jens.U.Skakkebaek/PCDC.tar.Z in binary mode.

3. Uncompress the file: uncompress PCDC.tar.Z

4. Extract files from the tar file: tar xpf PCDC.tar

5. Modify your ~/.pvsemacs to include the contents of the
   file: dc/load-dc.

6. Print out the documentation found in pvs/dc/doc.

7. The system is now ready for use.