Integrating SVC and HOL with the PROSPER Toolkit
We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit. The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexam...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2000
|
| Online Access: | https://eprints.nottingham.ac.uk/342/ |
| _version_ | 1848790395568259072 |
|---|---|
| author | Stevenson, Alan Dennis, Louise Abigail |
| author_facet | Stevenson, Alan Dennis, Louise Abigail |
| author_sort | Stevenson, Alan |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit.
The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting. |
| first_indexed | 2025-11-14T18:11:56Z |
| format | Conference or Workshop Item |
| id | nottingham-342 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:56Z |
| publishDate | 2000 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3422020-05-04T20:33:00Z https://eprints.nottingham.ac.uk/342/ Integrating SVC and HOL with the PROSPER Toolkit Stevenson, Alan Dennis, Louise Abigail We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit. The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting. 2000 Conference or Workshop Item NonPeerReviewed Stevenson, Alan and Dennis, Louise Abigail (2000) Integrating SVC and HOL with the PROSPER Toolkit. In: Theorem Proving in Higher Order Logics (TPHOLs 2000) Supplemental Proceedings, 2000, Oregon Graduate Institute, USA. |
| spellingShingle | Stevenson, Alan Dennis, Louise Abigail Integrating SVC and HOL with the PROSPER Toolkit |
| title | Integrating SVC and HOL with the PROSPER Toolkit |
| title_full | Integrating SVC and HOL with the PROSPER Toolkit |
| title_fullStr | Integrating SVC and HOL with the PROSPER Toolkit |
| title_full_unstemmed | Integrating SVC and HOL with the PROSPER Toolkit |
| title_short | Integrating SVC and HOL with the PROSPER Toolkit |
| title_sort | integrating svc and hol with the prosper toolkit |
| url | https://eprints.nottingham.ac.uk/342/ |