References and links

Here is some useful code if you want to do your own empirical analysis of decision procedure for modal logic:
genmodal.lsp
LISP code for generating hard random modal formulae according to the guidelines given in the MPII research report 97-2-003.
ftmodal.pl (Version 1.2)
SICStus Prolog code for the functional translation of modal formulae.
simplify.pl
SICStus Prolog code for simplifying modal formulae.
oft.tgz (Version 1.4)
A small collection of files to use the functional translation approach. Requires FLOTTER, SPASS, CLISP, SICStus Prolog, and Perl.
Availability of the systems mentioned in our report.
FaCT
FaCT request form.
KSAT
LISP Code. Allegro Common Lisp 4.1, 4.2, AKCL 1.623, or GCL (GNU Common Lisp) Version(2.1) is required.
KRIS
LISP Code. CLISP 1996-03-15 is required.
The Logics Workbench
Libraries and executable for Sun Solaris 2.x.
Further information can be found at the home page of the LWB
ModLeanTAP
Prolog Code. SICStus Prolog is required.
Further information can be found at the home page of ModLeanTAP

For further information about computational tools for modal logics see the page maintained by Renate Schmidt.


Contents | Previous: Semantic versus syntactic branching
[an error occurred while processing this directive]