Isabelle Isar
Features
- In some ways, writing a proof in Isabelle/Isar is like writing a function in an interpreted programming language.
- the computational realization of a formal ontology in Isabelle/HOL/Isar facilitates the explicit separation of three fundamental levels of ontology development: (I) the level of axiomatization; (II) the level of model instantiation; and (III) the level of theory presentation.
Backlinks