1 General purpose and functionality
2 Outstanding features
3 Obtaining, compiling and running ModProf
4 ModProf syntax
5 List of ModProf functions
6 ModProf messages
A List of ModProf global variables
B ModProf files
C ModProf data structure
GNU Public License
References
A knowledge base can be checked for satisfiability (or validity). Alternatively, a single formula can be checked for satisfiability (or validity) with respect to the knowledge base. This allows to verify e.g. whether a formula is implied by a set of global and local assumptions.
For satisfiable formulas, models are generated which can be stored or printed for later use.
Since ModProf is executed from the LISP command interface, the entire functionality of Common LISP can be used to preprocess formulas or postprocess ModProf output. ModProf is an open source application, i.e. the source code can be viewed and modified for research and noncommercial purposes. Details are specified in the public license contained in this documentation.
After unpacking the files into a directory, change into this directory, start LISP, and then compile the files using the command
:ld make.cl
This will compile all the files in the package, which is strongly recommended for efficient runtime behaviour. (You will only need to repeat this step after making changes to the source code.)
Now you can run ModProf by typing
:ld affairs
ModProf is ready to accept input as soon as the message
"ModProf formula interpreter loaded."
appears.
Parentheses around terms beginning with unary operators are not necessary.
Parentheses can also be omitted within sequences of terms connected by the same
binary connective, which is always parsed rightassocitive, i.e. a > b > c
is parsed
(a > (b > c))
.
An atom is any LISP symbol which is not a connective. Special atoms are the logical
constants T
and NIL
(for \bottom, the logical falsum).
A formula with all or parts of its binary operations written in prefix notation
is correctly parsed; however, a operation in prefixed notation must specify
exactly 2 operands.
Formulas are accepted, but cannot be printed, in the following alternative formats:
Modal formulas can also be written astrue
or*top*
forT
false
or*bottom*
forNIL
dia
orposs
for?
box
for!
and
for&
or
or\
for+
=>
for>
<=>
for<>
.
some rel fml
all rel fml
box rel \: fml
dia rel \: fml
In this, rel is ignored. Different relations cannot be distinguished as of Version 1.0.
L
will represent a formula according to the
syntax outlined above. Note that LISP expects the formula in the form '(formula)
.
Syntactically incorrect formulas will be rejected with an error message.
(resetaffairs)
(inputf L)
L
to the knowledge base and performs a
subsumption check. If the formula is found inconsistent with the knowledge
base, it will be rejected, and the knowledge base will remain unchanged.
Otherwise, the formula will be added, and a reminder will be printed out
that the knowledge base may still have become inconsistent.
(assertf L)
(inputf L)
. The formula is added to a copy of the
knowledge base, and after the subsumption check, ModProf will try to
create a model. If no model exists, the knowledge base remains unchanged.
Otherwise, the updated knowledge base will become the current knowledge base.
The model found will be rejected.
(getmodel L)
L
in the context of the current
knowledge base.
If a model for only the knowledge base is desired,
set L
to T
.printmodel
, written into a graph using
graphmodel
, or saved into a LISP variable for later use.
(getcountermodel L)
L
, i.e. a model satisfying
the current knowledge base that satisfies (~ L)
. If this function returns
NIL
, it means that L
is a valid formula (i.e. implied by the knowledge base).
(isconsistent L)
(getmodel)
on L
and returns a string reporting
whether or not a model exists. If so, the model will also be reported.
(isimplied L)
(getcountermodel)
on L
and thus tests
whether the formula L
follows logically from the current
knowledge base. Returns a string reporting whether or not a countermodel exists.
If yes, the falsifying model will also be printed.
(modelp M)
M
satisfies the
current knowledge base, that is, its root world satisfies the local formula, and
every world of the model satisfies the global assumptions..
(satisfiesp M L)
M
satisfies the formula L
.
(satisfiesglobally M L)
M
satisfy the formula L
, i.e. whether L
is a
global assumption satisfied by M
.
(savekb filename)
(loadkb filename)
savekb
. The
knowledge base is restored exactly to its state when it was saved.
(getkb filename)
loadkb
, this function reads
inputf
and assertf
commands (and possibly other LISP commands) from a file.
Before opening the file, the knowledge base is emptied.
(printaffairs)
(printglobals)
(topsaffairs filename)
(topsglobals filename)
(printmodel M)
(graphmodel M filename)
(debugto filename)
(nodebug)
(parsetancsfile fname)
inputformula (name, axioms, fml)
inputformula (name, hypothesis, fml)
.inputformula (name, conjecture, true)
(parsetab98file fname)
(parsealcfile fname)
"Axiom entered into knowledge base."
assertg
or inputg
.
"Formula entered into knowledge base."
assertf
or inputf
.
"ModProf Formula interpreter loaded."
affairs.cl
or affairs.fasl
.
"This formula is consistent. A model is: model."
isconsistent
.
"This formula is inconsistent with the knowledge base."
isconsistent
; also a status report of
assertf
, and sometimes inputf
, that the formula has not been added to the
knowledge base since doing so would render it inconsistent.
"This axiom is inconsistent with the knowledge base."
assertg
, and sometimes inputg
, that the formula has not been
added to the set of global assertions, since doing so would render the knowledge
base inconsistent.
"This formula follows logically from the knowledge base."
isimplied
.
"This formula does not follow from the knowledge base. A countermodel is: model."
isimplied
.
"n worlds created."
"Attempting formula n."
parsetab98file
.
Reports the index of the formula in the current Tableaux 1998 problem class
attempted.
"Global Assumptions template printed into postscript file filename."
topsglobals
.
"Local Assumptions template printed into postscript file filename."
topsaffairs
.
"Model written into graph file filename."
graphmodel
.
"This is not a syntactically correct formula."
"Warning: The knowledge base may have become inconsistent."
getmodel
must be called to verify if the
knowledge base is still consistent. The message is shown only once if several
formulas are inputted in sequence.
"Error in functionname: shouldn't happen"
There is also the possibility of (nonrepeatable and seemingly unexplicable) LISP system errors. These errors have been observed on very large problems, when ModProf runs out of memory. In this case, try allocating a larger amount of swap space, or run the problem on a machine with a larger amount of main memory.
*modprofaffairs*  contains the local formulas of the knowledge base. It is recommended to not modify this data structure manually. 
*modprofglobals*  contains the global assumptions of the knowledge base. It is recommended to not modify this data structure manually. 
*modprofvariables*  A translation table for variable names into variable numbers (negative integers). It is recommended to not modify this table manually. 
*printmodaldepth*  An integer, determining the maximum modal depth to which
a world is printed by the function printtemplate .

*debug*  If set to T , ModProf runs in debug mode. For testing purposes only!

*debugfile*  A file handle to the file into which debugging information is printed. 
*nodelevel*  An integer, determining the maximum depth to which debugging output for node expansion is printed. Root level is 0. 
*looplevel*  An integer, determining the maximum level to which debugging output for the simplification process is given. 
affairs.cl  user interface, defines the knowledge base, update, retrieval and model checking operations 
wff.cl  formula parser, converts an input formula into prefix notation and then to and/or normal form 
world.cl  basic routines for the template data structure, including conversion into templates, and printing them; as well as the structural subsumption algorithm 
resolve.cl  the simplification algorithm (function names which begin with resolve )

debug.cl  functionality for tracing and debugging the model checker 
model.cl  implementation of the tableau algorithm, including branching rules, modal rules, and caching; also containing the model verification routines 
sat.cl  Routines who provide a ranking of formulas according to their estimated likelihood of being satisfiable 
intset.cl  some additional lowlevel functionality used in the other modules 
pars.cl  parsers for various input file formats (see Section 5) 
make.cl  Sequence of LISP commands to compile the other modules of ModProf (see Section 3) 
pshead.ps  Auxilliary files for creating postscript printouts of templates. 
w = (F,P,N,D,c)
,
where F
is a storage space
for formulas which are in the stage of being converted into or added to
the template, as well as for statistical information; P
and N
are
(ordered) lists of propositional variables representing positive and negative
literals, D
is a list of socalled dual templates,
and c
is a constraint template.
We also define the inconsistent and the empty template,
represented as NIL
and 0
. Templates can be arbitrarily nested;
the outermost template in such a data structure is called the root template.
An empty root template is represented by (NIL,NIL,NIL,NIL,0)
,
deviating from the above rule.
A template represents the conjunction of its components; its constraint
template represents the conjunction of its components which are necessities.
Each of the remaining components  disjunctions and possibilities 
is represented by a dual template, which is the negation of the formula to be
represented. For instance, the disjunction (A + B + ~ C)
is represented by
a template containing the literals ~ A
, ~ B
, and C
, i.e. the template
(NIL,(C),(A,B),NIL,0)
. Hence, disjunctions and possibilities are implicitly
represented by the depth of the structure. This incorporates the duality
principle and allows for uniform handling of dual phenomena, such as
tautology and inconsistency. For details, see Reference [1].
The knowledge base maintains two distinct templates: the local assumptions and the global assumptions. Global assumptions are copied into the working templates each time a new world in the model is accessed.
To attain greater efficiency, variables are represented by (negative) integers. (Positive integers may be specified as variables by the user; these are left unchanged.) A hash table of variables is created to allow the conversion between the user format and the internal representation of variables.
ModProf is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should receive a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place  Suite 330, Boston, MA 021111307, USA.
ModProf has been developed by, and is the Copyright (C) 2001 of:
Jens Happe
Computational Logics Lab
School of Computing Science
Simon Fraser University
Burnaby, B.C.
V5A 1S6, Canada
[2] Jens Happe, A SubsumptionAided Caching Technique, in: E. Giunchiglia, F. Massacci(eds.), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, IJCAR2001 Workshop, Technical Report DII 14/01, Università degli Studi di Siena, Italy, 2001.