Rippling in PVS
Rippling is a method of controlling rewriting of the terms in an induction step of an inductive proof, to ensure that a position is reached whereby the induction hypothesis can be applied. Rippling was developed primarily by the Mathematical Reasoning Group at the University of Edinburgh. The prima...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
2003
|
| Online Access: | https://eprints.nottingham.ac.uk/320/ |
| _version_ | 1848790392083841024 |
|---|---|
| author | Adams, Andrew A. Dennis, Louise Abigail |
| author2 | Archer, Myla |
| author_facet | Archer, Myla Adams, Andrew A. Dennis, Louise Abigail |
| author_sort | Adams, Andrew A. |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Rippling is a method of controlling rewriting of the terms in an induction step of an inductive proof, to ensure that a position is reached whereby the induction hypothesis can be applied.
Rippling was developed primarily by the Mathematical Reasoning Group at the University of Edinburgh. The primary implementations are in the two proof planning systems Clam and Lambda-Clam. An implementation is also available in HOL. In this paper we explain how we plan to implement rippling as a tactic for automatic generation of proofs requiring induction in PVS.
Rippling has mostly been used as part of a larger project for developing high-level proof strategies, but has rarely been applied
to $quot;real-world$quot; examples. Once we have this implementation we intend to assess the utility of this as a tactic by running rippling on the large number of inductive proofs developed by Gottliebsen as part of the PVS Real Analysis library.
By comparing the performance of the automation offered by rippling on these proofs with the original proof, which were proved by a combination
of hand-generation of proofs and by existing PVS strategies, we hope to assess the utility of rippling as a technique for real-world applications. |
| first_indexed | 2025-11-14T18:11:53Z |
| format | Conference or Workshop Item |
| id | nottingham-320 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:53Z |
| publishDate | 2003 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3202020-05-04T20:31:53Z https://eprints.nottingham.ac.uk/320/ Rippling in PVS Adams, Andrew A. Dennis, Louise Abigail Rippling is a method of controlling rewriting of the terms in an induction step of an inductive proof, to ensure that a position is reached whereby the induction hypothesis can be applied. Rippling was developed primarily by the Mathematical Reasoning Group at the University of Edinburgh. The primary implementations are in the two proof planning systems Clam and Lambda-Clam. An implementation is also available in HOL. In this paper we explain how we plan to implement rippling as a tactic for automatic generation of proofs requiring induction in PVS. Rippling has mostly been used as part of a larger project for developing high-level proof strategies, but has rarely been applied to $quot;real-world$quot; examples. Once we have this implementation we intend to assess the utility of this as a tactic by running rippling on the large number of inductive proofs developed by Gottliebsen as part of the PVS Real Analysis library. By comparing the performance of the automation offered by rippling on these proofs with the original proof, which were proved by a combination of hand-generation of proofs and by existing PVS strategies, we hope to assess the utility of rippling as a technique for real-world applications. Archer, Myla Di Vito, Ben Munoz, Cesar 2003 Conference or Workshop Item PeerReviewed Adams, Andrew A. and Dennis, Louise Abigail (2003) Rippling in PVS. In: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), September 8, 2003, Rome, Italy. |
| spellingShingle | Adams, Andrew A. Dennis, Louise Abigail Rippling in PVS |
| title | Rippling in PVS |
| title_full | Rippling in PVS |
| title_fullStr | Rippling in PVS |
| title_full_unstemmed | Rippling in PVS |
| title_short | Rippling in PVS |
| title_sort | rippling in pvs |
| url | https://eprints.nottingham.ac.uk/320/ |