/calculus-toolbox

A set of tools for generating calculi in Isabelle and supporting tools through a JSON description file

Primary LanguageIsabelleMIT LicenseMIT

calculus-toolbox

A set of tools for generating calculi in Isabelle and supporting tools through a JSON description file

Get started

To get started, fork the github repository or download the project as a zip file and then head over to the Introduction page.

If you are using an older version of Isabelle (2014/2015), switch to the isabelle2015 branch via git checkout isabelle2015.

System requirements

To run the tools in the Calculus Toolbox, you need the following:

  • Isabelle2016 (isabelle needs to be added to bash PATH) (if running Isabelle2014, please use the --isa2014 flag when compiling the calculus)
  • Scala (preferred 2.10 or higher)
  • Python (2.7 or higher)
  • (optional) npyscreen and watchdog python modules

Compiled toolboxes

Compiled toolboxes for the D.EAK calculus and a version of an LK Sequent calculus fragment are available as separate repositories here: