EPSRC Reference: 
EP/E005322/1 
Title: 
Automated Reasoning in Large Structured Theories 
Principal Investigator: 
McCasland, Dr RL 
Other Investigators: 

Researcher CoInvestigators: 

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 computerbased 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 inthesmall , 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 inthelarge 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 inthelarge reasoning techniques.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic 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 