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

• Checking a knowledge base for consistency
• Checking a formula for satisfiability, given a knowledge base of local and global axioms
• Checking whether a knowledge base implies a formula
• Generating a Kripke model for the knowledge base, or for a formula
• Verifying a Kripke model

Prominent features

• 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 caching algorithms
• Kripke models generated can be printed in tabular form, or into a graphical structure.

Important Information

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

[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.