ModProf is a package of LISP functions allowing theorem proving for the modal logic K with or without global assumptions.

ModProf was developed by:

Jens Happe
Computational Logic Lab
School of Computing Science
Simon Fraser University
Burnaby, B.C.
V5A 1S6, Canada

Reasoning tasks that can be performed with ModProf

Prominent features

Download ModProf Version 1.0!

Read the Modprof Version 1.0 User Manual,
or get the TeX version as a Postscript file!

Important Information

ModProf is known to run on Sun Sparc stations with Solaris 2.6 or higher, and Allegro Common LISP 4.3 and 6.0. It may also run on other platforms and other Common LISP dialects.

The ModProf package is free software; it can be used for non-commercial purposes under the terms of the GNU General Public License published by the Free Software Foundation. See the user manual for more info.

Research Papers about ModProf

(Please ask the author for a copy.)

[1] Jens Happe, The ModProf Theorem Prover, in: Automated Reasoning---First Int'l Joint Conference (IJCAR 2001), Springer-Verlag, LNAI 2083, 2001.

[2] Jens Happe, A Subsumption-Aided Caching Technique, in: E. Giunchiglia, F. Massacci(eds.), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, IJCAR-2001 Workshop, Technical Report DII 14/01, Università degli Studi di Siena, Italy, 2001.
Last Modified: 07/21/2001