Automated Reasoning in Large Structured Theories

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics


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.


10 25 50