MSPASS: Documentation
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).
Formal specification of the MSPASS input language.
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.
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)
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.
System descriptions
Regular papers
Please browse through these:
MSPASS
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, schmidt@cs.man.ac.uk