EPSRC logo

Details of Grant 

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:
Artificial Intelligence
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