1
0
mirror of https://git.FreeBSD.org/ports.git synced 2024-12-05 01:55:52 +00:00
freebsd-ports/math/isabelle/pkg-descr
Simon Barner 80bd7289ee Add isabelle 2004, a generic proof assistant.
PR:		84859
Submitted by:	Timothy Bourke <timbob@bigpond.com>
2005-09-01 10:03:58 +00:00

21 lines
978 B
Plaintext

Isabelle is a generic proof assistant. It allows mathematical
formulas to be expressed in a formal language and provides tools
for proving those formulas in a logical calculus. The main application
is the formalization of mathematical proofs and in particular formal
verification, which includes proving the correctness of computer
hardware or software and proving properties of computer languages
and protocols.
Compared with similar tools, Isabelle's distinguishing feature is
its flexibility. Most proof assistants are built around a single
formal calculus, typically higher-order logic. Isabelle has the
capacity to accept a variety of formal calculi. The distributed
version supports higher-order logic but also axiomatic set theory
and several other formalisms. See logics for more details.
Isabelle is a joint project between Lawrence C. Paulson (University
of Cambridge, UK) and Tobias Nipkow (Technical University of Munich,
Germany).
WWW: http://isabelle.in.tum.de