Automated Prover Generation
- EPSRC Research Project EP/H043748/1
-
- Principal Investigator:
- Dr Renate Schmidt
- Researcher Co-Investigator:
- 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,
multi-agent 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 fully-automated reasoning tool is however a
time-consuming 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 fully-functioning
stand-alone provers specialised for the users application.
MetTeL is system that takes as input a high-level 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,
knowledge-based 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
hypertableau-style 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 well-known 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, three-valued 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 applications 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 push-button 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.
Another important outcome of the project is the development and
evaluation of a generic model generation paradigm for first-order
logic. Model generation is important for fault analysis, debugging of
formal specifications of security protocols, programs and ontology-based
knowledge processing. The research disproves a frequently made claim that
resolution-based inference cannot decide the Bernays-Schoenfinkel class,
which provides the foundation for Datalog, a tool widely used in database
practice.
-
MetTeL and the accompanying tools are freely available from the MetTeL
website http://www.mettel-prover.org.
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 web-interface is also provided.
-
SPASS-Yarralumla -
A bottom-up model generater and first-order theorem prover implementing
sophisticated forms of blocking and other enhancements.
- 1
-
MetTeL website.
http://www.mettel-prover.org.
- 2
-
P. Baumgartner, and R. A. Schmidt.
Blocking and Other Enhancements for Bottom-Up Model Generation Methods.
Journal of Automated Reasoning 64(2):197-251, 2020.
- 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 uk-ac-man-scw:161817 of Escholar,
pages 23-24. 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
111-118. 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, PAAR-2010:
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning,
volume 9 of EPiC Series, pages 63-73. 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 (DL-2012), volume 846
of CEUR Workshop Proceedings. CEUR-WS.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. Larchey-Wendling, editors, Automated
Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013), volume
8123 of Lecture Notes in Computer Science, pages 188-202. 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 (DL-2013), volume Vol-1014 of CEUR Workshop Proceedings, pages
724-734. CEUR-WS.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, PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of
Automated Reasoning, volume 21 of EPiC Series, pages 109-123.
EasyChair, 2012.
- 9
-
R. A. Schmidt.
Simulation and synthesis of deduction calculi.
Electronic Notes in Theoretical Computer Science, 262:221-229,
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 40-49. Springer, 2011.
- 11
-
R. A. Schmidt.
The Ackermann approach for modal logic, correspondence theory and
second-order reduction.
Journal of Applied Logic, 10(1):52-74, 2012.
- 12
-
R. A. Schmidt, J. G. Stell, and D. Rydeheard.
Axiomatic and tableau-based reasoning for Kt(H,R).
In R. Goré, B. Kooi, and A. Kurucz, editors, Advances in
Modal Logic, Volume 10, pages 478-497, London, 2014. College Publications.
- 13
-
R. A. Schmidt and D. Tishkovsky.
Automated synthesis of tableau calculi.
Logical Methods in Computer Science, 7(2):1-32, 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 30-31. Technical Report TR-2011-327,
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 e-Print 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 bi-intuitionistic 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 412-428. Springer, 2014.
- 18
-
D. Tishkovsky and R. A. Schmidt.
Refinement in the tableau synthesis framework, 2013.
arXiv e-Print 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 3-4. Technical Report TR-2011-327,
Department of Computing Science, University of Glasgow, 2011.
- 20
-
D. Tishkovsky, R. A. Schmidt, and M. Khodadadi.
MetTeL: A tableau prover with logic-independent 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 242-247. 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 uk-ac-man-scw:161817 of Escholar,
pages 25-26. 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, PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of
Automated Reasoning, volume 21 of EPiC Series, pages 149-162.
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 492-495. Springer, 2012.
- 24
-
M. Zawidzki, R. A. Schmidt, and D. Tishkovsky.
Satisfiability problem for modal logic with global counting operators
coded in binary is NExpTime-complete.
Information Processing Letters, 113(1-2):34-38, 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 2014-10-16
Renate A. Schmidt
2014-10-16