Tutorial: Generating tableau provers using MetTeL2
Lecturers: Dr D. Tishkovsky and Dr R. A. Schmidt
Non-classical logics, including modal logics, description logic, hybrid logics and intuitionistic logic, are popular and have many applications. The applications range from multi-agent systems to medical domains, web services and the semantic web. Despite the wide variety of logical formalisms and the importance for applications, for many of these logical formalisms no provers exists.
We developed a framework for synthesising sound, complete, and often terminating, tableau calculi from semantic specifications of propositional non-classical logics. Intended to complement this theoretical framework we have implemented a tool, called MetTeL2, for generating tableau provers from specification of the syntax of a logic and the specification of a tableau calculus for this logic (see the system description). MetTeL2 is designed to be as general as possible, allowing provers to be generated for very expressive logics, including logics not considered in the literature and logics for which no provers exist as yet. The intention is to make it very easy for users to obtain (almost at the touch of a button) correctly running reasoning tools, in many cases even decision procedures.
The tool is useful for experimenting with different calculi for different logics and different semantics, and, thus, is useful for research purposes but also in teaching and learning environments. Along with providing modularity and extensibility of the generated code an important concern is efficiency of the generated provers. In this respect, the rule refinement methodology of the tableau synthesis framework can considerably improve the performance of the generated provers. It also leads to exciting possibilities to automatically refine calculi and improve search in provers which is one of our current research interests.
In this tutorial, we are going to cover the following topics:
- specification and generation of tableau provers for various propositional non-classical logics using the MetTeL2 prover generator,
- use of the generated provers and possibilities of extending the generated code,
- generating optimised provers by tweaking their specifications in MetTeL2,
- termination through various forms of blocking within MetTeL2,
- equality reasoning via ordered forward and backward rewriting in tableau derivations.
Please visit the tutorial page at http://www.cs.manchester.ac.uk/~dmitry/courses/TABLEAUX2013/.