MSPASS: Documentation

Input language

The input language of of MSPASS is that of SPASS extended to handle modal logic formulae, description logic formulae and formulae of the relational calculus. Non-first-order formulae are built from a vocabulary of propositional symbols of two disjoint types, namely, type Boolean (concept) and type relational (role). These need to be declared in advance as predicates with zero arity.

The repertoire of logical constructs includes:

The symbols true and false have multiple interpretations. Apart from their usual interpretation in propositional logic and first-order logic, true and false may also be used as Boolean or relational formulae. true used as a Boolean type, represents the universal set, and used as a relational type it represents the universal relation. Similarly, false can be used as the bottom Boolean and relational type, representing the empty set and the empty relation.

MSPASS supports non-logical axioms (terminological axioms), certain modal axioms, all modal correspondence properties. In addition, because the first-order symbol associated by the translation mapping to a propositional symbol can be declared, it is possible to specify concrete relationships between worlds (ABox statements) as well as any first-order restrictions on relations.

Sample input files: HalpernMoses_1.dfg, pdl_vacuum2.dfg (modal logic), DLexample.dfg (description logic), relational.dfg (relation algebra/relational calculus).

Formal specification of the MSPASS input language.

Translation mappings

A number of different translation methods are available. These include: In the current implementation the standard relational translation method is most general and applies to the language described above. Some restrictions apply to the other methods. The functional translation method and semi-functional translation methods are available for the basic multi-modal logic K(m) possibly with serial (total) modalities (-EMLTheory=1), plus atom structures (ABox statements), terminological axioms and general inclusion and equivalence axioms. The optimised functional translation methods are implemented for K(m), possibly with serial modalities.

Background theories

If the problem needs to be solved in some modal logic different from K(m), then the following options add the necessary frame properties (for all modalities):

Other features of MSPASS

MSPASS has other attractive features including:


System descriptions

Regular papers

Please browse through these:

Web Interactive Input Form | Web Upload Form | Documentation

Last modified: 05 Feb 07
Copyright © 1999-2005 Renate A. Schmidt, School of Computer Science, Man Univ,