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