[Next][Index][Thread]
The theorem-prover Isabelle
Date: Wed, 17 Jan 90 11:45:34 GMT
To: proof%cs.chalmers.se@nsfnet-relay.ac.uk,
theorem-provers%mc.lcs.mit.edu@nsfnet-relay.ac.uk,
NEW VERSION OF ISABELLE AND MANUAL
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. Isabelle is written in Standard ML.
This release includes an Earley-type parser generator. Syntax rules are
specified in a mixfix notation, with pretty printing annotations. Some
translations still have to be coded in ML (particularly those involving
variable binding), but the rest is automatic.
The Manual has been completely rewritten. Its 150 pages include a gentle
introduction to Isabelle, descriptions of the built-in logics, and
discussion of advanced techniques. Every section contains several sample
sessions.
To existing license holders. You may obtain this release by e-mail, if
possible. Isabelle's new syntax, while far more concise, is not upwards
compatible with previous releases. Tools are provided to help you convert
to the new syntax.
For more information, please contact
Tobias Nipkow E-mail: tnn@cl.cam.ac.uk
Computer Laboratory Phone: +44-223-334600
University of Cambridge Fax: +44-223-334748
Pembroke Street
Cambridge CB2 3QG
England
or (until July 1990; thereafter at Cambridge)
Lawrence C Paulson E-mail: lcp@lfcs.ed.ac.uk
Department of Computer Science Phone: +44-31-667-1081
University of Edinburgh
Mayfield Road
Edinburgh EH9 3JZ
Scotland