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:

Implementation

  • MetTeL specification of the tableau calculus: biskt_calculi.zip
  • MetTeL generated provers for BISKT: biskt_provers.zip
  • Needed MetTeL packages: http://www.mettel-prover.org/downloads/mettel-2.0-646.zip
  • 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: biskt_problems.zip
  • 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, schmidt@cs.man.ac.uk