Automated Prover Generation
 EPSRC Research Project EP/H043748/1

 Principal Investigator:
 Dr Renate Schmidt
 Researcher CoInvestigator:
 Dr Dmitry Tishkovsky
 PhD Student:
 Mohammad Khodadadi
 Summer Internship students:
 Jacobus Meulen 2011, Tomas Alijevas 2013
 Academic visitor:
 Michal Zawidzki Oct. 2011, Jan.Jul. 2012.
 Start Date:
 01/04/2010
 End Date:
 31/03/2014
Reasoning is needed in many subfields of computer science from
verification of programs, ontology reasoning for the semantic web,
multiagent systems to artificial intelligence and text mining but
also other fields including mathematics, computational linguistics
and philosophy.
Automated theorem provers can ensure a much higher
level of trust in complex mathematical proofs, they can enable
us to automatically eliminate large classes of errors from software
systems, and communication protocols, and they can be used to support the
creation and reasoning in large knowledge bases and theories.
Implementing a fullyautomated reasoning tool is however a
timeconsuming and difficult undertaking.
To avoid the burden of developing a prover from scratch, or extend
and adapt an existing prover, this project has developed a tool,
called MetTeL, to automatically generate code of fullyfunctioning
standalone provers specialised for the users application.
MetTeL is system that takes as input a highlevel specification
of a logic, or a theory, together with a set of deduction rules and
then generates a prover for this logic and calculus.
Together with the tableau calculus synthesis framework, which we developed in
a previous EPSRC project, this provides for the first time a systematic
and nearly fully automated methodology for obtaining tableau provers
form the specification of a logical formalisation of an application.
Tableau synthesis amounts to a normalisation process of the definition
of the semantics of a logic.
Soundness and completeness of the obtained calculus follows from the
results of the general framework and termination can be guaranteed
with the unrestricted blocking technique, also developed in a previous
project.
Unrestricted blocking has the property that adding it to a sound and
complete semantic tableau calculus guarantees termination, for any
logic that has the finite model property.
For logics where the finite model property is already known this
therefore
provides an easy way of obtaining terminating calculi, from which
MetTeL will produce decision procedures than can then be integrated
as the reasoning component into decision support systems,
knowledgebased systems and the like.
So far nothing similar exists.
An important contribution of the project has been new generic
techniques for refining rules in semantic tableau calculi.
This significantly enhances the tableau synthesis framework, because
the refinements are based on automatically verifiable
conditions, which though weaker, are still general enough to be
relevant to a wide class of logics and obtain effective
hypertableaustyle calculi.
Other generic optimisation methods of tableau calculi have been
developed.
The generic heuristics for efficient management of search space in tableau derivations
were implemented for arbitrary tableau languages and automatically included
into the generated code of provers.
This includes wellknown techniques such as backjumping and conflict directed backtracking, but also
generic methods for optimising the traversal of the search space were developed
and tested with generated provers for different logics.
A series of secondary tools were developed within the project.
These includes automatic generation of testing and benchmarking tools
targeted towards the application.
A random generator can generate sets of random problems in accordance
with parameters given by the user.
A complementary tool for the random generator is a benchmarking tool
which allows to run lists of problems in parallel and gather runtime statistics.
Several case studies were conducted with MetTeL in order to evaluate
the acceptance by users and the practical benefit of generated
provers and to identify any issues and feed them back into the
development cycle.
The work included exploring applications and use of the tool for
various traditional modal logics, intuitionistic logic, threevalued logic, and
simple reasoning about properties of lists.
Essential use of MetTeL and tableau systems implemented with MetTeL was
made in these major case studies.
PhD project of Mohammad Khodadadi.
Various specialisations of the blocking mechanism were defined and
evaluated, and simulation of the standard blocking
techniques was shown.
Joint work with
Michal Zawidzki from the University of Lodz, Poland.
Joint work with Clare Dixon and Boris Konev from the University of Liverpool.
A method of dealing with fixpoints in the linear time temporal logic
was developed and tested.
Joint work with Stefan Minica from
Amsterdam.
Collaboration with Dr. John Stell (Leeds University) and Dr David Rydeheard
(University of Manchester).
The last two are new application which showed the tableau synthesis
and prover generation technology can be successfully applied to new
logical formalisations and significantly aid scientific research.
All these case studies have also shown the approach is especially useful
for systematic comparisons of different tableau calculi, different
strategies, and techniques for the same logical formalism.
Overall, the project has established automated prover generation as a
feasible, new research direction which provides pushbutton technology
for easy development of reasoning systems for applications requiring
logical reasoning.
Previously reasoning systems could only be developed by specialists
and with much effort.
Various case studies have shown the usefulness of the tableau synthesis
framework and MetTeL.
Theoretical findings of the project have revealed directions for further
development of the tools and methods for the prover synthesis approach.
MetTeL and the accompanying tools are freely available from the MetTeL
website
The website includes a user interface of the tool that
is designed to lead users through the steps of (i) specifying
the syntax of the logic and the tableau language, (ii) specifying
optional parameters, (iii) the tableau rules, and
(iv) the generation of the prover.
The possibility to run the generated prover
via a webinterface is also provided.
 1

MetTeL website.
http://www.mettelprover.org.
 2

C. Dixon, B. Konev, R. A. Schmidt, and D. Tishkovsky.
A labelled tableau approach for temporal logic with constraints.
In R. A. Schmidt and F. Papacchini, editors, Proceedings of the
Nineteenth Workshop on Automated Reasoning: Bridging the Gap Between Theory
and Practice (ARW 2012), volume ukacmanscw:161817 of Escholar,
pages 2324. Univ. Manchester, 2012.
 3

C. Dixon, B. Konev, R. A. Schmidt, and D. Tishkovsky.
Labelled tableaux for temporal logic with cardinality constraints.
In Proceedings of the 14th International Symposium on Symbolic
and Numeric Algorithms for Scientific Computing (SYNASC 2012), pages
111118. IEEE Computer Society, 2012.
 4

U. Hustadt and R. A. Schmidt.
A comparison of solvers for propositional dynamic logic.
In B. Konev, R. A. Schmidt, and S. Schulz, editors, PAAR2010:
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning,
volume 9 of EPiC Series, pages 6373. EasyChair, 2012.
 5

M. Khodadadi, R. A. Schmidt, and D. Tishkovsky.
An abstract tableau calculus for the description logic
using unrestricted blocking and rewriting.
In Y. Kazakov, D. Lembo, and F. Wolter, editors, Proceedings of
the 2012 International Workshop on Description Logics (DL2012), volume 846
of CEUR Workshop Proceedings. CEURWS.org, 2012.
 6

M. Khodadadi, R. A. Schmidt, and D. Tishkovsky.
A refined tableau calculus with controlled blocking for the
description logic
.
In D. Galmiche and D. LarcheyWendling, editors, Automated
Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013), volume
8123 of Lecture Notes in Computer Science, pages 188202. Springer,
2013.
 7

M. Khodadadi, R. A. Schmidt, and D. Tishkovsky.
A refined tableau calculus with controlled blocking for the
description logic
.
In Thomas Eiter, Birte Glimm, Yevgeny Kazakov, and Markus Krötzsch,
editors, Proceedings of the 26th International Workshop on Description
Logics (DL2013), volume Vol1014 of CEUR Workshop Proceedings, pages
724734. CEURWS.org, 2013.
 8

S. Minica, M. Khodadadi, D. Tishkovsky, and R. A. Schmidt.
Synthesising and implementing tableau calculi for interrogative
epistemic logics.
In P. Fontaine, R. A. Schmidt, and S. Schulz, editors, PAAR2012: Proceedings of the Third Workshop on Practical Aspects of
Automated Reasoning, volume 21 of EPiC Series, pages 109123.
EasyChair, 2012.
 9

R. A. Schmidt.
Simulation and synthesis of deduction calculi.
Electronic Notes in Theoretical Computer Science, 262:221229,
2010.
 10

R. A. Schmidt.
Synthesising terminating tableau calculi for relational logics:
Invited paper.
In H. de Swart, editor, Relational and Algebraic Methods in
Computer Science (RAMiCS 12), volume 6663 of Lecture Notes in Computer
Science, pages 4049. Springer, 2011.
 11

R. A. Schmidt.
The Ackermann approach for modal logic, correspondence theory and
secondorder reduction.
Journal of Applied Logic, 10(1):5274, 2012.
 12

R. A. Schmidt, J. G. Stell, and D. Rydeheard.
Axiomatic and tableaubased reasoning for Kt(H,R).
In R. Goré, B. Kooi, and A. Kurucz, editors, Advances in
Modal Logic, Volume 10, pages 478497, London, 2014. College Publications.
 13

R. A. Schmidt and D. Tishkovsky.
Automated synthesis of tableau calculi.
Logical Methods in Computer Science, 7(2):132, 2011.
 14

R. A. Schmidt and D. Tishkovsky.
Solving rule admissability problem for S4 by a tableau method.
In A. Miller and R. Kirwan, editors, Proceedings of the
Eighteenth Workshop on Automated Reasoning: Bridging the Gap Between Theory
and Practice (ARW 2011), pages 3031. Technical Report TR2011327,
Department of Computing Science, University of Glasgow, 2011.
 15

R. A. Schmidt and D. Tishkovsky.
Using tableau to decide description logics with full role negation
and identity, 2012.
arXiv ePrint 1208.1476v1 [cs.LO].
 16

R. A. Schmidt and D. Tishkovsky.
Using tableau to decide description logics with full role negation
and identity.
ACM Transactions on Computational Logic, 15(1), 2014.
 17

J. G. Stell, R. A. Schmidt, and D. Rydeheard.
Tableau development for a biintuitionistic tense logic.
In P. Jipsen and W. Kahl, editors, Relational and Algebraic
Methods in Computer Science (RAMiCS 14), volume 8428 of Lecture Notes
in Computer Science, pages 412428. Springer, 2014.
 18

D. Tishkovsky and R. A. Schmidt.
Refinement in the tableau synthesis framework, 2013.
arXiv ePrint 1305.3131v1 [cs.LO].
 19

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
Mettel: A generic tableau prover.
In A. Miller and R. Kirwan, editors, Proceedings of the
Eighteenth Workshop on Automated Reasoning: Bridging the Gap Between Theory
and Practice (ARW 2011), pages 34. Technical Report TR2011327,
Department of Computing Science, University of Glasgow, 2011.
 20

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
MetTeL: A tableau prover with logicindependent inference engine.
In K. Brünnler and G. Metcalfe, editors, Automated Reasoning
with Analytic Tableaux and Related Methods (TABLEAUX 2011), volume 6793 of
Lecture Notes in Artificial Intelligence, pages 242247. Springer,
2011.
 21

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
Mettel2: Towards a prover generation platform.
In R. A. Schmidt and F. Papacchini, editors, Proceedings of the
Nineteenth Workshop on Automated Reasoning: Bridging the Gap Between Theory
and Practice (ARW 2012), volume ukacmanscw:161817 of Escholar,
pages 2526. Univ. Manchester, 2012.
 22

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
MetTeL2: Towards a tableau prover generation platform.
In P. Fontaine, R. A. Schmidt, and S. Schulz, editors, PAAR2012: Proceedings of the Third Workshop on Practical Aspects of
Automated Reasoning, volume 21 of EPiC Series, pages 149162.
EasyChair, 2012.
 23

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
The tableau prover generator MetTeL2.
In L. F. del Cerro, A. Herzig, and J. Mengin, editors, Proceedings of the 13th European Conference on Logics in Artificial
Intelligence (JELIA 2012), volume 7519 of Lecture Notes in Computer
Science, pages 492495. Springer, 2012.
 24

M. Zawidzki, R. A. Schmidt, and D. Tishkovsky.
Satisfiability problem for modal logic with global counting operators
coded in binary is NExpTimecomplete.
Information Processing Letters, 113(12):3438, 2013.
Automated Prover Generation
This document was generated using the
LaTeX2HTML translator Version 2012 (1.2)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html no_navigation split 0 dir website prover_gen.tex
The translation was initiated by Renate A. Schmidt on 20141016
Renate A. Schmidt
20141016