Version 1.0

Table of Contents

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


1 General purpose and functionality

ModProf is a package of LISP functions allowing theorem proving for the modal logic K with or without global assumptions. Its core data structure, the knowledge base, holds all the global and local assumptions entered by the user. Formulas are preprocessed into the knowledge base. The knowledge base can be saved, restored or emptied; however, individual formulas can not be retracted. For the internal format of the data structures see Appendix C.

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 non-commercial purposes. Details are specified in the public license contained in this documentation.

2 Outstanding features

3 Obtaining, compiling and running ModProf

The ModProf package can be obtained here. 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. (It is highly recommended to run ModProf under a case-insensitive LISP image.)

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 run-time 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.

4 ModProf syntax

Formulas in ModProf are denoted as follows:

fml = atom | (fml) | (fml1 & fml2) (logical AND) | (fml1 + fml2) (logical OR) | (fml1 -> fml2) | (fml1 <-> fml2) | ~ fml | ? fml (Possibility) | ! fml (Necessity)

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 right-associtive, 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:

true or *top* for T
false or *bottom* for NIL
dia or poss for ?
box for !
and for &
or or \| for +
=> for ->
<=> for <->.
Modal formulas can also be written as
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.

5 List of ModProf functions

In the following, 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.

(reset-affairs)
Empties the knowledge base and variable index.
(inputf L)
Adds the formula 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)
Stronger than (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.
(get-model L)
Finds a model for the formula L in the context of the current knowledge base. If a model for only the knowledge base is desired, set L to T.
This function returns the model in internal format. This model can be displayed in pretty format using print-model, written into a graph using graph-model, or saved into a LISP variable for later use.
(get-countermodel L)
Finds a countermodel for 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).
(is-consistent L)
Calls (get-model) on L and returns a string reporting whether or not a model exists. If so, the model will also be reported.
(is-implied L)
Calls (get-countermodel) 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)
Tests whether the specified model 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)
Tests whether the specified model M satisfies the formula L.
(satisfies-globally M L)
Tests whether all worlds in the specified model M satisfy the formula L, i.e. whether L is a global assumption satisfied by M.
(save-kb filename)
Writes all components of the knowledge base into the file with the specified name, which must be a new file. The satisfiability status of the knowledge base is saved, if known, but without a satisfying model.
(load-kb filename)
Reads a knowledge base previously saved by save-kb. The knowledge base is restored exactly to its state when it was saved.
(get-kb filename)
Different from load-kb, this function reads inputf and assertf commands (and possibly other LISP commands) from a file. Before opening the file, the knowledge base is emptied.
(print-affairs)
Prints the local formulas in the knowledge base into a (conjunctive) formula in infix notation.
(print-globals)
Prints the global formulas in the knowledge base into a (conjunctive) formula in infix notation.
(tops-affairs filename)
Prints a graphical representation of the local formulas in the knowledge base into a Postscript file named filename.
(tops-globals filename)
Prints a graphical representation of the global formulas in the knowledge base into a Postscript file named filename.
(print-model M)
Outputs a tabular form of a satisfying model. Each world of the model is shown in a different row, with an integer index. Beside its index, the variables assigned true and false, respectively, are shown; finally the indexes of all accessible worlds (successors) are displayed.
(graph-model M filename)
Outputs a graphical representation of the model into the specified file. The file can be read into the daVinci program package, which creates an optimized and aesthetically pleasing layout of the model graph. The worlds in the graph are labelled by the lists of variables assigned true and false, respectively.
Note that the daVinci package is licensed software, free to use for non-commercial purposes only. It is maintained and distributed by the Technologie-Zentrum Informatik, Technische Universität Bremen; the ModProf authors do not support any of their activities, nor give any guarantee for the availability or usability of this package.
(debug-to filename)
Sets ModProf into debugging mode. World templates will be protocolled into filename as they are traversed.
(no-debug)
Returns from the ModProf debugging mode. This function must be called to ensure that the debugging information will be completely written and the protocol file will be closed.

Convenience functions for loading problem files:

The following functions all read formulas from the file specified in the parameter; each time a model is created, the elapsed time and memory allocation is reported. At the beginning of command execution, the knowledge base is cleared.
(parse-tancs-file fname)
Accepts formulas in the format of the TANCS theorem prover comparisons. (See the practical information page.) A knowledge base is built up by reading global assumptions contained in commands of the form
inputformula (name, axioms, fml)
and local formulas contained in commands of the form
inputformula (name, hypothesis, fml).
Whenever a command of the form
inputformula (name, conjecture, true)
is encountered, a model will be constructed for the current knowledge base.
The language covered is actually a subset of the full specification. Concatenations, conjunctions or inverse roles are not supported.
(parse-tab98-file fname)
Accepts formulas in the format of the Logics Workbench, or equivalently, the Tableaux 1998 theorem prover comparisons. (See the .) Each line of the file beginning with an integer number is assumed to specify a formula. For each formula, it is tested whether a countermodel can be built, given an empty knowledge base.
(parse-alc-file fname)
Accepts formulas in the format of the Description Logic Benchmark Suite. (Technical report not available.) Note that only ALC satisfiability problems can be solved, not classification problems, as ModProf does not feature a description logics classifier.

6 ModProf messages

The following ModProf messages may be displayed to the user:

Status messages:

"Axiom entered into knowledge base."
States that a global assumption has been successfully entered through the command assertg or inputg.
"Formula entered into knowledge base."
States that a formula has been successfully inputted through the command assertf or inputf.
"ModProf Formula interpreter loaded."
Ready message of the ModProf system. Appears after loading the file affairs.cl or affairs.fasl.

"This formula is consistent. A model is: model."
Positive answer to the function is-consistent.
"This formula is inconsistent with the knowledge base."
Negative answer to the function is-consistent; 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."
A status report of 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."
Positive answer to the function is-implied.
"This formula does not follow from the knowledge base. A countermodel is: model."
Negative answer to the function is-implied.
"n worlds created."
Reports on the size of the model found upon any of the model-finding commands. If n is 0, the given formula is inconsistent with respect to the knowledge base.
"Attempting formula n."
Status message in function parse-tab98-file. Reports the index of the formula in the current Tableaux 1998 problem class attempted.

"Global Assumptions template printed into postscript file filename."
Completion message for function tops-globals.
"Local Assumptions template printed into postscript file filename."
Completion message for function tops-affairs.
"Model written into graph file filename."
Completion message for function graph-model.

Error or warning messages:

"This is not a syntactically correct formula."
The input formula is not well-formed according to the syntax described in Section 4. Possible causes are: omission of parentheses around binary operators; use of variable names that are reserved operators.

"Warning: The knowledge base may have become inconsistent."
A fairly common message after inputting a new formula with inputf or inputg. This indicates that a function like get-model 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 function-name: shouldn't happen"
ModProf encountered a formula template which, in normal operation with the simplification algorithm, should not occur, e.g. a template containing both a literal and its negation. If this error occurs, the proof or model can not be guaranteed to be correct. If this message reoccurs on a problem, please contact the developers immediately. Include into your message the input that causes the error.
A LISP I/O error message may occur on attempts to read a file which does not exist, or to overwrite a file which already exists. Make sure the cause for these errors is removed, then resume or restart execution of the command.

There is also the possibility of (non-repeatable 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.

A List of ModProf global variables

Knowledge of these variables is not required for working with ModProf. They are listed for reference purposes. Many of these variables are only used for debugging purposes.

*modprof-affairs*contains the local formulas of the knowledge base. It is recommended to not modify this data structure manually.
*modprof-globals*contains the global assumptions of the knowledge base. It is recommended to not modify this data structure manually.
*modprof-variables*A translation table for variable names into variable numbers (negative integers). It is recommended to not modify this table manually.
*print-modal-depth*An integer, determining the maximum modal depth to which a world is printed by the function print-template.
*debug*If set to T, ModProf runs in debug mode. For testing purposes only!
*debug-file*A file handle to the file into which debugging information is printed.
*node-level*An integer, determining the maximum depth to which debugging output for node expansion is printed. Root level is 0.
*loop-level*An integer, determining the maximum level to which debugging output for the simplification process is given.


B ModProf files

The ModProf functionality is split into several modules, which are kept in files as follows:
affairs.cluser interface, defines the knowledge base, update, retrieval and model checking operations
wff.clformula parser, converts an input formula into prefix notation and then to and/or normal form
world.clbasic routines for the template data structure, including conversion into templates, and printing them; as well as the structural subsumption algorithm
resolve.clthe simplification algorithm (function names which begin with resolve)
debug.clfunctionality for tracing and debugging the model checker
model.climplementation of the tableau algorithm, including branching rules, modal rules, and caching; also containing the model verification routines
sat.clRoutines who provide a ranking of formulas according to their estimated likelihood of being satisfiable
intset.cl
list.cl
some additional low-level functionality used in the other modules
pars.clparsers for various input file formats (see Section 5)
make.clSequence of LISP commands to compile the other modules of ModProf (see Section 3)
pshead.ps
psend.ps
Auxilliary files for creating postscript printouts of templates.

C ModProf data structure

Formulas are first converted into and/or normal form with negations pulled inside as far as possible. Subsequently, they are converted into templates, which represent a ``canonical form'' of the formula. Templates are tuples of the form 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 so-called 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.

GNU Public License

The ModProf package is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

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 02111-1307, 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

References

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


http://www.cs.sfu.ca/~cl/Projects/Modprof/manual.html
Last Modified: 07/19/2001