# 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 standard Boolean operators on Boolean type and relational type formulae: true, false, not, and, or, implies (subsumed by), implied (subsumes), equiv,
• multi-modal operators, with complex relational arguments: dia and box (synonymes are some and all), as well as domain and range,
• additional relational operators: comp (composition), sum (relative sum), conv (converse), id (the identity relation), div (the diversity relation), and
• test (test), domrestr (domain restriction) and ranrestr (range restriction).
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).

## Translation mappings

A number of different translation methods are available. These include:
• the standard relational translation method (which is determined by the usual Kripke semantics)
option: -EMLTranslation=0 (default)
• the functional translation method
option: -EMLTranslation=1
• the optimised functional translation method
option: -EMLTranslation=2
including a variation defined in terms of n-ary predicates instead of unary predicates and paths
options: -EMLTranslation=2 -EMLFuncNary=1
• the semi-functional translation method
option: -EMLTranslation=3
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):

• -EMLTheory=1 for KD(m)
• -EMLTheory=2 for KT(m)
• -EMLTheory=3 for KB(m)
• -EMLTheory=4 for K4(m)
• -EMLTheory=5 for K5(m)
• -EMLTheory=6 for S4(m)
• -EMLTheory=7 for S5(m)

## Other features of MSPASS

MSPASS has other attractive features including:
• It is a decision procedure for many decidable modal logics (e.g. extensions of Boolean modal logic with converse, cylindrification, domain/range restriction, positive occurrences of composition).
• It is a decision procedure for many decidable description logics (e.g. extensions of ALB with cylindrification, domain/range restriction, positive occurrences of composition).
• It is a decision procedure for many solvable first-order fragments including the guarded fragment, Maslov's class K, first-order logic in two variables, DL*, (soon) all decidable quantifier prefix classes.
• It implements improved and extended renaming techniques.
• It outputs not only yes/no answers but it also outputs a proof or saturated set of clauses.
• It can be used as a model generator.
• Features of SPASS.