Details of Grant 

EPSRC Reference:	EP/H043748/1
Title:	Automated Prover Generation
Principal Investigator:	Schmidt, Dr RA
Other Investigators:
Researcher Co-Investigators:	Dr D Tishkovsky
Project Partners:
Department:	Computer Science
Organisation:	University of Manchester, The
Scheme:	Standard Research
Starts:	01 May 2010	Ends:	31 March 2014	Value (£):	410,798
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 16 Mar 2010 ICT Prioritisation Panel (March 10) Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.man.ac.uk