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

Summary

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.

Various mainstream and non-mainstream description logics with emphasis on $\cal SHOI$ .

PhD project of Mohammad Khodadadi. Various specialisations of the blocking mechanism were defined and evaluated, and simulation of the standard blocking techniques was shown.

Hybrid modal logic with counting quantifiers.

Joint work with Michal Zawidzki from the University of Lodz, Poland.

Linear temporal logic with Boolean constraints.

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.

Interrogative-epistemic logics for reasoning about questions and queries of multiple agents.

Joint work with Stefan Minica from Amsterdam.

Logics and algebras of hypergraphs with relevance to image processing.

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.

Software

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.

Bibliography

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 ${\mathcal SHOI}$ 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 $\mathcal SHOI$ .
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 ${\mathcal SHOI}$ .
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.

About this document ...

Automated Prover Generation

This document was generated using the LaTeX2HTML translator Version 2012 (1.2)

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