Описание тега isabelle

Isabelle is a generic proof assistant, which is best-known for its Isabelle/HOL instance. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. HOL specifications may be turned into program code in SML, OCaml, Haskell, or Scala. Isabelle includes many add-on tools like CVC4, Z3, SPASS, E prover.

User interfaces

• Isabelle/jEdit Prover IDE (default)
• Isabelle/VSCode (experimental)
• Isabelle/Eclipse (inactive)
• Clide (inactive)

Important links

• Main website (mirrors): Cambridge (.uk) and Munich (.de) and Sydney (.au) and Potsdam, NY (.us)
• The Archive of Formal Proof with Isabelle examples and applications.
• The isabelle-users mailing list.