| EPSRC Reference: |
GR/K84981/01 |
| Title: |
DIFFERENCE REDUCTION TECHNIQUES IN AUTOMATING THEOREM PROVING |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Artificial Intelligence |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 June 1996 |
Ends: |
31 August 1996 |
Value (£): |
12,443
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Using formal methods in software engineering requires a considerable amount of deductive support to fulfil the various proof obligations arising from the verification tasks. Although theorem proving has a long tradition in AI, it still lacks an efficient control of the tremendous search space for these proof problems.In recent years considerable progress was made to guide inductive proofs by difference-reduction technique called rippling. Rippling is based on an explicit notion of syntactical differences of formulas which allows one to predict certain effects of applying deduction rules in advance. Since the target situation of the deduction process can be sufficiently described in terms of these effects they can be used for hierarchical planning of inductive proof. Motivated by the success of guiding inductive proofs, the proposed work will be concerned with a generalisation of this approach to general first order theorem proving and will be based on ongoing research activities in Saarbrcken and Edinburgh.
|
|
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 |