ModProf is a package of LISP functions allowing theorem proving for the modal logic K
with or without global assumptions.
ModProf was developed by:
Computational Logic Lab
School of Computing Science
Simon Fraser University
V5A 1S6, Canada
Reasoning tasks that can be performed with ModProf
- Checking a knowledge base for consistency
- Checking a formula for satisfiability, given a knowledge base of local and
- Checking whether a knowledge base implies a formula
- Generating a Kripke model for the knowledge base, or for a formula
- Verifying a Kripke model
- a highly normalized template data structure, which allows fast reasoning
and compact representation
- Templates can be listed and even graphically outputted.
- An extensive simplification process which eliminates a wide range of
obvious redundancies and contradictions
- efficient caching of submodels
- a structural subsumption checker which powers the simplification and
- Kripke models generated can be printed in tabular form,
or into a graphical structure.
Download ModProf Version 1.0!
Read the Modprof Version 1.0 User Manual,
or get the TeX version as a Postscript file!
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.)
 Jens Happe, The ModProf Theorem Prover, in: Automated Reasoning---First Int'l Joint Conference (IJCAR 2001), Springer-Verlag, LNAI 2083, 2001.
 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