Isabelle

Owner: makarius

Category: Application

Isabelle theorem prover

Isabelle is a theorem prover for higher-order logics (HOL, ZF etc.). It is an integrated development environment for theories, proofs, and mathematical tools in Isabelle/ML (based on Poly/ML). System programming is done in Isabelle/Scala.

Dependencies:

Platform: Linux, Windows, macOS

Poly/ML version: bundled

Licence: BSD and others

Download link: https://isabelle.in.tum.de

Project link: https://isabelle-dev.sketis.net