Details of Grant 

EPSRC Reference:	EP/E005322/1
Title:	Automated Reasoning in Large Structured Theories
Principal Investigator:	McCasland, Dr RL
Other Investigators:	Bundy, Professor A
Researcher Co-Investigators:
Project Partners:
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research
Starts:	01 May 2006	Ends:	31 July 2006	Value (£):	21,690
EPSRC Research Topic Classifications:	Artificial Intelligence Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
The main application domains of computer-based theorem proving are mathematical assistant systems, mathematical teaching assistants, and hardware and software verification in computer science. The formalisations of mathematical knowledge and software systems are typically organised in large structured theories and the conjectures of their properties need to be proved relative to some specific theory. In these domains human guidance of the automatic proof procedures is indispensable, even for theorems that are simple by human standards.Aside from providing guidance information about how to explore the search space, the human user has to select a relevant subset of the available axioms and lemmas which are provided to the theorem proving system and the performance of automatic proof procedures depends on the concise filtering of the available information. In case proof attempts fail, the user needs to either readjust the selected knowledge from the theories or he has to come up with a missing lemma which is not yet part of the knowledge contained in the theories. In these domains, a proof attempt consists not only of trying to prove a conjecture from a set of axioms, i.e. the classical theorem proving in-the-small , but takes place in a large, structured context of different theories. There has been intensive research and tool development for automated theorem proving, for representing and maintaining structured theories and for theory exploration to synthesise interesting properties of a new domain, but there has been little research about how to efficiently combine them to solve a given problem.In this project, we aim at the development of in-the-large reasoning procedures automating the combination of these three components in order to prove a given conjecture. To this end we will develop a set of criteria characterising the kind of information the components can provide: How can we filter relevant knowledge from the structure of the theories and the kind of knowledge contained therein; how can we analyse failed proof attempts in order to determine our needs for additional knowledge; how can we decide when additional theory exploration is necessary and how to combine theory exploration with structured theories. The developed criteria will then serve as a basis for the design and implement of in-the-large reasoning techniques.
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.ed.ac.uk