Isabelle
Formal-language theorem proving
What it does
Isabelle provides a generic proof assistant expressing formulas in formal languages and using logical calculi and supporting tools to construct mechanically checkable proofs.
When to use it
For structured proofs, consult Isar and logic references to understand theorem statements and the relationship between successive reasoning steps.
