Content

In this tutorial we discuss an approach of generating tableau provers for propositional non-classical logics on the example of an implemented prover generator MetTeL2.

• We describe syntax and tableau specification languages of MetTeL2, talk about options accepted by the generator and its command line parameters.
• We explain usage of provers generated by MetTeL2 and discuss the generic tableau algorithm providing the basis for the provers.
• Since the MetTeL2 tableau algorithm is one of the first implementations for non-classical logics which combines tableau reasoning and ordered rewriting, we discuss the purpose and advantages of the ordered rewriting in the algorithm, and how the rewriting is triggered within tableau derivations.
• We briefly talk about generic optimisations of tableau derivations which are implemented within the algorithm such as dynamic backtracking, conflict-directed backjumping, and branch merging.
• We consider several examples of various known logics and discuss different possibilities in the specification of the syntax and tableau calculi for these logics in MetTeL2.
• Experimenting with specifications and applying rule refinement methods from the tableau synthesis framework we achieve better performance of the generated provers and discuss why the speed-up has been obtained.
• We propose several ways of specifying blocking with sound blocking rules to ensure the generated provers are decision procedures.
• We show a special trick with syntax and tableau rule specifications which allows to check ``bad'' and ``good'' loops in tableau derivations for logics with fix-point operators.
• Finally, we briefly discuss how the generated code can be used, extended, and improved by a technically advanced user.
• Additionally, we give a short introduction how to use special Java classes also generated by MetTeL2 for obtaining random formulae in the language of specified logics.