|
|
Description
In brief
The MetTeL system consists of two parts at the moment.
The first part is a general tableau core
and plug-in like specifications of
several tableau systems.
The second part gathers a few translators
from MetTeL language into SPASS and MSPASS prover
.dfg representation of problems in
first-order language.
A bit of history
The implementation of the MetTeL system has been started
in June 2005 at the Computer Science Department of
The University of Liverpool.
At that time, the main aim of the implementation was to develop
a decision algorithm for metric logics
with the tessellation (`closer') operator.
That is why it called MetTeL which is an abbreviation
from "Met(ric) Te(sselation) L(ogic)".
Because there were no tableau calculus formulated
for metric logics with the `closer' operator
and many experiments with different tableau rules
were to be performed,
my decision was to make the tableau part
of the system as flexible as possible.
About the tableau part of the system
I tried to achieve flexibility of
specification of tableau algorithms
by writing
a core which can deal with standard generics
of tableau algorithms: rule applications,
loop-checking, etc
allow to arbitrarily extend algorithms
by tableau rules.
For this purpose,
before the implementation started,
I developed a language
for representation of a tableau calculus.
Although, at the moment, this language
exists only as a sub-hierarchy of classes
in the system, I see no problems
(except possibly a lack of time)
to formalise it more strictly.
In future releases,
I am going to implement
a small addition to the tableau system
which will be able to parse
a tableau specification in this language
and obtain a tableau prover as result.
Most of tableau rules
can be represented in this tableau language.
This allows to implement and add a new rule
in a matter of several minutes.
So, at the moment, every tableau rule
can be regarded as a separate plug-in
to the tableau core of MetTeL.
|