Automated Prover Generation

Reasoning is needed in many areas of computing from verification of programs, ontology reasoning for the semantic web, multi-agent systems to artificial intelligence and text mining and also other fields including mathematics, computational linguistics and philosophy. Successful 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 of and reasoning in large knowledge bases and web-based repositories.Implementing a fully-automated reasoning tool is a time-consuming and difficult undertaking. Currently, researchers requiring an automated reasoning tool for an application can develop a prover from scratch; they can extend and adapt an existing prover; they can use an existing prover for a wider logic into which their logic can be embedded, e.g., a prover for first-order logic or higher-order logic; or they can use logical frameworks or prover development platforms. While these approaches have led to impressive successes, all these approaches are difficult to adopt for users without significant expertise in logic and automated reasoning.As an alternative the aim of this project is to automatically generate implemented provers. The idea is that users will be able to define a logical formalisation of their application. This is automatically transformed first into a deduction calculus and then into an implemented prover. The way this is envisaged to work is similar to a compiler or interpreter, which automatically transforms a program written in a high-level programming language into machine-code or byte-code. The difference is that the input to the prover generator is not a set of instructions, but a high-level specification of a logic or a theory. This project will focus on the automated generation of tableau provers. The foundation for tableau prover generation will be a tableau calculus synthesis framework that we developed in recent work and have already applied to a number of logics. Based on this framework the software to be developed will be able to automatically generate a sound and complete tableau calculus for the given logic or theory. We believe that it is now possible to go further and develop software that will automatically generate an implemented automated theorem prover for this calculus. This will give non-expert users and developers the ability to obtain implemented provers with relative ease in a supported way. For the user crucially this removes the burden of being concerned with proving soundness, completeness and decidability results, and implementing or adapting a prover.We will extend the theoretical foundation of the framework in various ways in order to make it more comprehensive and extend the scope of tableau methods as decision procedures. A series of tools will be developed: a tableau prover generator program and auxiliary software to ensure reliability, correctness and efficiency of the generator and the generated provers. To allow for the rapid employment of the technology and receive feedback from users a first prototype will be completed and released within one year and two tutorials will be organised. Several case studies will be conducted with the prototype to identify important issues that may need to be changed and improved in the prototype. Areas where it is crucial to find optimisations are rule refinement, prover efficiency, and generalisation of the framework. To quantify the success of the project, the utility of the developed tools and the generated provers, the acceptance by users and the practical benefit of generated provers an evaluation will be conducted.Overall, automated prover generation is a new and difficult research problem, but we believe that it is now a real possibility that we intend to realise in this project.

Who will benefit? The most immediate beneficiaries of this work are researchers and students working in the area of logic and automated reasoning. However, any users and developers in the many application domains within which reasoning plays an important role will benefit. This is where we expect the maximum impact to be. How will they benefit? Currently, the descriptions of tableau calculi in the literature far outnumber the implementations of tableau calculi. We believe that automated prover generation can help to close this gap. We expect the number of implemented systems to increase significantly. It will not be necessary that users have expert knowledge of automated reasoning techniques in order to implement provers. Through an easy-to-learn specification language they will be able to easily build a prover for their particular application. The prover will produce derivations and models in an easy-to-learn language. We envisage semantic web engineers and companies to be able to tailor different provers for different ontologies and websites. We envisage companies in the hardware and software industry to use prover generation technology to develop systems for supporting the business/development processes in their companies and for verifying the correctness of chips and software products. We envisage people working in the area of text mining and natural language processing to be able to generate provers and integrate them into their natural language analysis tools. We envisage people developing agent programming environments to be able to integrate implemented provers with their tools. For the end-user we envisage the following benefits. Improved quality and reliability of automated reasoning tools. Much reduced development time and resources for the implementation process, because provers do not need to be implemented from scratch. Though this may be a bit speculative, we expect to see improved understanding of logical reasoning and formalisation processes through the need to learn an abstract logical specification language. Easier maintenance, because new advances in prover development can be incorporated into the prover generator technology without the specification of the logic or the application needing to change. Incremental development of automated reasoning tools. As mentioned in 'Academic Beneficiaries' above, a long-term consequence for academic beneficiaries and research in automated reasoning could be a new prover generation paradigm. What will be done to ensure that they have the opportunity to benefit? The developed software will be made freely available under a permissive license that will maximise uptake of the technology by academic and industrial users. To overcome the expected skepticism of users and researchers the existence of a well-developed working system is crucial so that it is possible for anybody to experiment with the system and exploit the technology in their work. We thus aim to have a working prototype ready for general use as early as possible in the life cycle of the project. This will allow us to take on board feedback received from early users. For interested researchers, students and industrial users we plan to run 2 tutorials on automated tableau prover generation. To maximise impact we will organise the tutorials in association with large international conferences and/or at established summer schools. The results of the research will be presented at leading international conferences and workshops and will be published in respected scientific journals. The results of the PhD project will be written up as a PhD thesis. A website will be set up for the project where background information to the project, tutorial material, demos, reports and published papers will be made available. The website will give free access to repositories of problems, logic specifications and calculi. There a download area for source code of the prover generation tool as well as other developed tools.