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.

The implementation was very rapid, about four months for the core of the tableau. It, in particular, were based on the following ideas.

• The unrestricted blocking rule has been implemented in the tableau prover on early stages of its development as an attempt to avoid complications related to standard loop checking mechanisms for the metric logics. My aim was to exploit the effective finite model property of these logics for termination of corresponding tableau algorithms. However, difficulties in the proof of termination caused that the rule was replaced by the standard loop-checking mechanisms. A second life for the unrestricted blocking rule began after a discussion with Renate Schmidt about importance of fairness for termination of deterministic tableau procedures.In 2007, I found how to prove a general termination of sound and complete tableau algorithms equipped by this rule with use of the filtration technique which is commonly employed in proofs of the effective finite model property in the area of Modal Logic. Original proof was for the description logic ALBO [ISWC2007] but has been generalised to for arbitary sound and complete tabelau calculi and logics which admit finite filtrations [IJCAR2008]. In October 2010, I expanded this result to first-order representable logics with the finite model property.From 2007 the unrestricted blocking rule is detached from the core of the MetTeL tableau prover and re-implemented as a separate rule.
• Most of the tableau calculi implemented in MetTeL are developed with use of the idea of extracting sound and complete tableau calculus from a first-order specification specification of semantics of a logic. This idea has been developed into a formal method of automatic generation of tableau calculi from a first-order sematic specifications. Together with the unrestricted blocking rule, this gives a semi-automatic method of developing tableau decision procedures for logics admitting finite filtrations [TABLEAUX2009].
• I use a simple indexing technique which allows to avoid repeated formulae unifications. The technique is not developed well but dramatically improved performance of the prover core.
• From the very start of the implementation formulae of the form @i i or i:{i} are used to provide domain predication. This idea allows to avoid many unnecessary instantiations in tableau derivations while not introducing a new predicate which is true on all individuals occurred in a branch.
• Starting from the version 1.0, the tableau language allows arbitrary Skolem functions which can be used in premises and conclusions of tableau rules. Use of Skolem function in premises leads to a non-standard kind of tableau rules which cannot yet be handled by other known tableau provers.