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:
-
A Bi-Intuitionistic Modal Logic: Foundations and Automation.
J. G. Stell, R. Schmidt and D. Rydeheard.
Journal of Logical and Algebraic Methods in Programming
85 (4),
500-519, 2016.
Abstract,
BiBTeX,
DOI Link to Elsevier.
- Tableau Development for a Bi-Intuitionistic Tense Logic.
J. G. Stell, R. Schmidt and D. Rydeheard.
In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds),
Relational and Algebraic Methods in Computer Science (RAMiCS 14).
Lecture Notes in Computer Science,
Vol. 8428,
Springer,
412-428 (2014).
Abstract,
BiBTeX,
PDF (final version available via DOI link to Springer).
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