Tutorial Description
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.
Topics
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.