| EPSRC Reference: |
GR/L31104/01 |
| Title: |
DEVELOPMENT OF AN INDUCTIVE PROOF ASSISTANT FOR Z INTEGRATING CLASSICAL AND REWRITE STRATEGIES |
| Principal Investigator: |
Frisch, Dr A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of York |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 1997 |
Ends: |
30 April 2000 |
Value (£): |
228,657
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Z is a formal specification language based upon Zermelo-Frankal set theory that is extensively used in both academia and industry. Several tools have been developed for reasoning about Z specifications, but they all lack substantial facilities for inductive reasoning. We propose the development of such as reasoning assistant for Z. Utilising the concept of ordered covering , our proposed approach will combine aspects of both the classical and rewrite-based approaches to proof by induction. In particular, it will include the classical induction on variables and use of heuristics, and the re-write induction on subterms and unification for generation of induction cases. In this way, we will not be developing an inductive reasoner for Z but will be furthering our understanding of the automation of proof by induction. To ensure that our reasoning principles and strategies are appropriate for Z, we propose to implement them in CADiz, an interactive reasoning tool for Z developed by University of York. We will evaluate the utility of the resulting system by attempting to construct a broad range of proofs, including some of practical importance to computer security, safety-critical systems and compiler correctness.
|
|
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.york.ac.uk |