[Prev][Next][Index][Thread]

Isabelle available by FTP



Date: Wed, 9 May 90 15:26:02 BST
To: ailist%ai.ai.mit.edu@nsfnet-relay.ac.uk,
        info-hol%clover.ucdavis.edu@nsfnet-relay.ac.uk,
        logic@theory.lcs.mit.edu, proof-sci%cs.chalmers.se@nsfnet-relay.ac.uk,
        types@theory.lcs.mit.edu


	Theorem Prover ISABELLE now available by FTP

Isabelle is now available for anonymous ftp from princeton.edu and
research.att.com.  It now has a nonrestrictive copyright notice similar to
that of the X Windows system.  This means you do not need to sign a license
to obtain a copy of Isabelle, and you are free to redistribute Isabelle as
long as you retain the copyright notices and permission notice.

Thanks to Andrew Appel and David MacQueen for making Isabelle available by
ftp. Isabelle resides on the same directory as Standard ML of New Jersey.
Note however that Isabelle was developed using a different compiler, called
Poly/ML. Although Isabelle has been tested under SML of New Jersey, the
compilers are not completely compatible. In particular, the Makefiles will
only work for Poly/ML.

Isabelle is a generic theorem prover. It suppports interactive proof in
several formal systems, including first-order logic (intuitionistic and
classical), higher-order logic, Martin-L\"of type theory, and
Zermelo-Fraenkel set theory. New logics can be introduced by specifying
their syntax and rules of inference. Both natural deduction and sequent
calculi are allowed. Proof procedures (tactics and tacticals) can be
expressed using Standard ML.

For more information about Isabelle, consult the following:

L. C. Paulson, Natural deduction as higher-order resolution,
Journal of Logic Programming 3 (1986), 237-258.

L. C. Paulson, The foundation of a generic theorem prover,
Journal of Automated Reasoning 5 (1989), 363-397.

L. C. Paulson, Isabelle: The next 700 theorem provers,
In: P. Odifreddi (editor), Logic and Computer Science
(Academic Press, 1990, in press), 361-385.

---------------------------------------------------------------------------
FTP instructions:

To obtain Isabelle by internet ftp, connect to host princeton.edu use
login id "anonymous" with your name as password, and go to directory
pub/ml/isabelle ("cd pub/ml/isabelle").  Then put ftp in binary mode
("binary") and "get" the relevant files in that directory.  An
alternate site is research.att.com, directory "dist/ml/isabelle".

Host:		 Net Address:	Login:	    Passwd:	Directory:
princeton.edu	 128.112.128.1	anonymous   Your name	pub/ml/isabelle
research.att.com 192.20.225.2	anonymous   Your name	dist/ml/isabelle

The directory pub/ml/isabelle (dist/ml/isabelle on research.att.com)
contains the compressed tar file isabelle.tar.Z, which contains the
sources.  Ftp MUST be put into BINARY MODE before transferring this
file.

Here is a sample dialog:

   ftp
   ftp> open princeton.edu [research.att.com]
   Name: anonymous
   Password: <your name>
   ftp> binary
   ftp> cd pub/ml/isabelle [dist/ml/isabelle]
   ftp> get isabelle.tar.Z
   ftp> close
   ftp> quit

Once transferred, the file should be uncompressed using the uncompress
command, then extracted using tar into a directory called isa. The
following sequence of commands should suffice:

   mkdir isa
   mv isabelle.tar.Z isa
   cd isa
   uncompress -c isabelle.tar.Z | tar xf -

Once you have completed those commands, the directory should contain
the files announce, License, and README.NJ. The file README.NJ contains
instructions for compiling Isabelle under SML of New Jersey.