Implementation and experimental data for the logic BISKT

This is the webpage accompanying work undertaken by John Stell, Renate Schmidt and David Rydeheard on the logic BISKT, a logic of bi-intuitionistic stable tense logic.

This work is published as:


  • MetTeL specification of the tableau calculus:
  • MetTeL generated provers for BISKT:
  • Needed MetTeL packages:
  • Download all of the above into one directory. To generate a prover type:
    java -jar mettel2.jar -i BISKT_specification
    To run the generated prover type:
    java -jar BISKT.jar
    To specify a problem file use -i (optional). Without -i, enter formulae at the terminal. ^D on a new line terminates the input and starts the run.

    Experimental data and results

  • Problem set:
  • Results: stats_BISKT200_10624, stats_AtMonBISKT200_10624, stats_NoBlockingBISKT200_10624
  • Results as plots: biskt_plots.pdf

  • Renate A. Schmidt
    Home | Publications | Tools | FM Group | School | Man Univ

    Last modified: 23 Nov 16
    Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ,