| EPSRC Reference: |
GR/N20492/01 |
| Title: |
EFFICIENT FIRST-ORDER THEOREM PROVING |
| Principal Investigator: |
Voronkov, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Victoria University of Manchester, The |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 June 2000 |
Ends: |
31 May 2002 |
Value (£): |
62,007
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The main aim of the project is to strengthen our world leading position in first-order theorem proving. Our system Vampire won the last competition of first-order theorem provers at the International Conference on Automated Deduction. The project is centered around the implementation of better algorithms and datastructures for Vampire. The main subareas within the project are: (i) term indexing and implementation, (ii) propositional theorem proving, (iii) constraints in first-order reasoning.Keywords describing areas of proposaLAutomated reasoning, verification, term indexing, constraints in automated reasoning
|
|
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: |
|