Integrating SVC and HOL with the PROSPER Toolkit
Stevenson, Alan; Dennis, Louise Abigail
Louise Abigail Dennis
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.
|Publication Date||Jan 1, 2000|
|Peer Reviewed||Not Peer Reviewed|
|APA6 Citation||Stevenson, A., & Dennis, L. A. (2000). Integrating SVC and HOL with the PROSPER Toolkit|
|Copyright Statement||Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf|
|Additional Information||Published in OGI Technical Report CSE 00-009|
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf