Skip to main content

Research Repository

See what's under the surface

Advanced Search

Integrating SVC and HOL with the PROSPER Toolkit

Stevenson, Alan; Dennis, Louise Abigail

Authors

Alan Stevenson

Louise Abigail Dennis



Abstract

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

Files

prospersvc.ps (303 Kb)
Other

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





Downloadable Citations

;