Tinker - STTT paper resources

Authors : G. Grov and Y. Lin

Foreword

This webpage aims to present resources used for our tool presentation. To use these resources

1. Download and install Isabelle (the latest version is 2016-1) from here.

Then go to the contrib directory:

cd contrib

and grab the quantomatic libraries either over https,:

git clone -b tinker https://github.com/Quantomatic/quantomatic

Note that this assumed that you have `git` installed.

2. Download and install Tinker from here

git clone -b sttt16 https://github.com/ggrov/tinker.git

The example files are available under:

$SOME_PATH/tinker/src/core/demo/STTT16/

In sttt_setup.thy, set tinkerhome to the path of tinker, e.g.

$SOME_PATH/tinker

The example can then be run by opening the file sttt_example.thy. For more details on how to start the GUI can be found in Tinker's user guide.

Disjunctions to the top

Existential quantifiers via a one-point rule

This recording shows the use of breakpoint to debug version0 of the one point rule:

This recording compares the differences between version0 and version1

This recording shows the evaluation of the version1:

Rippling + PWF

Tool demo