TABLEAUX 2013 tutorial: Generating tableau provers using MetTeL2
Lecturers: Dr D. Tishkovsky and Dr R. A. Schmidt
|
|
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.
|
|
|