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