[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.