PV6 ⊧ Isabelle/HOLinteractive theorem prover

Application domain/field

• Interactive theorem proving
• Proof assistant
• Deductive verification

Type of tool

Interactive theorem prover/proof assistant

Expected input

A 'theory' that you want to proof correct. A theory is a collection of types, functions and theorems.

Format:

HOL (for the formula that should be proven) and Isar (language for writing proof scripts).

Expected output

Whether the mathematical formula has been proven. It is also possible to turn (verified) executable specifications into code (SML, OCaml, Haskell or Scala).

Internals

This is an interactive theorem prover based on higher-order logic. It is sometimes also called a "proof assistant". You can use it to prove the correctness of mathematical formulas. E.g. you can use it to verify the correctness of a protocol. Note that proving the correctness of something is an interactive process, while the tool can deduce some things automatically, it will often require user interaction! This interaction is done through writing proof scripts in the Isar language. Isabelle is also capable of turning executable specifications directly into code in SML, OCaml, Haskell and Scala.