| EPSRC Reference: |
GR/R52954/01 |
| Title: |
Flexible incorporation of decision procedures into the LambdaClam proof-planning system |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 June 2001 |
Ends: |
30 September 2002 |
Value (£): |
19,670
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Describe the proposed research in about 200 words. It is generally accepted that future practical theorem provers must contain both heuristic components and decision procedures. In order to use the power of decision procedures for small decidable theories in larger theories, we need a system which can combine decision procedures and/orwhich can incorporate them into a heuristic component of a prover. There are several important goals in defining schemes for combining and iincorporating decision procedures; some of them are: a formal, precise description (which should enable implementing the scheme into different provers and also which should enable formal reasoning about the scheme) and a flexible architecture of the scheme (which should make the scheme applicable to different decision procedures, different theories and different theorem provers). We defined a so called GS/SGS system for flexibly combining and incorporating decision procedures into theorem provers (and we made a prototype implementation). The system is capable of covering most of the influential approaches to solving this problem. We plan to further refine and polish the system and to implement it in the LambdaClam proofplanning system.
|
|
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 |